X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fdrop_defs.v;h=ee7eea93cd691702e3ec0942365d6c12de44aea9;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=e1576c50481bc9555557f4ce659168cf3174c84b;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v b/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v
index e1576c504..ee7eea93c 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v
@@ -1,16 +1,22 @@
-(*#* #stop file *)
-
 Require Export contexts_defs.
 Require Export lift_defs.
 
-      Inductive drop : nat -> nat -> C -> C -> Prop :=
-         | drop_sort : (h,d,n:?) (drop h d (CSort n) (CSort n))
-         | drop_tail : (c,e:?) (drop (0) (0) c e) ->
-                       (k:?; u:?) (drop (0) (0) (CTail c k u) (CTail e k u))
-         | drop_drop : (k:?; h:?; c,e:?) (drop (r k h) (0) c e) ->
-                       (u:?) (drop (S h) (0) (CTail c k u) e)
-         | drop_skip : (k:?; h,d:?; c,e:?) (drop h (r k d) c e) -> (u:?)
-                       (drop h (S d) (CTail c k (lift h (r k d) u)) (CTail e k u)).
+(*#* #caption "current axioms for dropping",
+   "base case", "untouched tail item", 
+   "dropped tail item", "updated tail item"
+*)
+(*#* #cap #alpha c in C1, e in C2, u in V, k in z, n in k, d in i, r in q *)
+
+      Inductive drop: nat -> nat -> C -> C -> Prop :=
+         | drop_sort: (h,d,n:?) (drop h d (CSort n) (CSort n))
+         | drop_comp: (c,e:?) (drop (0) (0) c e) ->
+                      (k:?; u:?) (drop (0) (0) (CTail c k u) (CTail e k u))
+         | drop_drop: (k:?; h:?; c,e:?) (drop (r k h) (0) c e) ->
+                      (u:?) (drop (S h) (0) (CTail c k u) e)
+         | drop_skip: (k:?; h,d:?; c,e:?) (drop h (r k d) c e) -> (u:?)
+                      (drop h (S d) (CTail c k (lift h (r k d) u)) (CTail e k u)).
+
+(*#* #stop file *)
 
       Hint drop : ltlc := Constructors drop.
 
@@ -18,53 +24,53 @@ Require Export lift_defs.
 
    Section drop_gen_base. (**************************************************)
 
-      Theorem drop_gen_sort : (n,h,d:?; x:?)
-                              (drop h d (CSort n) x) -> x = (CSort n).
+      Theorem drop_gen_sort: (n,h,d:?; x:?)
+                             (drop h d (CSort n) x) -> x = (CSort n).
       Intros until 1; InsertEq H '(CSort n); XElim H; Intros;
       Try Inversion H1; XAuto.
       Qed.
 
-      Theorem drop_gen_refl : (x,e:?) (drop (0) (0) x e) -> x = e.
+      Theorem drop_gen_refl: (x,e:?) (drop (0) (0) x e) -> x = e.
       Intros until 1; Repeat InsertEq H '(0); XElim H; Intros.
-(* case 1 : drop_sort *)
+(* case 1: drop_sort *)
       XAuto.
-(* case 2 : drop_tail *)
+(* case 2: drop_comp *)
       Rewrite H0; XAuto.
-(* case 3 : drop_drop *)
+(* case 3: drop_drop *)
       Inversion H2.
-(* case 4 : drop_skip *)
+(* case 4: drop_skip *)
       Inversion H1.
       Qed.
 
-      Theorem drop_gen_drop : (k:?; c,x:?; u:?; h:?)
-                              (drop (S h) (0) (CTail c k u) x) ->
-                              (drop (r k h) (0) c x).
+      Theorem drop_gen_drop: (k:?; c,x:?; u:?; h:?)
+                             (drop (S h) (0) (CTail c k u) x) ->
+                             (drop (r k h) (0) c x).
       Intros until 1;
       InsertEq H '(CTail c k u); InsertEq H '(0); InsertEq H '(S h);
       XElim H; Intros.
-(* case 1 : drop_sort *)
+(* case 1: drop_sort *)
       Inversion H1.
-(* case 2 : drop_tail *)
+(* case 2: drop_comp *)
       Inversion H1.
-(* case 3 : drop_drop *)
+(* case 3: drop_drop *)
       Inversion H1; Inversion H3.
       Rewrite <- H5; Rewrite <- H6; Rewrite <- H7; XAuto.
-(* case 4 : drop_skip *)
+(* case 4: drop_skip *)
       Inversion H2.
       Qed.
 
-      Theorem drop_gen_skip_r : (c,x:?; u:?; h,d:?; k:?)
-                                (drop h (S d) x (CTail c k u)) ->
-                                (EX e | x = (CTail e k (lift h (r k d) u)) & (drop h (r k d) e c)).
+      Theorem drop_gen_skip_r: (c,x:?; u:?; h,d:?; k:?)
+                               (drop h (S d) x (CTail c k u)) ->
+                               (EX e | x = (CTail e k (lift h (r k d) u)) & (drop h (r k d) e c)).
       Intros; Inversion_clear H; XEAuto.
       Qed.
 
-      Theorem drop_gen_skip_l : (c,x:?; u:?; h,d:?; k:?)
-                                (drop h (S d) (CTail c k u) x) ->
-                                (EX e v | x = (CTail e k v) &
-                                          u = (lift h (r k d) v) &
-                                          (drop h (r k d) c e)
-                                ).
+      Theorem drop_gen_skip_l: (c,x:?; u:?; h,d:?; k:?)
+                               (drop h (S d) (CTail c k u) x) ->
+                               (EX e v | x = (CTail e k v) &
+                                         u = (lift h (r k d) v) &
+                                         (drop h (r k d) c e)
+                               ).
       Intros; Inversion_clear H; XEAuto.
       Qed.
 
@@ -100,9 +106,9 @@ Require Export lift_defs.
 
       Hints Resolve drop_refl : ltlc.
 
-      Theorem drop_S : (b:?; c,e:?; u:?; h:?)
-                       (drop h (0) c (CTail e (Bind b) u)) ->
-                       (drop (S h) (0) c e).
+      Theorem drop_S: (b:?; c,e:?; u:?; h:?)
+                      (drop h (0) c (CTail e (Bind b) u)) ->
+                      (drop (S h) (0) c e).
       XElim c.
 (* case 1: CSort *)
       Intros; DropGenBase; Inversion H.
@@ -122,4 +128,3 @@ Require Export lift_defs.
          Match Context With
             [ _: (drop ?1 (0) ?2 (CTail ?3 (Bind ?4) ?5)) |- ? ] ->
                LApply (drop_S ?4 ?2 ?3 ?5 ?1); [ Intros | XAuto ].
-