+++ /dev/null
-(*#* #stop file *)
-
-Require Export Base.
-
- Inductive Set B := Abbr: B
- | Abst: B
- | Void: B.
-
- Inductive Set F := Appl: F
- | Cast: F.
-
- Inductive Set K := Bind: B -> K
- | Flat: F -> K.
-
- Inductive Set T := TSort: nat -> T
- | TLRef: nat -> T
- | TTail: K -> T -> T -> T.
-
- Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
-
- Tactic Definition TGenBase :=
- Match Context With
- | [ H: (TSort ?) = (TSort ?) |- ? ] -> Inversion H; Clear H
- | [ H: (TLRef ?) = (TLRef ?) |- ? ] -> Inversion H; Clear H
- | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
- | _ -> Idtac.
-
- Definition s: K -> nat -> nat := [k;i] Cases k of
- | (Bind _) => (S i)
- | (Flat _) => i
- end.
-
- Section s_props. (********************************************************)
-
- Theorem s_S: (k:?; i:?) (s k (S i)) = (S (s k i)).
- XElim k; XAuto.
- Qed.
-
- Theorem s_plus: (k:?; i,j:?) (s k (plus i j)) = (plus (s k i) j).
- XElim k; XAuto.
- Qed.
-
- Theorem s_plus_sym: (k:?; i,j:?) (s k (plus i j)) = (plus i (s k j)).
- XElim k; [ Intros; Simpl; Rewrite plus_n_Sm | Idtac ]; XAuto.
- Qed.
-
- Theorem s_minus: (k:?; i,j:?) (le j i) ->
- (s k (minus i j)) = (minus (s k i) j).
- XElim k; [ Intros; Unfold s; Cbv Iota | XAuto ].
- Rewrite minus_Sn_m; XAuto.
- Qed.
-
- Theorem minus_s_s: (k:?; i,j:?) (minus (s k i) (s k j)) = (minus i j).
- XElim k; XAuto.
- Qed.
-
- Theorem s_le: (k:?; i,j:?) (le i j) -> (le (s k i) (s k j)).
- XElim k; Simpl; XAuto.
- Qed.
-
- Theorem s_lt: (k:?; i,j:?) (lt i j) -> (lt (s k i) (s k j)).
- XElim k; Simpl; XAuto.
- Qed.
-
- Theorem s_inj: (k:?; i,j:?) (s k i) = (s k j) -> i = j.
- XElim k; XEAuto.
- Qed.
-
- End s_props.
-
- Hints Resolve s_le s_lt s_inj : ltlc.
-
- Tactic Definition SRw :=
- Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).
-
- Tactic Definition SRwIn H :=
- Repeat (Rewrite s_S in H Orelse Rewrite s_plus in H).
-
- Tactic Definition SRwBack :=
- Repeat (Rewrite <- s_S Orelse Rewrite <- s_plus Orelse Rewrite <- s_plus_sym).
-
- Tactic Definition SRwBackIn H :=
- Repeat (Rewrite <- s_S in H Orelse Rewrite <- s_plus in H Orelse Rewrite <- s_plus_sym in H).
-
- Hint discr : ltlc := Extern 4 (le ? (plus (s ? ?) ?)) SRwBack.