]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/metasenv_ordering.ma
update in basic_2
[helm.git] / matitaB / matita / tests / metasenv_ordering.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 num (instance 0) = "natural number".
20 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
21
22 (* REWRITE *)
23
24 theorem th1 : 
25    \forall P:Prop.
26    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
27    1 = 1 \land 1 = 0 \land 2 = 2.
28    intros. split; split;
29    [ reflexivity
30    | rewrite > H;
31      [ reflexivity | exact nat | exact (0=0) | exact Type ]
32    ]
33 qed.    
34     
35 theorem th2 : 
36    \forall P:Prop.
37    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
38    1 = 1 \land 1 = 0 \land 3 = 3.
39    intros. split. split.
40    focus 13.
41      rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type].     
42    unfocus.
43    reflexivity.
44    reflexivity.
45 qed.       
46     
47 theorem th3 : 
48    \forall P:Prop.
49    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
50    1 = 1 \land 1 = 0 \land 4 = 4.
51    intros. split. split.
52    focus 13.
53      rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
54    unfocus.     
55    reflexivity.
56    reflexivity.
57 qed. 
58
59 theorem th4 : 
60    \forall P:Prop.
61    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
62    1 = 1 \land 1 = 0 \land 5 = 5.
63    intros. split. split.
64    focus 13.
65      rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
66    unfocus.     
67    reflexivity.
68    reflexivity.
69 qed. 
70
71 (* APPLY *)
72
73 theorem th5 : 
74    \forall P:Prop.
75    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
76    1 = 1 \land 1 = 0 \land 6 = 6.
77    intros. split. split.
78    focus 13.
79      apply H; [exact nat | exact (0=0) | exact Type].
80    unfocus.     
81    reflexivity.
82    reflexivity.
83 qed. 
84
85 theorem th6 : 
86    \forall P:Prop.
87    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
88    1 = 1 \land 1 = 0 \land 7 = 7.
89    intros. split. split.
90    focus 13.
91      apply (H ?); [exact nat | exact (0=0) | exact Type].
92    unfocus.     
93    reflexivity.
94    reflexivity.
95 qed.
96       
97 theorem th7 : 
98    \forall P:Prop.
99    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
100    1 = 1 \land 1 = 0 \land 8 = 8.
101    intros. split. split.
102    focus 13.
103      apply (H ? ?); [exact nat | exact (0=0) | exact Type].
104    unfocus.     
105    reflexivity.
106    reflexivity.
107 qed.     
108       
109 theorem th8 : 
110    \forall P:Prop.
111    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
112    1 = 1 \land 1 = 0 \land 9 = 9.
113    intros. split. split.
114    focus 13.
115      apply (H ? ? ?); [exact nat | exact (0=0) | exact Type].
116    unfocus.     
117    reflexivity.
118    reflexivity.
119 qed.
120
121 (* ELIM *)
122
123 theorem th9:
124   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
125   intros (P Q R S r s H).
126   elim (H ? ?); [split; assumption | exact r | exact s].
127   qed.
128  
129 theorem th10:
130   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
131   intros (P Q R S r s H).
132   elim (H ?); [split; assumption | exact r | exact s].
133   qed.
134   
135 theorem th11:
136   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
137   intros (P Q R S r s H).
138   elim H; [split; assumption | exact r | exact s].
139   qed.