X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Flift_defs.v;h=8b69ec4b49c62cb3c639e182bd8c8c3990b8f20a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=3185aad6fb79c0a0edea8cac24edc4269edccac3;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
index 3185aad6f..8b69ec4b4 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
@@ -2,16 +2,16 @@
 
 Require Export terms_defs.
 
-      Fixpoint bref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
+      Fixpoint lref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
          | (TSort n)     => (TSort n)
-         | (TBRef n)     =>
-            if (blt n d) then (TBRef n) else (TBRef (g n))
+         | (TLRef n)     =>
+            if (blt n d) then (TLRef n) else (TLRef (g n))
          | (TTail k u t) =>
-            (TTail k (bref_map g d u) (bref_map g (s k d) t))
+            (TTail k (lref_map g d u) (lref_map g (s k d) t))
       end.
 
       Definition lift : nat -> nat -> T -> T :=
-                        [h](bref_map [x](plus x h)).
+                        [h](lref_map [x](plus x h)).
 
    Section lift_rw. (********************************************************)
 
@@ -19,14 +19,14 @@ Require Export terms_defs.
       XAuto.
       Qed.
 
-      Theorem lift_bref_lt: (n:?; h,d:?) (lt n d) ->
-                            (lift h d (TBRef n)) = (TBRef n).
+      Theorem lift_lref_lt: (n:?; h,d:?) (lt n d) ->
+                            (lift h d (TLRef n)) = (TLRef n).
       Intros; Unfold lift; Simpl.
       Replace (blt n d) with true; XAuto.
       Qed.
 
-      Theorem lift_bref_ge: (n:?; h,d:?) (le d n) ->
-                            (lift h d (TBRef n)) = (TBRef (plus n h)).
+      Theorem lift_lref_ge: (n:?; h,d:?) (le d n) ->
+                            (lift h d (TLRef n)) = (TLRef (plus n h)).
 
       Intros; Unfold lift; Simpl.
       Replace (blt n d) with false; XAuto.
@@ -52,7 +52,7 @@ Require Export terms_defs.
 
    End lift_rw.
 
-      Hints Resolve lift_bref_lt lift_bind lift_flat : ltlc.
+      Hints Resolve lift_lref_lt lift_bind lift_flat : ltlc.
 
       Tactic Definition LiftTailRw :=
          Repeat (Rewrite lift_tail Orelse Rewrite lift_bind Orelse Rewrite lift_flat).
@@ -67,68 +67,68 @@ Require Export terms_defs.
       XElim t; Intros.
 (* case 1 : TSort *)
       XAuto.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
       Apply (lt_le_e n0 d); Intros.
 (* case 2.1 : n0 < d *)
-      Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+      Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
 (* case 2.2 : n0 >= d *)
-      Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+      Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
 (* case 3 : TTail k *)
       Rewrite lift_tail in H1; Inversion H1.
       Qed.
 
-      Theorem lift_gen_bref_lt: (h,d,n:?) (lt n d) ->
-                                (t:?) (TBRef n) = (lift h d t) ->
-                                t = (TBRef n).
+      Theorem lift_gen_lref_lt: (h,d,n:?) (lt n d) ->
+                                (t:?) (TLRef n) = (lift h d t) ->
+                                t = (TLRef n).
       XElim t; Intros.
 (* case 1 : TSort *)
       XAuto.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
       Apply (lt_le_e n0 d); Intros.
 (* case 2.1 : n0 < d *)
-      Rewrite lift_bref_lt in H0; XAuto.
+      Rewrite lift_lref_lt in H0; XAuto.
 (* case 2.2 : n0 >= d *)
-      Rewrite lift_bref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
+      Rewrite lift_lref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
       Rewrite H3 in H; Clear H3 n.
       EApply le_false; [ Apply H1 | XEAuto ].
 (* case 3 : TTail k *)
       Rewrite lift_tail in H2; Inversion H2.
       Qed.
 
-      Theorem lift_gen_bref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
-                                   (t:?) (TBRef n) = (lift h d t) ->
+      Theorem lift_gen_lref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
+                                   (t:?) (TLRef n) = (lift h d t) ->
                                     (P:Prop) P.
       XElim t; Intros.
 (* case 1 : TSort *)
       Inversion H1.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
       Apply (lt_le_e n0 d); Intros.
 (* case 2.1 : n0 < d *)
-      Rewrite lift_bref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
+      Rewrite lift_lref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
       Rewrite <- H4 in H2; Clear H4 n0.
       EApply le_false; [ Apply H | XEAuto ].
 (* case 2.2 : n0 >= d *)
