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

   1 (*#* #stop file *)
   2
   3 Require Export subst1_defs.
   4 Require Export csubst0_defs.
   5
   6       Inductive csubst1 [i:nat; v:T; c1:C] : C -> Prop :=
   7          | csubst1_refl   : (csubst1 i v c1 c1)
   8          | csubst1_single : (c2:?) (csubst0 i v c1 c2) -> (csubst1 i v c1 c2).
   9
  10       Hint csubst1 : ltlc := Constructors csubst1.
  11
  12    Section csubst1_props. (**************************************************)
  13
  14       Theorem csubst1_tail: (k:?; i:?; v,u1,u2:?) (subst1 (r k i) v u1 u2) ->
  15                             (c1,c2:?) (csubst1 (r k i) v c1 c2) ->
  16                             (csubst1 (S i) v (CTail c1 k u1) (CTail c2 k u2)).
  17       Intros until 1; XElim H; Clear u2.
  18 (* case 1: csubst1_refl *)
  19       Intros until 1; XElim H; Clear c2; XAuto.
  20 (* case 2: csubst1_single *)
  21       Intros until 2; XElim H0; Clear c2; XAuto.
  22       Qed.
  23
  24    End csubst1_props.
  25
  26       Hints Resolve csubst1_tail : ltlc.
  27
  28    Section csubst1_gen_base. (***********************************************)
  29
  30       Theorem csubst1_gen_tail: (k:?; c1,x:?; u1,v:?; i:?)
  31                                 (csubst1 (S i) v (CTail c1 k u1) x) ->
  32                                 (EX u2 c2 | x = (CTail c2 k u2) &
  33                                             (subst1 (r k i) v u1 u2) &
  34                                             (csubst1 (r k i) v c1 c2)
  35                                 ).
  36       Intros; InsertEq H '(CTail c1 k u1); InsertEq H '(S i);
  37       XElim H; Clear x; Intros.
  38 (* case 1: csubst1_refl *)
  39       Rewrite H0; XEAuto.
  40 (* case 2: csubst1_single *)
  41       Rewrite H0 in H; Rewrite H1 in H; Clear H0 H1 y y0.
  42       CSubst0GenBase; Rewrite H; XEAuto.
  43       Qed.
  44
  45    End csubst1_gen_base.
  46
  47       Tactic Definition CSubst1GenBase :=
  48          Match Context With
  49             | [ H: (csubst1 (S ?1) ?2 (CTail ?3 ?4 ?5) ?6) |- ? ] ->
  50                LApply (csubst1_gen_tail ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
  51                XElim H; Intros.
  52
  53    Section csubst1_drop. (***************************************************)
  54
  55       Theorem csubst1_drop_ge : (i,n:?) (le i n) ->
  56                                 (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
  57                                 (e:?) (drop n (0) c1 e) ->
  58                                 (drop n (0) c2 e).
  59       Intros until 2; XElim H0; Intros;
  60       Try CSubst0Drop; XAuto.
  61       Qed.
  62
  63       Theorem csubst1_drop_lt : (i,n:?) (lt n i) ->
  64                                 (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
  65                                 (e1:?) (drop n (0) c1 e1) ->
  66                                 (EX e2 | (csubst1 (minus i n) v e1 e2) &
  67                                          (drop n (0) c2 e2)
  68                                 ).
  69       Intros until 2; XElim H0; Intros;
  70       Try (
  71          CSubst0Drop; Try Rewrite H1; Try Rewrite minus_x_Sy;
  72          Try Rewrite r_minus in H3; Try Rewrite r_minus in H4
  73       ); XEAuto.
  74       Qed.
  75
  76       Theorem csubst1_drop_ge_back : (i,n:?) (le i n) ->
  77                                      (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
  78                                      (e:?) (drop n (0) c2 e) ->
  79                                      (drop n (0) c1 e).
  80       Intros until 2; XElim H0; Intros;
  81       Try CSubst0Drop; XAuto.
  82       Qed.
  83
  84    End csubst1_drop.
  85
  86       Tactic Definition CSubst1Drop :=
  87          Match Context With
  88             | [ H1: (lt ?2 ?1);
  89                 H2: (csubst1 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
  90                LApply (csubst1_drop_lt ?1 ?2); [ Intros H_x | XAuto ];
  91                LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
  92                LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
  93                XElim H3; Intros
  94             | [H2: (csubst1 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?4 ?6) |- ? ] ->
  95                LApply (csubst1_drop_ge ?1 ?1); [ Intros H_x | XAuto ];
  96                LApply (H_x ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
  97                LApply (H2 ?6); [ Clear H2 H3; Intros | XAuto ]
  98             | [ H2: (csubst1 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
  99                LApply (csubst1_drop_ge ?1 ?2); [ Intros H_x | XAuto ];
 100                LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
 101                LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ].