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

   1 (*#* #stop file *)
   2
   3 Require Export terms_defs.
   4
   5       Inductive Set C := CSort: nat -> C
   6                       |  CTail: C -> K -> T -> C.
   7
   8       Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
   9
  10       Tactic Definition CGenBase :=
  11          Match Context With
  12             | [ H: (CSort ?) = (CSort ?) |- ? ]         -> Inversion H; Clear H
  13             | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
  14             | _                                         -> TGenBase.
  15
  16       Definition r: K -> nat -> nat := [k;i] Cases k of
  17          | (Bind _) => i
  18          | (Flat _) => (S i)
  19       end.
  20
  21       Fixpoint app [c:C] : nat -> T -> T := [j;t]Cases j c of
  22          | (0)   _             => t
  23          | _     (CSort _)     => t
  24          | (S i) (CTail c k u) => (app c (r k i) (TTail k u t))
  25       end.
  26
  27    Section r_props. (********************************************************)
  28
  29       Theorem r_S: (k:?; i:?) (r k (S i)) = (S (r k i)).
  30       XElim k; XAuto.
  31       Qed.
  32
  33       Theorem r_plus_sym: (k:?; i,j:?) (r k (plus i j)) = (plus i (r k j)).
  34       XElim k; Intros; Simpl; XAuto.
  35       Qed.
  36
  37       Theorem r_minus: (i,n:?) (lt n i) ->
  38                        (k:?) (minus (r k i) (S n)) = (r k (minus i (S n))).
  39       XElim k; Intros; Simpl; XEAuto.
  40       Qed.
  41
  42       Theorem r_dis: (k:?; P:Prop)
  43                      (((i:?) (r k i) = i) -> P) ->
  44                      (((i:?) (r k i) = (S i)) -> P) -> P.
  45       XElim k; XAuto.
  46       Qed.
  47
  48    End r_props.
  49
  50       Tactic Definition RRw :=
  51          Repeat (Rewrite r_S Orelse Rewrite r_plus_sym).
  52
  53    Section r_arith. (********************************************************)
  54
  55       Theorem r_arith0: (k:?; i:?) (minus (r k (S i)) (1)) = (r k i).
  56       Intros; RRw; Rewrite minus_Sx_SO; XAuto.
  57       Qed.
  58
  59       Theorem r_arith1: (k:?; i,j:?) (minus (r k (S i)) (S j)) = (minus (r k i) j).
  60       Intros; RRw; XAuto.
  61       Qed.
  62
  63    End r_arith.
  64
  65    Section app_props. (******************************************************)
  66
  67       Theorem app_csort: (t:?; i,n:?) (app (CSort n) i t) = t.
  68       XElim i; Intros; Simpl; XAuto.
  69       Qed.
  70
  71       Theorem app_O: (c:?; t:?) (app c (0) t) = t.
  72       XElim c; XAuto.
  73       Qed.
  74
  75    End app_props.
  76
  77       Hints Resolve app_csort app_O : ltlc.