helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v

   1 (*#* #stop file *)
   2
   3 Require Export terms_defs.
   4
   5       Definition wadd : (nat -> nat) -> nat -> (nat -> nat) :=
   6          [f;w;n] Cases n of (0) => w | (S m) => (f m) end.
   7
   8       Fixpoint weight_map [f:nat->nat; t:T] : nat := Cases t of
   9          | (TSort n)               => (0)
  10          | (TLRef n)               => (f n)
  11          | (TTail (Bind Abbr) u t) =>
  12             (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f u))) t)))
  13          | (TTail (Bind _) u t)    =>
  14             (S (plus (weight_map f u) (weight_map (wadd f (0)) t)))
  15          | (TTail _ u t)           => (S (plus (weight_map f u) (weight_map f t)))
  16       end.
  17
  18       Definition weight : T -> nat := (weight_map [_](0)).
  19
  20       Definition tlt : T -> T -> Prop := [t1,t2](lt (weight t1) (weight t2)).
  21
  22    Section wadd_props. (*****************************************************)
  23
  24       Theorem wadd_le: (f,g:?) ((n:?) (le (f n) (g n))) -> (v,w:?) (le v w) ->
  25                        (n:?) (le (wadd f v n) (wadd g w n)).
  26       XElim n; Simpl; XAuto.
  27       Qed.
  28
  29       Theorem wadd_lt: (f,g:?) ((n:?) (le (f n) (g n))) -> (v,w:?) (lt v w) ->
  30                        (n:?) (le (wadd f v n) (wadd g w n)).
  31       XElim n; Simpl; XAuto.
  32       Qed.
  33
  34       Theorem wadd_O: (n:?) (wadd [_](0) (0) n) = (0).
  35       XElim n; XAuto.
  36       Qed.
  37
  38    End wadd_props.
  39
  40       Hints Resolve wadd_le wadd_lt wadd_O : ltlc.
  41
  42    Section weight_props. (***************************************************)
  43
  44       Theorem weight_le : (t:?; f,g:?) ((n:?) (le (f n) (g n))) ->
  45                           (le (weight_map f t) (weight_map g t)).
  46       XElim t; [ XAuto | Simpl; XAuto | Idtac ].
  47       XElim k; Simpl; [ Idtac | XAuto ].
  48       XElim b; Auto 7 with ltlc. (**)
  49       Qed.
  50
  51       Theorem weight_eq : (t:?; f,g:?) ((n:?) (f n) = (g n)) ->
  52                           (weight_map f t) = (weight_map g t).
  53       Intros; Apply le_antisym; Apply weight_le;
  54       Intros; Rewrite (H n); XAuto.
  55       Qed.
  56
  57       Hints Resolve weight_le weight_eq : ltlc.
  58
  59       Theorem weight_add_O : (t:?) (weight_map (wadd [_](0) (0)) t) = (weight_map [_](0) t).
  60       XAuto.
  61       Qed.
  62
  63       Theorem weight_add_S : (t:?; m:?) (le (weight_map (wadd [_](0) (0)) t) (weight_map (wadd  [_](0) (S m)) t)).
  64       XAuto.
  65       Qed.
  66
  67    End weight_props.
  68
  69       Hints Resolve weight_le weight_add_S : ltlc.
  70
  71    Section tlt_props. (******************************************************)
  72
  73       Theorem tlt_trans: (v,u,t:?) (tlt u v) -> (tlt v t) -> (tlt u t).
  74       Unfold tlt; XEAuto.
  75       Qed.
  76
  77       Theorem tlt_tail_sx: (k:?; u,t:?) (tlt u (TTail k u t)).
  78       Unfold tlt weight.
  79       XElim k; Simpl; [ XElim b | Idtac ]; XAuto.
  80       Qed.
  81
  82       Theorem tlt_tail_dx: (k:?; u,t:?) (tlt t (TTail k u t)).
  83       Unfold tlt weight.
  84       XElim k; Simpl; [ Idtac | XAuto ].
  85       XElim b; Intros; Try Rewrite weight_add_O; [ Idtac | XAuto | XAuto ].
  86       EApply lt_le_trans; [ Apply lt_n_Sn | Apply le_n_S ].
  87       EApply le_trans; [ Rewrite <- (weight_add_O t); Apply weight_add_S | XAuto ].
  88       Qed.
  89
  90    End tlt_props.
  91
  92       Hints Resolve tlt_tail_sx tlt_tail_dx tlt_trans : ltlc.
  93
  94    Section tlt_wf. (*********************************************************)
  95
  96       Local Q: (T -> Prop) -> nat -> Prop :=
  97          [P;n] (t:?) (weight t) = n -> (P t).
  98
  99       Remark q_ind: (P:T->Prop)((n:?) (Q P n)) -> (t:?) (P t).
 100       Unfold Q; Intros.
 101       Apply (H (weight t) t); XAuto.
 102       Qed.
 103
 104       Theorem tlt_wf_ind: (P:T->Prop)
 105                           ((t:?)((v:?)(tlt v t) -> (P v)) -> (P t)) ->
 106                           (t:?)(P t).
 107       Unfold tlt; Intros.
 108       XElimUsing q_ind t; Intros.
 109       Apply lt_wf_ind; Clear n; Intros.
 110       Unfold Q in H0; Unfold Q; Intros.
 111       Rewrite <- H1 in H0; Clear H1.
 112       Apply H; XEAuto.
 113       Qed.
 114
 115    End tlt_wf.