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

   1 (*#* #stop file *)
   2
   3 Require lift_props.
   4 Require subst0_defs.
   5
   6    Section subst0_gen_lift_lt. (*********************************************)
   7
   8       Tactic Definition IH :=
   9          Match Context With
  10             [ H1: (x:T; i,h,d:nat) (subst0 i (lift h d ?1) (lift h (S (plus i d)) ?2) x) -> ?;
  11               H2: (subst0 ?3 (lift ?4 ?5 ?1) (lift ?4 (S (plus ?3 ?5)) ?2) ?6) |- ? ] ->
  12                LApply (H1 ?6 ?3 ?4 ?5); [ Clear H1 H2; Intros H1 | XAuto ];
  13                XElim H1; Intros.
  14
  15       Theorem subst0_gen_lift_lt : (u,t1,x:?; i,h,d:?) (subst0 i (lift h d u) (lift h (S (plus i d)) t1) x) ->
  16                                    (EX t2 | x = (lift h (S (plus i d)) t2) & (subst0 i u t1 t2)).
  17       XElim t1; Intros.
  18 (* case 1: TSort *)
  19       Rewrite lift_sort in H; Subst0GenBase.
  20 (* case 2: TLRef n *)
  21       Apply (lt_le_e n (S (plus i d))); Intros.
  22 (* case 2.1: n < 1 + i + d *)
  23       Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
  24       Subst0GenBase; Rewrite H1; Rewrite H.
  25       Rewrite <- lift_d; Simpl; XEAuto.
  26 (* case 2.2: n >= 1 + i + d *)
  27       Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
  28       Subst0GenBase; Rewrite <- H in H0.
  29       EApply le_false; [ Idtac | Apply H0 ]; XAuto.
  30 (* case 3: TTail k *)
  31       Rewrite lift_tail in H1; Subst0GenBase; Rewrite H1; Clear H1 x.
  32 (* case 3.1: subst0_fst *)
  33       IH; Rewrite H; Rewrite <- lift_tail; XEAuto.
  34 (* case 3.2: subst0_snd *)
  35       SRwIn H2; IH; Rewrite H0; SRwBack; Rewrite <- lift_tail; XEAuto.
  36 (* case 3.2: subst0_snd *)
  37       SRwIn H3; Repeat IH; Rewrite H; Rewrite H0; SRwBack;
  38       Rewrite <- lift_tail; XEAuto.
  39       Qed.
  40
  41    End subst0_gen_lift_lt.
  42
  43    Section subst0_gen_lift_false. (******************************************)
  44
  45       Theorem subst0_gen_lift_false : (t,u,x:?; h,d,i:?)
  46                                       (le d i) -> (lt i (plus d h)) ->
  47                                       (subst0 i u (lift h d t) x) ->
  48                                       (P:Prop) P.
  49       XElim t; Intros.
  50 (* case 1: TSort *)
  51       Rewrite lift_sort in H1; Subst0GenBase.
  52 (* case 2: TLRef n *)
  53       Apply (lt_le_e n d); Intros.
  54 (* case 2.1: n < d *)
  55       Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
  56       Subst0GenBase; Rewrite H1 in H2.
  57       EApply le_false; [ Apply H | XAuto ].
  58 (* case 2.2: n >= d *)
  59       Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
  60       Subst0GenBase; Rewrite <- H1 in H0.
  61       EApply le_false; [ Apply H2 | XEAuto ].
  62 (* case 3: TTail k *)
  63       Rewrite lift_tail in H3; Subst0GenBase.
  64 (* case 3.1: subst0_fst *)
  65       EApply H; XEAuto.
  66 (* case 3.2: subst0_snd *)
  67       EApply H0; [ Idtac | Idtac | XEAuto ]; [ Idtac | SRwBack ]; XAuto.
  68 (* case 3.3: subst0_both *)
  69       EApply H; XEAuto.
  70       Qed.
  71
  72    End subst0_gen_lift_false.
  73
  74    Section subst0_gen_lift_ge. (*********************************************)
  75
  76       Tactic Definition IH :=
  77          Match Context With
  78             [ H1: (x:?; i,h,d:?) (subst0 i ?1 (lift h d ?2) x) -> ?;
  79               H2: (subst0 ?3 ?1 (lift ?4 ?5 ?2) ?6) |- ? ] ->
  80                LApply (H1 ?6 ?3 ?4 ?5); [ Clear H1 H2; Intros H1 | XAuto ];
  81                LApply H1; [ Clear H1; Intros H1 | SRwBack; XAuto ];
  82                XElim H1; Intros.
  83
  84       Theorem subst0_gen_lift_ge : (u,t1,x:?; i,h,d:?) (subst0 i u (lift h d t1) x) ->
  85                                    (le (plus d h) i) ->
  86                                    (EX t2 | x = (lift h d t2) & (subst0 (minus i h) u t1 t2)).
  87       XElim t1; Intros.
  88 (* case 1: TSort *)
  89       Rewrite lift_sort in H; Subst0GenBase.
  90 (* case 2: TLRef n *)
  91       Apply (lt_le_e n d); Intros.
  92 (* case 2.1: n < d *)
  93       Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
  94       Subst0GenBase; Rewrite H in H1.
  95       EApply le_false; [ Apply H0 | XAuto ].
  96 (* case 2.2: n >= d *)
  97       Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
  98       Subst0GenBase; Rewrite <- H; Rewrite H2.
  99       Rewrite minus_plus_r.
 100       EApply ex2_intro; [ Idtac | XAuto ].
 101       Rewrite lift_free; [ Idtac | XEAuto (**) | XAuto ].
 102       Rewrite plus_sym; Rewrite plus_n_Sm; XAuto.
 103 (* case 3: TTail k *)
 104       Rewrite lift_tail in H1; Subst0GenBase; Rewrite H1; Clear H1 x;
 105       Repeat IH; Try Rewrite H; Try Rewrite H0;
 106       Rewrite <- lift_tail; Try Rewrite <- s_minus in H1; XEAuto.
 107       Qed.
 108
 109    End subst0_gen_lift_ge.
 110
 111       Tactic Definition Subst0Gen :=
 112          Match Context With
 113             | [ H: (subst0 ?0 (lift ?1 ?2 ?3) (lift ?1 (S (plus ?0 ?2)) ?4) ?5) |- ? ] ->
 114                LApply (subst0_gen_lift_lt ?3 ?4 ?5 ?0 ?1 ?2); [ Clear H; Intros H | XAuto ];
 115                XElim H; Intros
 116             | [ H: (subst0 ?0 ?1 (lift (1) ?0 ?2) ?3) |- ? ] ->
 117                LApply (subst0_gen_lift_false ?2 ?1 ?3 (1) ?0 ?0); [ Intros H_x | XAuto ];
 118                LApply H_x; [ Clear H_x; Intros H_x | Rewrite plus_sym; XAuto ];
 119                LApply H_x; [ Clear H H_x; Intros H | XAuto ];
 120                Apply H
 121             | [ _: (le ?1 ?2); _: (lt ?2 (plus ?1 ?3));
 122                 _: (subst0 ?2 ?4 (lift ?3 ?1 ?5) ?6) |- ? ] ->
 123                Apply (subst0_gen_lift_false ?5 ?4 ?6 ?3 ?1 ?2); XAuto
 124             | [ _: (subst0 ?1 ?2 (lift (S ?1) (0) ?3) ?4) |- ? ] ->
 125                Apply (subst0_gen_lift_false ?3 ?2 ?4 (S ?1) (0) ?1); XAuto
 126             | [ H: (subst0 ?0 ?1 (lift ?2 ?3 ?4) ?5) |- ? ] ->
 127                LApply (subst0_gen_lift_ge ?1 ?4 ?5 ?0 ?2 ?3); [ Clear H; Intros H | XAuto ];
 128                LApply H; [ Clear H; Intros H | Simpl; XAuto ];
 129                XElim H; Intros
 130             | _ -> Subst0GenBase.