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

   1 (*#* #stop file *)
   2
   3 Require Export subst0_defs.
   4
   5       Inductive subst1 [i:nat; v:T; t1:T] : T -> Prop :=
   6          | subst1_refl   : (subst1 i v t1 t1)
   7          | subst1_single : (t2:?) (subst0 i v t1 t2) -> (subst1 i v t1 t2).
   8
   9       Hint subst1 : ltlc := Constructors subst1.
  10
  11    Section subst1_props. (***************************************************)
  12
  13       Theorem subst1_tail: (v,u1,u2:?; i:?) (subst1 i v u1 u2) ->
  14                            (k:?; t1,t2:?) (subst1 (s k i) v t1 t2) ->
  15                            (subst1 i v (TTail k u1 t1) (TTail k u2 t2)).
  16       Intros until 1; XElim H; Clear u2.
  17 (* case 1: csubst1_refl *)
  18       Intros until 1; XElim H; Clear t2; XAuto.
  19 (* case 2: csubst1_single *)
  20       Intros until 2; XElim H0; Clear t3; XAuto.
  21       Qed.
  22
  23    End subst1_props.
  24
  25       Hints Resolve subst1_tail : ltlc.
  26
  27    Section subst1_gen_base. (************************************************)
  28
  29       Theorem subst1_gen_sort : (v,x:?; i,n:?) (subst1 i v (TSort n) x) ->
  30                                 x = (TSort n).
  31       Intros; XElim H; Clear x; Intros;
  32       Try Subst0GenBase; XAuto.
  33       Qed.
  34
  35       Theorem subst1_gen_lref : (v,x:?; i,n:?) (subst1 i v (TLRef n) x) ->
  36                                 x = (TLRef n) \/
  37                                 n = i /\ x = (lift (S n) (0) v).
  38       Intros; XElim H; Clear x; Intros;
  39       Try Subst0GenBase; XAuto.
  40       Qed.
  41
  42       Theorem subst1_gen_tail : (k:?; v,u1,t1,x:?; i:?)
  43                                 (subst1 i v (TTail k u1 t1) x) ->
  44                                 (EX u2 t2 | x = (TTail k u2 t2) &
  45                                             (subst1 i v u1 u2) &
  46                                             (subst1 (s k i) v t1 t2)
  47                                 ).
  48       Intros; XElim H; Clear x; Intros;
  49       Try Subst0GenBase; XEAuto.
  50       Qed.
  51
  52    End subst1_gen_base.
  53
  54       Tactic Definition Subst1GenBase :=
  55          Match Context With
  56             | [ H: (subst1 ?1 ?2 (TTail ?3 ?4 ?5) ?6) |- ? ] ->
  57                LApply (subst1_gen_tail ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
  58                XElim H; Intros.