contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v
new file mode 100644 (file)
index 0000000..689477a
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v
@@ -0,0 +1,115 @@
+(*#* #stop file *)
+
+Require Export terms_defs.
+
+      Definition wadd : (nat -> nat) -> nat -> (nat -> nat) :=
+         [f;w;n] Cases n of (0) => w | (S m) => (f m) end.
+
+      Fixpoint weight_map [f:nat->nat; t:T] : nat := Cases t of
+         | (TSort n)               => (0)
+         | (TBRef n)               => (f n)
+         | (TTail (Bind Abbr) u t) =>
+            (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f u))) t)))
+         | (TTail (Bind _) u t)    =>
+            (S (plus (weight_map f u) (weight_map (wadd f (0)) t)))
+         | (TTail _ u t)           => (S (plus (weight_map f u) (weight_map f t)))
+      end.
+
+      Definition weight : T -> nat := (weight_map [_](0)).
+
+      Definition tlt : T -> T -> Prop := [t1,t2](lt (weight t1) (weight t2)).
+
+   Section wadd_props. (*****************************************************)
+
+      Theorem wadd_le: (f,g:?) ((n:?) (le (f n) (g n))) -> (v,w:?) (le v w) ->
+                       (n:?) (le (wadd f v n) (wadd g w n)).
+      XElim n; Simpl; XAuto.
+      Qed.
+
+      Theorem wadd_lt: (f,g:?) ((n:?) (le (f n) (g n))) -> (v,w:?) (lt v w) ->
+                       (n:?) (le (wadd f v n) (wadd g w n)).
+      XElim n; Simpl; XAuto.
+      Qed.
+
+      Theorem wadd_O: (n:?) (wadd [_](0) (0) n) = (0).
+      XElim n; XAuto.
+      Qed.
+
+   End wadd_props.
+
+      Hints Resolve wadd_le wadd_lt wadd_O : ltlc.
+
+   Section weight_props. (***************************************************)
+
+      Theorem weight_le : (t:?; f,g:?) ((n:?) (le (f n) (g n))) ->
+                          (le (weight_map f t) (weight_map g t)).
+      XElim t; [ XAuto | Simpl; XAuto | Idtac ].
+      XElim k; Simpl; [ Idtac | XAuto ].
+      XElim b; Auto 7 with ltlc. (**)
+      Qed.
+
+      Theorem weight_eq : (t:?; f,g:?) ((n:?) (f n) = (g n)) ->
+                          (weight_map f t) = (weight_map g t).
+      Intros; Apply le_antisym; Apply weight_le;
+      Intros; Rewrite (H n); XAuto.
+      Qed.
+
+      Hints Resolve weight_le weight_eq : ltlc.
+
+      Theorem weight_add_O : (t:?) (weight_map (wadd [_](0) (0)) t) = (weight_map [_](0) t).
+      XAuto.
+      Qed.
+
+      Theorem weight_add_S : (t:?; m:?) (le (weight_map (wadd [_](0) (0)) t) (weight_map (wadd  [_](0) (S m)) t)).
+      XAuto.
+      Qed.
+
+   End weight_props.
+
+      Hints Resolve weight_le weight_add_S : ltlc.
+
+   Section tlt_props. (******************************************************)
+
+      Theorem tlt_trans: (v,u,t:?) (tlt u v) -> (tlt v t) -> (tlt u t).
+      Unfold tlt; XEAuto.
+      Qed.
+
+      Theorem tlt_tail_sx: (k:?; u,t:?) (tlt u (TTail k u t)).
+      Unfold tlt weight.
+      XElim k; Simpl; [ XElim b | Idtac ]; XAuto.
+      Qed.
+
+      Theorem tlt_tail_dx: (k:?; u,t:?) (tlt t (TTail k u t)).
+      Unfold tlt weight.
+      XElim k; Simpl; [ Idtac | XAuto ].
+      XElim b; Intros; Try Rewrite weight_add_O; [ Idtac | XAuto | XAuto ].
+      EApply lt_le_trans; [ Apply lt_n_Sn | Apply le_n_S ].
+      EApply le_trans; [ Rewrite <- (weight_add_O t); Apply weight_add_S | XAuto ].
+      Qed.
+
+   End tlt_props.
+
+      Hints Resolve tlt_tail_sx tlt_tail_dx tlt_trans : ltlc.
+
+   Section tlt_wf. (*********************************************************)
+
+      Local Q: (T -> Prop) -> nat -> Prop :=
+         [P;n] (t:?) (weight t) = n -> (P t).
+
+      Remark q_ind: (P:T->Prop)((n:?) (Q P n)) -> (t:?) (P t).
+      Unfold Q; Intros.
+      Apply (H (weight t) t); XAuto.
+      Qed.
+
+      Theorem tlt_wf_ind: (P:T->Prop)
+                          ((t:?)((v:?)(tlt v t) -> (P v)) -> (P t)) ->
+                          (t:?)(P t).
+      Unfold tlt; Intros.
+      XElimUsing q_ind t; Intros.
+      Apply lt_wf_ind; Clear n; Intros.
+      Unfold Q in H0; Unfold Q; Intros.
+      Rewrite <- H1 in H0; Clear H1.
+      Apply H; XEAuto.
+      Qed.
+
+   End tlt_wf.