1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/test/prova".
17 include "../legacy/coq.ma".
19 theorem pippo: \forall (A,B:Prop). A \land B \to A.
20 intros; decompose; assumption.
23 inline procedural "cic:/matita/test/prova/pippo.con".
25 alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
26 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
27 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
28 theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n).
29 intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
33 include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
34 alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
35 alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
36 alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)".
37 alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)".
38 alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)".
39 alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)".
40 alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)".
41 alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)".
48 .ty3 g c (THead (Flat Cast) t2 t1) x
49 \rarr pc3 c t2 x\land ty3 g c t1 t2)
52 intros 6 (g c t1 t2 x H).
53 apply insert_eq;(* 6 P P P C I I 3 0 *)
54 [apply T(* dependent *)
55 |apply (THead (Flat Cast) t2 t1)(* dependent *)
56 |apply (\lambda t:T.ty3 g c t x)(* dependent *)
58 alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con".
59 elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
60 [intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
61 letin H7 \def (f_equal T T (\lambda e:T.e) u (THead (Flat Cast) t2 t1) H6).(* 6 C C C C C I *)
62 rewrite > H7 in H4:(%) as (H8).
63 cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
66 apply refl_equal(* 2 C C *)
68 elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *)
70 apply conj;(* 4 C C I I *)
71 [alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con".
72 apply pc3_t;(* 6 P C C I C I *)
73 [apply t3(* dependent *)
74 |apply H11(* assumption *)
75 |apply H5(* assumption *)
77 |apply H12(* assumption *)
80 alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)".
81 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
82 [TSort (_:nat)\rArr True
83 |TLRef (_:nat)\rArr False
84 |THead (_:K) (_:T) (_:T)\rArr False] as H2;
86 |rewrite < H1 in \vdash (%).
90 change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
91 [TSort (_:nat)\rArr True
92 |TLRef (_:nat)\rArr False
93 |THead (_:K) (_:T) (_:T)\rArr False].
94 elim H2 using False_ind names 0(* 2 C I 2 0 *)
95 |intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
96 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
97 [TSort (_:nat)\rArr False
98 |TLRef (_:nat)\rArr True
99 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
101 |rewrite < H4 in \vdash (%).
105 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
106 [TSort (_:nat)\rArr False
107 |TLRef (_:nat)\rArr True
108 |THead (_:K) (_:T) (_:T)\rArr False].
109 elim H5 using False_ind names 0(* 2 C I 2 0 *)
110 |intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
111 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
112 [TSort (_:nat)\rArr False
113 |TLRef (_:nat)\rArr True
114 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
116 |rewrite < H4 in \vdash (%).
120 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
121 [TSort (_:nat)\rArr False
122 |TLRef (_:nat)\rArr True
123 |THead (_:K) (_:T) (_:T)\rArr False].
124 elim H5 using False_ind names 0(* 2 C I 2 0 *)
125 |intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7).
126 alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)".
127 alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)".
128 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
129 [TSort (_:nat)\rArr False
130 |TLRef (_:nat)\rArr False
131 |THead (k:K) (_:T) (_:T)\rArr
132 match k in K return \lambda _:K.Prop with
133 [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8;
135 |rewrite < H7 in \vdash (%).
139 change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
140 [TSort (_:nat)\rArr False
141 |TLRef (_:nat)\rArr False
142 |THead (k:K) (_:T) (_:T)\rArr
143 match k in K return \lambda _:K.Prop with
144 [Bind (_:B)\rArr True|Flat (_:F)\rArr False]].
145 elim H8 using False_ind names 0(* 2 C I 2 0 *)
146 |intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5).
147 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
148 [TSort (_:nat)\rArr False
149 |TLRef (_:nat)\rArr False
150 |THead (k:K) (_:T) (_:T)\rArr
151 match k in K return \lambda _:K.Prop with
152 [Bind (_:B)\rArr False
154 match f in F return \lambda _:F.Prop with
155 [Appl\rArr True|Cast\rArr False]]] as H6;
157 |rewrite < H5 in \vdash (%).
161 change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
162 [TSort (_:nat)\rArr False
163 |TLRef (_:nat)\rArr False
164 |THead (k:K) (_:T) (_:T)\rArr
165 match k in K return \lambda _:K.Prop with
166 [Bind (_:B)\rArr False
168 match f in F return \lambda _:F.Prop with
169 [Appl\rArr True|Cast\rArr False]]].
170 elim H6 using False_ind names 0(* 2 C I 2 0 *)
171 |intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5).
172 letin H6 \def (f_equal T T
174 .match e in T return \lambda _:T.T with
175 [TSort (_:nat)\rArr t3
176 |TLRef (_:nat)\rArr t3
177 |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
178 (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
179 letin H7 \def (f_equal T T
181 .match e in T return \lambda _:T.T with
182 [TSort (_:nat)\rArr t0
183 |TLRef (_:nat)\rArr t0
184 |THead (_:K) (_:T) (t:T)\rArr t]) (THead (Flat Cast) t3 t0)
185 (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
186 cut (t3=t2\rarr pc3 c0 t2 t3\land ty3 g c0 t1 t2) as DEFINED;
189 rewrite > H8 in H2:(%) as (UNUSED).
190 rewrite > H8 in H1:(%) as (H12).
191 rewrite > H8 in \vdash (%).
193 change in H7:(%) with (match THead (Flat Cast) t3 t0 in T return \lambda _:T.T with
194 [TSort (_:nat)\rArr t0
195 |TLRef (_:nat)\rArr t0
196 |THead (_:K) (_:T) (t:T)\rArr t]
197 =match THead (Flat Cast) t2 t1 in T return \lambda _:T.T with
198 [TSort (_:nat)\rArr t0
199 |TLRef (_:nat)\rArr t0
200 |THead (_:K) (_:T) (t:T)\rArr t]).
201 rewrite > H7 in H12:(%) as (H14).
202 apply conj;(* 4 C C I I *)
203 [alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
204 apply pc3_refl(* 2 C C *)
205 |apply H14(* assumption *)
208 apply DEFINED.(* 1 I *)
209 apply H6(* assumption *)
211 |apply H(* assumption *)
216 include "nat/orders.ma".
219 \forall P:nat \to Prop
223 (p1 = p2 \to P p2) \to
226 (p1 = n1 \to P n1) \to
227 p1 = S n1 \to P (S n1)) \to
229 intros 4; elim H names 0; clear H p1; intros;
230 [ apply H; reflexivity
231 | apply H3; clear H3; intros;
232 [ apply H | apply H1; clear H1; intros; subst;
233 [ apply H2; apply H3 | ]