5 Inductive Set B := Abbr : B
9 Inductive Set F := Appl : F
12 Inductive Set K := Bind : B -> K
15 Inductive Set T := TSort : nat -> T
17 | TTail : K -> T -> T -> T.
19 Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
21 Tactic Definition TGenBase :=
23 | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
26 Definition s: K -> nat -> nat := [k;i] Cases k of
31 Section s_props. (********************************************************)
33 Theorem s_S: (k:?; i:?) (s k (S i)) = (S (s k i)).
37 Theorem s_plus: (k:?; i,j:?) (s k (plus i j)) = (plus (s k i) j).
41 Theorem s_plus_sym: (k:?; i,j:?) (s k (plus i j)) = (plus i (s k j)).
42 XElim k; [ Intros; Simpl; Rewrite plus_n_Sm | Idtac ]; XAuto.
45 Theorem s_minus: (k:?; i,j:?) (le j i) ->
46 (s k (minus i j)) = (minus (s k i) j).
47 XElim k; [ Intros; Unfold s; Cbv Iota | XAuto ].
48 Rewrite minus_Sn_m; XAuto.
51 Theorem minus_s_s: (k:?; i,j:?) (minus (s k i) (s k j)) = (minus i j).
55 Theorem s_le: (k:?; i,j:?) (le i j) -> (le (s k i) (s k j)).
56 XElim k; Simpl; XAuto.
59 Theorem s_lt: (k:?; i,j:?) (lt i j) -> (lt (s k i) (s k j)).
60 XElim k; Simpl; XAuto.
63 Theorem s_inj: (k:?; i,j:?) (s k i) = (s k j) -> i = j.
69 Hints Resolve s_le s_lt s_inj.
71 Tactic Definition SRw :=
72 Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).
74 Tactic Definition SRwIn H :=
75 Repeat (Rewrite s_S in H Orelse Rewrite s_plus in H).
77 Tactic Definition SRwBack :=
78 Repeat (Rewrite <- s_S Orelse Rewrite <- s_plus Orelse Rewrite <- s_plus_sym).
80 Tactic Definition SRwBackIn H :=
81 Repeat (Rewrite <- s_S in H Orelse Rewrite <- s_plus in H Orelse Rewrite <- s_plus_sym in H).
83 Hint discr : ltlc := Extern 4 (le ? (plus (s ? ?) ?)) SRwBack.