From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 15 Jul 2005 18:18:13 +0000 (+0000)
Subject: some reorganization and some corrections
X-Git-Tag: pre_notation~3
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1ea21db6644417e6cd3c44c84915712a5321a37a;p=helm.git

some reorganization and some corrections
---

diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v
deleted file mode 100644
index 1050288ee..000000000
--- a/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v
+++ /dev/null
@@ -1,103 +0,0 @@
-(*#* #stop file *)
-
-Require pr0_subst0.
-Require pr3_defs.
-Require pr3_props.
-Require cpr0_defs.
-
-   Section cpr0_drop. (******************************************************)
-
-      Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
-                          (drop h (0) c1 (CTail e1 k u1)) ->
-                          (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
-                                      (cpr0 e1 e2) & (pr0 u1 u2)
-                          ).
-      Intros until 1; XElim H.
-(* case 1 : cpr0_refl *)
-      XEAuto.
-(* case 2 : cpr0_cont *)
-      XElim h.
-(* case 2.1 : h = 0 *)
-      Intros; DropGenBase.
-      Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
-(* case 2.2 : h > 0 *)
-      XElim k; Intros; DropGenBase.
-(* case 2.2.1 : Bind *)
-      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
-      XElim H0; XEAuto.
-(* case 2.2.2 : Flat *)
-      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
-      XElim H0; XEAuto.
-      Qed.
-
-      Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
-                               (drop h (0) c1 (CTail e1 k u1)) ->
-                               (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
-                                           (cpr0 e2 e1) & (pr0 u2 u1)
-                               ).
-      Intros until 1; XElim H.
-(* case 1 : cpr0_refl *)
-      XEAuto.
-(* case 2 : cpr0_cont *)
-      XElim h.
-(* case 2.1 : h = 0 *)
-      Intros; DropGenBase.
-      Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
-(* case 2.2 : h > 0 *)
-      XElim k; Intros; DropGenBase.
-(* case 2.2.1 : Bind *)
-      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
-      XElim H0; XEAuto.
-(* case 2.2.2 : Flat *)
-      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
-      XElim H0; XEAuto.
-      Qed.
-
-   End cpr0_drop.
-
-      Tactic Definition Cpr0Drop :=
-         Match Context With
-            | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
-                _: (cpr0 ?2 ?6) |- ? ] ->
-               LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
-               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
-               XElim H_x; Intros
-            | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
-                _: (cpr0 ?6 ?2) |- ? ] ->
-               LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
-               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
-               XElim H_x; Intros
-            | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
-                _: (cpr0 ?2 ?6) |- ? ] ->
-               LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
-               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
-               XElim H_x; Intros
-            | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
-                _: (cpr0 ?6 ?2) |- ? ] ->
-               LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
-               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
-               XElim H_x; Intros.
-
-   Section cpr0_pr3. (*******************************************************)
-
-      Theorem cpr0_pr3_t : (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
-                           (pr3 c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1 : cpr0_refl *)
-      XAuto.
-(* case 2 : cpr0_cont *)
-      Pr3Context.
-      XElim H1; Intros.
-(* case 2.1 : pr3_r *)
-      XAuto.
-(* case 2.2 : pr3_u *)
-      EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
-      Inversion_clear H1.
-(* case 2.2.1 : pr2_pr0 *)
-      XAuto.
-(* case 2.2.1 : pr2_delta *)
-      Cpr0Drop; Pr0Subst0.
-      EApply pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
-      Qed.
-
-   End cpr0_pr3.
diff --git a/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
new file mode 100644
index 000000000..c7382bf20
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
@@ -0,0 +1,20 @@
+Require Export subst0_defs.
+Require Export csubst0_defs.
+
+(*#* #caption "axioms for strict substitution in focalized terms",
+   "substituted term part", 
+   "substituted context part", 
+   "substituted both parts"
+*)
+(*#* #cap #cap c1, c2, t1, t2 #alpha v in W *)  
+
+      Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
+         | fsubst0_snd : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
+         | fsubst0_fst : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
+         | fsubst0_both : (t2:?) (subst0 i v t1 t2) ->
+                       (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
+
+(*#* #stop file *)
+
+      Hint fsubst0 : ltlc := Constructors fsubst0.
+
diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
index 106bfe66c..b5c7df937 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_props.v
@@ -1,73 +1,70 @@
 Require subst0_subst0.
 Require pr0_subst0.
+Require cpr0_defs.
 Require pr2_lift.
+Require pr2_gen.
 Require pr3_defs.
 
-(*#* #caption "main properties of predicate \\texttt{pr3}" *)
+(*#* #caption "main properties of the relation $\\PrT{}{}{}$" *)
 (*#* #clauses *)
 
 (*#* #stop file *)
 
    Section pr3_context. (****************************************************)
 
-      Theorem pr3_pr0_pr2_t : (u1,u2:?) (pr0 u1 u2) ->
-                              (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
-                              (pr3 (CTail c k u1) t1 t2).
-      Intros.
-      Inversion H0; Clear H0; XAuto.
+      Theorem pr3_pr0_pr2_t: (u1,u2:?) (pr0 u1 u2) ->
+                             (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+                             (pr3 (CTail c k u1) t1 t2).
+      Intros; Inversion H0; Clear H0; XAuto.
       NewInduction i.
-(* case 1 : pr2_delta i = 0 *)
-      DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
-      Rewrite H5 in H; Clear H5 u2.
+(* case 1 : pr2_delta i = 0 *) 
+      DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
+      Rewrite H7 in H; Clear H7 u2.
       Pr0Subst0; XEAuto.
 (* case 2 : pr2_delta i > 0 *)
       NewInduction k; DropGenBase; XEAuto.
       Qed.
 
-      Theorem pr3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u1 u2) ->
-                              (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
-                              (pr3 (CTail c k u1) t1 t2).
+      Theorem pr3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u1 u2) ->
+                             (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+                             (pr3 (CTail c k u1) t1 t2).
       Intros until 1; Inversion H; Clear H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
       EApply pr3_pr0_pr2_t; [ Apply H0 | XAuto ].
 (* case 2 : pr2_delta *)
-      Inversion H; [ XAuto | NewInduction i0 ].
+      Inversion H; [ XAuto | NewInduction i0 ]. 
 (* case 2.1 : i0 = 0 *)
-      DropGenBase; Inversion H2; Clear H2.
-      Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
-      Subst0Subst0; Arith9'In H4 i. (*; XDEAuto 7.
+      DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
+      Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
+      Subst0Subst0; Arith9'In H4 i; Clear H2 H H6 u2.
+      Pr0Subst0; Apply pr3_sing with t2:=x0; XEAuto.
 (* case 2.2 : i0 > 0 *)
       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
       Qed.
 
-      Theorem pr3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
-                              (pr3 (CTail c k u2) t1 t2) ->
-                              (u1:?) (pr2 c u1 u2) ->
-                              (pr3 (CTail c k u1) t1 t2).
+      Theorem pr3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
+                             (pr3 (CTail c k u2) t1 t2) ->
+                             (u1:?) (pr2 c u1 u2) ->
+                             (pr3 (CTail c k u1) t1 t2).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
       EApply pr3_t.
       EApply pr3_pr2_pr2_t; [ Apply H2 | Apply H ].
       XAuto.
       Qed.
 
-(*#* #start file *)
-
 (*#* #caption "reduction inside context items" *)
 (*#* #cap #cap t1, t2 #alpha c in E, u1 in V1, u2 in V2, k in z *)
 
-      Theorem pr3_pr3_pr3_t : (c:?; u1,u2:?) (pr3 c u1 u2) ->
-                              (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) ->
-                              (pr3 (CTail c k u1) t1 t2).
-
-(*#* #stop file *)
-
+      Theorem pr3_pr3_pr3_t: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                             (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) ->
+                             (pr3 (CTail c k u1) t1 t2).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
       EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ].
       Qed.
 
@@ -76,34 +73,29 @@ Require pr3_defs.
       Tactic Definition Pr3Context :=
          Match Context With
             | [ H1: (pr0 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
-               LApply (pr3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
+               LApply (pr3_pr0_pr2_t ?2 ?3); [ Intros H_x | XAuto ];
+               LApply (H_x ?1 ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
             | [ H1: (pr0 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
                LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
-               LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
+               LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
-               LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
+               LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
+               LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
                LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
-               LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
+               LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
             | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
-               LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ].
+               LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
+               LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ].
 
    Section pr3_lift. (*******************************************************)
 
-(*#* #start file *)
-
 (*#* #caption "conguence with lift" *)
 (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
 
-      Theorem pr3_lift : (c,e:?; h,d:?) (drop h d c e) ->
-                         (t1,t2:?) (pr3 e t1 t2) ->
-                         (pr3 c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
+      Theorem pr3_lift: (c,e:?; h,d:?) (drop h d c e) ->
+                        (t1,t2:?) (pr3 e t1 t2) ->
+                        (pr3 c (lift h d t1) (lift h d t2)).
       Intros until 2; XElim H0; Intros; XEAuto.
       Qed.
 
@@ -111,4 +103,25 @@ Require pr3_defs.
 
       Hints Resolve pr3_lift : ltlc.
 
-*)
+   Section pr3_cpr0. (*******************************************************)
+
+      Theorem pr3_cpr0_t: (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
+                          (pr3 c2 t1 t2).
+      Intros until 1; XElim H; Intros.
+(* case 1 : cpr0_refl *)
+      XAuto.
+(* case 2 : cpr0_comp *)
+      Pr3Context; Clear H1.
+      XElim H2; Intros.
+(* case 2.1 : pr3_refl *)
+      XAuto.
+(* case 2.2 : pr3_sing *)
+      EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
+      Inversion_clear H1.
+(* case 2.2.1 : pr2_free *)
+      XAuto.
+(* case 2.2.1 : pr2_delta *)
+      Cpr0Drop; Pr0Subst0; Apply pr3_sing with t2:=x; XEAuto.
+      Qed.
+
+   End pr3_cpr0.