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

   1 (*#* #stop file *)
   2
   3 Require subst1_defs.
   4 Require subst1_confluence.
   5 Require drop_props.
   6 Require pr0_subst1.
   7 Require pr2_defs.
   8
   9    Section pr2_subst1_props. (***********************************************)
  10
  11       Theorem pr2_delta1: (c,d:?; u:?; i:?) (drop i (0) c (CTail d (Bind Abbr) u)) ->
  12                           (t1,t2:?) (pr0 t1 t2) -> (t:?) (subst1 i u t2 t) ->
  13                           (pr2 c t1 t).
  14       Intros; XElim H1; Clear t; XEAuto.
  15       Qed.
  16
  17       Hints Resolve pr2_delta1 : ltlc.
  18
  19       Theorem pr2_subst1: (c,e:?; v:?; i:?) (drop i (0) c (CTail e (Bind Abbr) v)) ->
  20                           (t1,t2:?) (pr2 c t1 t2) ->
  21                           (w1:?) (subst1 i v t1 w1) ->
  22                           (EX w2 | (pr2 c w1 w2) & (subst1 i v t2 w2)).
  23      Intros until 2; XElim H0; Intros;
  24      Pr0Subst1.
  25 (* case 1: pr2_free *)
  26      XEAuto.
  27 (* case 2: pr2_delta *)
  28      Apply (neq_eq_e i i0); Intros.
  29 (* case 2.1: i <> i0 *)
  30      Subst1Confluence; XEAuto.
  31 (* case 2.2: i = i0 *)
  32      Rewrite <- H4 in H0; Rewrite <- H4 in H2; Clear H4 i0.
  33      DropDis; Inversion H0; Rewrite H6 in H3; Clear H0 H5 H6 e v.
  34      Subst1Confluence; XEAuto.
  35      Qed.
  36
  37    End pr2_subst1_props.
  38
  39       Hints Resolve pr2_delta1 : ltlc.
  40
  41       Tactic Definition Pr2Subst1 :=
  42          Match Context With
  43             | [ H0: (drop ?1 (0) ?2 (CTail ?3 (Bind Abbr) ?4));
  44                 H1: (pr2 ?2 ?5 ?6); H3: (subst1 ?1 ?4 ?5 ?7) |- ? ] ->
  45                LApply (pr2_subst1 ?2 ?3 ?4 ?1); [ Intros H_x | XAuto ];
  46                LApply (H_x ?5 ?6); [ Clear H_x H1; Intros H1 | XAuto ];
  47                LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
  48                XElim H1; Intros.