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

   1 (*#* #stop file *)
   2
   3 Require Export Base.
   4
   5       Inductive Set B := Abbr: B
   6                       |  Abst: B
   7                       |  Void: B.
   8
   9       Inductive Set F := Appl: F
  10                       |  Cast: F.
  11
  12       Inductive Set K := Bind: B -> K
  13                       |  Flat: F -> K.
  14
  15       Inductive Set T := TSort: nat -> T
  16                       |  TLRef: nat -> T
  17                       |  TTail: K -> T -> T -> T.
  18
  19       Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
  20
  21       Tactic Definition TGenBase :=
  22          Match Context With
  23             | [ H: (TSort ?) = (TSort ?) |- ? ]         -> Inversion H; Clear H
  24             | [ H: (TLRef ?) = (TLRef ?) |- ? ]         -> Inversion H; Clear H
  25             | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
  26             | _                                         -> Idtac.
  27
  28       Definition s: K -> nat -> nat := [k;i] Cases k of
  29          | (Bind _) => (S i)
  30          | (Flat _) => i
  31       end.
  32
  33    Section s_props. (********************************************************)
  34
  35       Theorem s_S: (k:?; i:?) (s k (S i)) = (S (s k i)).
  36       XElim k; XAuto.
  37       Qed.
  38
  39       Theorem s_plus: (k:?; i,j:?) (s k (plus i j)) = (plus (s k i) j).
  40       XElim k; XAuto.
  41       Qed.
  42
  43       Theorem s_plus_sym: (k:?; i,j:?) (s k (plus i j)) = (plus i (s k j)).
  44       XElim k; [ Intros; Simpl; Rewrite plus_n_Sm | Idtac ]; XAuto.
  45       Qed.
  46
  47       Theorem s_minus: (k:?; i,j:?) (le j i) ->
  48                        (s k (minus i j)) = (minus (s k i) j).
  49       XElim k; [ Intros; Unfold s; Cbv Iota | XAuto ].
  50       Rewrite minus_Sn_m; XAuto.
  51       Qed.
  52
  53       Theorem minus_s_s: (k:?; i,j:?) (minus (s k i) (s k j)) = (minus i j).
  54       XElim k; XAuto.
  55       Qed.
  56
  57       Theorem s_le: (k:?; i,j:?) (le i j) -> (le (s k i) (s k j)).
  58       XElim k; Simpl; XAuto.
  59       Qed.
  60
  61       Theorem s_lt: (k:?; i,j:?) (lt i j) -> (lt (s k i) (s k j)).
  62       XElim k; Simpl; XAuto.
  63       Qed.
  64
  65       Theorem s_inj: (k:?; i,j:?) (s k i) = (s k j) -> i = j.
  66       XElim k; XEAuto.
  67       Qed.
  68
  69    End s_props.
  70
  71       Hints Resolve s_le s_lt s_inj : ltlc.
  72
  73       Tactic Definition SRw :=
  74          Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).
  75
  76       Tactic Definition SRwIn H :=
  77          Repeat (Rewrite s_S in H Orelse Rewrite s_plus in H).
  78
  79       Tactic Definition SRwBack :=
  80          Repeat (Rewrite <- s_S Orelse Rewrite <- s_plus Orelse Rewrite <- s_plus_sym).
  81
  82       Tactic Definition SRwBackIn H :=
  83          Repeat (Rewrite <- s_S in H Orelse Rewrite <- s_plus in H Orelse Rewrite <- s_plus_sym in H).
  84
  85       Hint discr : ltlc := Extern 4 (le ? (plus (s ? ?) ?)) SRwBack.