X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_gen.v;fp=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_gen.v;h=0b634e59c8c314a4d90a7ad5817b64f3b0b2ec56;hb=1b21075e987872a2e3103203b4e67c939e4a9f6a;hp=0000000000000000000000000000000000000000;hpb=ea6b99ed26a954a578e3c88909479dcf9cab7345;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
new file mode 100644
index 000000000..0b634e59c
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
@@ -0,0 +1,104 @@
+(*#* #stop file *)
+
+Require lift_gen.
+Require lift_props.
+Require subst0_gen.
+Require pr0_defs.
+Require pr0_lift.
+
+   Section pr0_gen_abbr. (***************************************************)
+
+      Theorem pr0_gen_abbr : (u1,t1,x:?) (pr0 (TTail (Bind Abbr) u1 t1) x) ->
+                             (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
+                                         (pr0 u1 u2) &
+                                         (pr0 t1 t2) \/
+                                         (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
+                             ) \/
+                             (pr0 t1 (lift (1) (0) x)).
+      Intros.
+      Inversion H; Clear H; XDEAuto 6.
+      Qed.
+
+   End pr0_gen_abbr.
+
+   Section pr0_gen_void. (***************************************************)
+
+      Theorem pr0_gen_void : (u1,t1,x:?) (pr0 (TTail (Bind Void) u1 t1) x) ->
+                             (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
+                                         (pr0 u1 u2) & (pr0 t1 t2)
+                             ) \/
+                             (pr0 t1 (lift (1) (0) x)).
+      Intros.
+      Inversion H; Clear H; XEAuto.
+      Qed.
+
+   End pr0_gen_void.
+
+   Section pr0_gen_lift. (***************************************************)
+
+      Tactic Definition IH :=
+         Match Context With
+            | [ H: (_:?; _:?) ?0 = (lift ? ? ?) -> ?;
+                H0: ?0 = (lift ? ?2 ?3) |- ? ] ->
+               LApply (H ?3 ?2); [ Clear H H0; Intros H_x | XAuto ];
+               XElim H_x; Intro; Intros H_x; Intro;
+               Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
+
+(*#* #start file *)
+
+(*#* #caption "generation lemma for lift" *)
+(*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
+
+      Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
+                             (EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
+
+(*#* #stop file *)
+
+      Intros until 1; InsertEq H '(lift h d t1);
+      UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
+      Rename x into t3; Rename x0 into d.
+(* case 1 : pr0_r *)
+      XEAuto.
+(* case 2 : pr0_c *)
+      NewInduction k; LiftGen; Rewrite H3; Clear H3 t0;
+      IH; IH; XEAuto.
+(* case 3 : pr0_beta *)
+      LiftGen; Rewrite H3; Clear H3 t0.
+      LiftGen; Rewrite H3; Clear H3 H5 x1 k.
+      IH; IH; XEAuto.
+(* case 4 : pr0_gamma *)
+      LiftGen; Rewrite H6; Clear H6 t0.
+      LiftGen; Rewrite H6; Clear H6 x1.
+      IH; IH; IH.
+      Rewrite <- lift_d; [ Simpl | XAuto ].
+      Rewrite <- lift_flat; XEAuto.
+(* case 5 : pr0_delta *)
+      LiftGen; Rewrite H4; Clear H4 t0.
+      IH; IH; Arith3In H3 d; Subst0Gen.
+      Rewrite H3; XEAuto.
+(* case 6 : pr0_zeta *)
+      LiftGen; Rewrite H2; Clear H2 t0.
+      Arith7In H4 d; LiftGen; Rewrite H2; Clear H2 x1.
+      IH; XEAuto.
+(* case 7 : pr0_zeta *)
+      LiftGen; Rewrite H1; Clear H1 t0.
+      IH; XEAuto.
+      Qed.
+
+   End pr0_gen_lift.
+
+      Tactic Definition Pr0Gen :=
+         Match Context With
+            | [ H: (pr0 (TTail (Bind Abbr) ?1 ?2) ?3) |- ? ] ->
+               LApply (pr0_gen_abbr ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
+               XElim H;
+               [ Intros H; XElim H; Do 4 Intro; Intros H_x;
+                 XElim H_x; [ Intros | Intros H_x; XElim H_x; Intros ]
+               | Intros ]
+            | [ H: (pr0 (TTail (Bind Void) ?1 ?2) ?3) |- ? ] ->
+               LApply (pr0_gen_void ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
+               XElim H; [ Intros H; XElim H; Intros | Intros ]
+            | [ H: (pr0 (lift ?0 ?1 ?2) ?3) |- ? ] ->
+               LApply (pr0_gen_lift ?2 ?3 ?0 ?1); [ Clear H; Intros H | XAuto ];
+               XElim H; Intros
+            | _ -> Pr0GenBase.