we restored the scripts of \lambda\delta version 1

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / contexts_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
deleted file mode 100644 (file)
index a9a6892..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v
+++ /dev/null
@@ -1,77 +0,0 @@
-(*#* #stop file *)
-
-Require Export terms_defs.
-
-      Inductive Set C := CSort: nat -> C
-                      |  CTail: C -> K -> T -> C.
-
-      Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
-
-      Tactic Definition CGenBase :=
-         Match Context With
-            | [ H: (CSort ?) = (CSort ?) |- ? ]         -> Inversion H; Clear H
-            | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
-           | _                                         -> TGenBase.
-
-      Definition r: K -> nat -> nat := [k;i] Cases k of
-         | (Bind _) => i
-         | (Flat _) => (S i)
-      end.
-
-      Fixpoint app [c:C] : nat -> T -> T := [j;t]Cases j c of
-         | (0)   _             => t
-         | _     (CSort _)     => t
-         | (S i) (CTail c k u) => (app c (r k i) (TTail k u t))
-      end.
-
-   Section r_props. (********************************************************)
-
-      Theorem r_S: (k:?; i:?) (r k (S i)) = (S (r k i)).
-      XElim k; XAuto.
-      Qed.
-
-      Theorem r_plus_sym: (k:?; i,j:?) (r k (plus i j)) = (plus i (r k j)).
-      XElim k; Intros; Simpl; XAuto.
-      Qed.
-
-      Theorem r_minus: (i,n:?) (lt n i) ->
-                       (k:?) (minus (r k i) (S n)) = (r k (minus i (S n))).
-      XElim k; Intros; Simpl; XEAuto.
-      Qed.
-
-      Theorem r_dis: (k:?; P:Prop)
-                     (((i:?) (r k i) = i) -> P) ->
-                     (((i:?) (r k i) = (S i)) -> P) -> P.
-      XElim k; XAuto.
-      Qed.
-
-   End r_props.
-
-      Tactic Definition RRw :=
-         Repeat (Rewrite r_S Orelse Rewrite r_plus_sym).
-
-   Section r_arith. (********************************************************)
-
-      Theorem r_arith0: (k:?; i:?) (minus (r k (S i)) (1)) = (r k i).
-      Intros; RRw; Rewrite minus_Sx_SO; XAuto.
-      Qed.
-
-      Theorem r_arith1: (k:?; i,j:?) (minus (r k (S i)) (S j)) = (minus (r k i) j).
-      Intros; RRw; XAuto.
-      Qed.
-
-   End r_arith.
-
-   Section app_props. (******************************************************)
-
-      Theorem app_csort: (t:?; i,n:?) (app (CSort n) i t) = t.
-      XElim i; Intros; Simpl; XAuto.
-      Qed.
-
-      Theorem app_O: (c:?; t:?) (app c (0) t) = t.
-      XElim c; XAuto.
-      Qed.
-
-   End app_props.
-
-      Hints Resolve app_csort app_O : ltlc.