From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 1 Mar 2007 15:45:33 +0000 (+0000)
Subject: procedural proof of ty3_gen_cast
X-Git-Tag: 0.4.95@7852~580
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a03d59129f60b894b64e4e003a5ac81ac3d9f936;p=helm.git

procedural proof of ty3_gen_cast
---

diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma
index cab82e7df..b975eaffb 100644
--- a/matita/contribs/prova.ma
+++ b/matita/contribs/prova.ma
@@ -15,66 +15,178 @@
 set "baseuri" "cic:/matita/test/prova".
 
 include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
-
-alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
-alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
-(*
-alias id "B" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1)".
-*)
-theorem not_abbr_abst:
- (Abbr\neq Abst)
-.(* tactics: 7 *)
-whd in \vdash (%).
-intros 1 (H).
-letin DEFINED \def (\lambda ee:B
- .match ee in B return \lambda _:B.Prop with 
-  [Abbr\rArr True|Abst\rArr False|Void\rArr False]).(* extracted *)
-cut (DEFINED Abbr) as ASSUMED;
-[rewrite > H in ASSUMED:(%) as (H0)
-|apply I
+alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
+alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
+alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)".
+alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)".
+alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)".
+alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)".
+alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)".
+alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)".
+theorem ty3_gen_cast:
+ (\forall g:G
+ .\forall c:C
+  .\forall t1:T
+   .\forall t2:T
+    .\forall x:T
+     .ty3 g c (THead (Flat Cast) t2 t1) x
+      \rarr pc3 c t2 x\land ty3 g c t1 t2)
+.
+(* tactics: 68 *)
+intros 6 (g c t1 t2 x H).
+apply insert_eq;(* 6 P P P C I I 3 0 *)
+[apply T(* dependent *)
+|apply (THead (Flat Cast) t2 t1)(* dependent *)
+|apply (\lambda t:T.ty3 g c t x)(* dependent *)
+|intros 2 (y H0).
+alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con".
+elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
+[intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
+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 *)
+clearbody H7.
+rewrite > H7 in H4:(%) as (H8).
+cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
+[id
+|apply H8.(* 1 I *)
+apply refl_equal(* 2 C C *)
+].
+elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *)
+intros 2 (H11 H12).
+apply conj;(* 4 C C I I *)
+[alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con".
+apply pc3_t;(* 6 P C C I C I *)
+[apply t3(* dependent *)
+|apply H11(* assumption *)
+|apply H5(* assumption *)
+]
+|apply H12(* assumption *)
+]
+|intros 3 (c0 m H1).
+alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)".
+cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr True
+|TLRef (_:nat)\rArr False
+|THead (_:K) (_:T) (_:T)\rArr False] as H2;
+[id
+|rewrite < H1 in \vdash (%).
+apply I
+].
+clearbody H2.
+change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr True
+|TLRef (_:nat)\rArr False
+|THead (_:K) (_:T) (_:T)\rArr False].
+elim H2 using False_ind names 0(* 2 C I 2 0 *)
+|intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
+cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr True
+|THead (_:K) (_:T) (_:T)\rArr False] as H5;
+[id
+|rewrite < H4 in \vdash (%).
+apply I
+].
+clearbody H5.
+change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr True
+|THead (_:K) (_:T) (_:T)\rArr False].
+elim H5 using False_ind names 0(* 2 C I 2 0 *)
+|intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
+cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr True
+|THead (_:K) (_:T) (_:T)\rArr False] as H5;
+[id
+|rewrite < H4 in \vdash (%).
+apply I
+].
+clearbody H5.
+change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr True
+|THead (_:K) (_:T) (_:T)\rArr False].
+elim H5 using False_ind names 0(* 2 C I 2 0 *)
+|intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7).
+alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)".
+alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)".
+cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr False
+|THead (k:K) (_:T) (_:T)\rArr 
+ match k in K return \lambda _:K.Prop with 
+ [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8;
+[id
+|rewrite < H7 in \vdash (%).
+apply I
+].
+clearbody H8.
+change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr False
+|THead (k:K) (_:T) (_:T)\rArr 
+ match k in K return \lambda _:K.Prop with 
+ [Bind (_:B)\rArr True|Flat (_:F)\rArr False]].
+elim H8 using False_ind names 0(* 2 C I 2 0 *)
+|intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5).
+cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr False
+|THead (k:K) (_:T) (_:T)\rArr 
+ match k in K return \lambda _:K.Prop with 
+ [Bind (_:B)\rArr False
+ |Flat (f:F)\rArr 
+  match f in F return \lambda _:F.Prop with 
+  [Appl\rArr True|Cast\rArr False]]] as H6;
+[id
+|rewrite < H5 in \vdash (%).
+apply I
+].
+clearbody H6.
+change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with 
+[TSort (_:nat)\rArr False
+|TLRef (_:nat)\rArr False
+|THead (k:K) (_:T) (_:T)\rArr 
+ match k in K return \lambda _:K.Prop with 
+ [Bind (_:B)\rArr False
+ |Flat (f:F)\rArr 
+  match f in F return \lambda _:F.Prop with 
+  [Appl\rArr True|Cast\rArr False]]].
+elim H6 using False_ind names 0(* 2 C I 2 0 *)
+|intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5).
+letin H6 \def (f_equal T T
+ (\lambda e:T
+  .match e in T return \lambda _:T.T with 
+   [TSort (_:nat)\rArr t3
+   |TLRef (_:nat)\rArr t3
+   |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
+ (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
+alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
+letin DEFINED \def (let H7 \def 
+        f_equal T T
+        (\lambda e:T
+         .match e in T return \lambda _:T.T with 
+          [TSort (_:nat)\rArr t0
+          |TLRef (_:nat)\rArr t0
+          |THead (_:K) (_:T) (t:T)\rArr t])
+        (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5
+ in
+ \lambda H8:t3=t2
+ .(let H11 \def 
+          eq_ind T t3
+          (\lambda t:T
+           .t0=THead (Flat Cast) t2 t1
+            \rarr pc3 c0 t2 t\land ty3 g c0 t1 t2) H2 t2 H8
+   in
+   let H12 \def eq_ind T t3 (\lambda t:T.ty3 g c0 t0 t) H1 t2 H8 in
+   eq_ind_r T t2 (\lambda t:T.pc3 c0 t2 t\land ty3 g c0 t1 t2)
+   (let H14 \def eq_ind T t0 (\lambda t:T.ty3 g c0 t t2) H12 t1 H7 in
+    conj (pc3 c0 t2 t2) (ty3 g c0 t1 t2) (pc3_refl c0 t2) H14) t3
+   H8)).
+apply DEFINED.(* 1 I *)
+apply H6(* assumption *)
+]
+|apply H(* assumption *)
 ].
-elim H0 using False_ind names 0.(* 2 C I 2 0 *)
 qed.
 
-alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
-alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
-alias id "Appl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/1)".
-alias id "Bind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/K.ind#xpointer(1/1/1)".
-alias id "Cast" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/2)".
-alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con".
-alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con".
-alias id "Flat" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/K.ind#xpointer(1/1/2)".
-alias id "lift" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs/lift.con".
-alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.con".
-alias id "pr0_beta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/3)".
-alias id "pr0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1)".
-alias id "pr0_comp" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/2)".
-alias id "pr0_delta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/5)".
-alias id "pr0_epsilon" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/7)".
-alias id "pr0_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0_ind.con".
-alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con".
-alias id "pr0_upsilon" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/4)".
-alias id "pr0_zeta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/6)".
-alias id "s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs/s.con".
-alias id "subst0_both" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/4)".
-alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)".
-alias id "subst0_confluence_neq" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_confluence_neq.con".
-alias id "subst0_fst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/2)".
-alias id "subst0_gen_head" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_head.con".
-alias id "subst0_gen_lift_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_lift_ge.con".
-alias id "subst0_lift_ge_s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/props/subst0_lift_ge_s.con".
-alias id "subst0_snd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/3)".
-alias id "subst0_subst0_back" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_subst0_back.con".
-alias id "subst0_trans" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_trans.con".
-alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)".
-alias id "THead" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1/3)".
-
-inline procedural
-   "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
-(*
-inline procedural
-   "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3/ty3_sred_wcpr0_pr0.con".
-
-inline procedural
-   "cic:/Coq/Reals/RiemannInt/FTC_Riemann.con".
-*)