contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
new file mode 100644 (file)
index 0000000..157cb74
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v
@@ -0,0 +1,78 @@
+(*#* #stop file *)
+
+Require Export Base.
+
+      Inductive Set B := Abbr : B
+                      |  Abst : B
+                      |  Void : B.
+
+      Inductive Set F := Appl : F
+                      |  Cast : F.
+
+      Inductive Set K := Bind : B -> K
+                      |  Flat : F -> K.
+
+      Inductive Set T := TSort : nat -> T
+                      |  TBRef : nat -> T
+                      |  TTail : K -> T -> T -> T.
+
+      Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
+
+      Definition s: K -> nat -> nat := [k;i] Cases k of
+         | (Bind _) => (S i)
+         | (Flat _) => i
+      end.
+
+   Section s_props. (********************************************************)
+
+      Theorem s_S: (k:?; i:?) (s k (S i)) = (S (s k i)).
+      XElim k; XAuto.
+      Qed.
+
+      Theorem s_plus: (k:?; i,j:?) (s k (plus i j)) = (plus (s k i) j).
+      XElim k; XAuto.
+      Qed.
+
+      Theorem s_plus_sym: (k:?; i,j:?) (s k (plus i j)) = (plus i (s k j)).
+      XElim k; [ Intros; Simpl; Rewrite plus_n_Sm | Idtac ]; XAuto.
+      Qed.
+
+      Theorem s_minus: (k:?; i,j:?) (le j i) ->
+                       (s k (minus i j)) = (minus (s k i) j).
+      XElim k; [ Intros; Unfold s; Cbv Iota | XAuto ].
+      Rewrite minus_Sn_m; XAuto.
+      Qed.
+
+      Theorem minus_s_s: (k:?; i,j:?) (minus (s k i) (s k j)) = (minus i j).
+      XElim k; XAuto.
+      Qed.
+
+      Theorem s_le: (k:?; i,j:?) (le i j) -> (le (s k i) (s k j)).
+      XElim k; Simpl; XAuto.
+      Qed.
+
+      Theorem s_lt: (k:?; i,j:?) (lt i j) -> (lt (s k i) (s k j)).
+      XElim k; Simpl; XAuto.
+      Qed.
+
+      Theorem s_inj: (k:?; i,j:?) (s k i) = (s k j) -> i = j.
+      XElim k; XEAuto.
+      Qed.
+
+   End s_props.
+
+      Hints Resolve s_le s_lt s_inj.
+
+      Tactic Definition SRw :=
+         Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).
+
+      Tactic Definition SRwIn H :=
+         Repeat (Rewrite s_S in H Orelse Rewrite s_plus in H).
+
+      Tactic Definition SRwBack :=
+         Repeat (Rewrite <- s_S Orelse Rewrite <- s_plus Orelse Rewrite <- s_plus_sym).
+
+      Tactic Definition SRwBackIn H :=
+         Repeat (Rewrite <- s_S in H Orelse Rewrite <- s_plus in H Orelse Rewrite <- s_plus_sym in H).
+
+      Hint discr : ltlc := Extern 4 (le ? (plus (s ? ?) ?)) SRwBack.