3 Require Export terms_defs.
5 Inductive Set C := CSort: nat -> C
6 | CTail: C -> K -> T -> C.
8 Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
10 Tactic Definition CGenBase :=
12 | [ H: (CSort ?) = (CSort ?) |- ? ] -> Inversion H; Clear H
13 | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
16 Definition r: K -> nat -> nat := [k;i] Cases k of
21 Fixpoint app [c:C] : nat -> T -> T := [j;t]Cases j c of
24 | (S i) (CTail c k u) => (app c (r k i) (TTail k u t))
27 Section r_props. (********************************************************)
29 Theorem r_S: (k:?; i:?) (r k (S i)) = (S (r k i)).
33 Theorem r_plus_sym: (k:?; i,j:?) (r k (plus i j)) = (plus i (r k j)).
34 XElim k; Intros; Simpl; XAuto.
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.
42 Theorem r_dis: (k:?; P:Prop)
43 (((i:?) (r k i) = i) -> P) ->
44 (((i:?) (r k i) = (S i)) -> P) -> P.
50 Tactic Definition RRw :=
51 Repeat (Rewrite r_S Orelse Rewrite r_plus_sym).
53 Section r_arith. (********************************************************)
55 Theorem r_arith0: (k:?; i:?) (minus (r k (S i)) (1)) = (r k i).
56 Intros; RRw; Rewrite minus_Sx_SO; XAuto.
59 Theorem r_arith1: (k:?; i,j:?) (minus (r k (S i)) (S j)) = (minus (r k i) j).
65 Section app_props. (******************************************************)
67 Theorem app_csort: (t:?; i,n:?) (app (CSort n) i t) = t.
68 XElim i; Intros; Simpl; XAuto.
71 Theorem app_O: (c:?; t:?) (app c (0) t) = t.
77 Hints Resolve app_csort app_O : ltlc.