]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/unfold.ma
restructuring
[helm.git] / matita / matita / tests / unfold.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16
17 include "coq.ma".
18
19 alias symbol "plus" (instance 0) = "Coq's natural plus".
20 definition myplus \def \lambda x,y. x+y.
21
22 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
23 lemma lem: \forall n. S (n + n) = (S n) + n.
24  intro; reflexivity.
25 qed.
26
27 theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
28  unfold myplus in \vdash (\forall _.(? ? ? %)).
29  intro.
30  unfold myplus.
31  rewrite > lem.
32  reflexivity.
33 qed.
34
35 (* This test needs to parse "uno" in the context of the hypothesis H,
36    not in the context of the goal. *)
37 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
38 theorem t: let uno \def S O in uno + uno = S uno \to uno=uno.
39  intros. unfold uno in H.
40  reflexivity.
41 qed.