-      Rewrite lift_bref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
+      Rewrite lift_lref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
       Rewrite H4 in H0; Clear H4.
       EApply le_false; [ Apply H2 | XEAuto ].
 (* case 3 : TTail k *)
       Rewrite lift_tail in H3; Inversion H3.
       Qed.
 
-      Theorem lift_gen_bref_ge: (h,d,n:?) (le d n) ->
-                                (t:?) (TBRef (plus n h)) = (lift h d t) ->
-                                t = (TBRef n).
+      Theorem lift_gen_lref_ge: (h,d,n:?) (le d n) ->
+                                (t:?) (TLRef (plus n h)) = (lift h d t) ->
+                                t = (TLRef n).
       XElim t; Intros.
 (* case 1 : TSort *)
       Inversion H0.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
       Apply (lt_le_e n0 d); Intros.
 (* case 2.1 : n0 < d *)
-      Rewrite lift_bref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
+      Rewrite lift_lref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
       Rewrite <- H3 in H1; Clear H3 n0.
       EApply le_false; [ Apply H | XEAuto ].
 (* case 2.2 : n0 >= d *)
-      Rewrite lift_bref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
+      Rewrite lift_lref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
 (* case 3 : TTail k *)
       Rewrite lift_tail in H2; Inversion H2.
       Qed.
@@ -143,12 +143,12 @@ Require Export terms_defs.
       XElim x; Intros.
 (* case 1 : TSort *)
       Inversion H.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1 : n < d *)
-      Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+      Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
 (* case 2.2 : n >= d *)
-      Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+      Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
 (* case 3 : TTail k *)
       Rewrite lift_tail in H1; Inversion H1.
       XEAuto.
@@ -163,12 +163,12 @@ Require Export terms_defs.
       XElim x; Intros.
 (* case 1 : TSort *)
       Inversion H.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1 : n < d *)
-      Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+      Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
 (* case 2.2 : n >= d *)
-      Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+      Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
 (* case 3 : TTail k *)
       Rewrite lift_tail in H1; Inversion H1.
       XEAuto.
@@ -181,22 +181,24 @@ Require Export terms_defs.
             | [ H: (TSort ?0) = (lift ?1 ?2 ?3) |- ? ] ->
                LApply (lift_gen_sort ?1 ?2 ?0 ?3); [ Clear H; Intros | XAuto ]
             | [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
-                H3: (TBRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
-               Apply (lift_gen_bref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
-            | [ H: (TBRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
-               LApply (lift_gen_bref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
+                H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
+               Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
+            | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] ->
+	       EApply lift_gen_lref_false; [ Idtac | Idtac | XEAuto ]; XEAuto
+	    | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
+               LApply (lift_gen_lref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
                LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
                LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
                Apply H_x
-            | [ H: (TBRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
-               LApply (lift_gen_bref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
+            | [ H: (TLRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
+               LApply (lift_gen_lref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
                LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
-            | [ H1: (TBRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
-               LApply (lift_gen_bref_lt ?1 ?2 ?0);
+            | [ H1: (TLRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
+               LApply (lift_gen_lref_lt ?1 ?2 ?0);
                [ Intros H_x | Apply lt_le_trans with m:=?4; XEAuto ];
                LApply (H_x ?3); [ Clear H_x H1; Intros | XAuto ]
-            | [ H: (TBRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
-               LApply (lift_gen_bref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
+            | [ H: (TLRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
+               LApply (lift_gen_lref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
                LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
             | [ H: (TTail (Bind ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
                LApply (lift_gen_bind ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
@@ -211,20 +213,20 @@ Require Export terms_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt; XAuto.
+      Rewrite lift_lref_lt; XAuto.
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge; XAuto.
+      Rewrite lift_lref_ge; XAuto.
 (* case 3: TTail *)
       LiftTailRw; XAuto.
       Qed.
 
-      Theorem lift_bref_gt : (d,n:?) (lt d n) ->
-                             (lift (1) d (TBRef (pred n))) = (TBRef n).
+      Theorem lift_lref_gt : (d,n:?) (lt d n) ->
+                             (lift (1) d (TLRef (pred n))) = (TLRef n).
       Intros.
-      Rewrite lift_bref_ge.
+      Rewrite lift_lref_ge.
 (* case 1: first branch *)
       Rewrite <- plus_sym; Simpl; Rewrite <- (S_pred n d); XAuto.
 (* case 2: second branch *)
@@ -233,4 +235,4 @@ Require Export terms_defs.
 
    End lift_props.
 
-      Hints Resolve lift_r lift_bref_gt : ltlc.
+      Hints Resolve lift_r lift_lref_gt : ltlc.