7 Section subst0_subst0. (**************************************************)
9 Tactic Definition IH :=
11 | [ H1: (u1,u:?; i:?) (subst0 i u u1 ?1) -> ?;
12 H2: (subst0 ?2 ?3 ?4 ?1) |- ? ] ->
13 LApply (H1 ?4 ?3 ?2); [ Clear H1; Intros H1 | XAuto ];
15 | [ H1: (u1,u:?; i:?) (subst0 i u ?1 u1) -> ?;
16 H2: (subst0 ?2 ?3 ?1 ?4) |- ? ] ->
17 LApply (H1 ?4 ?3 ?2); [ Clear H1; Intros H1 | XAuto ];
20 Theorem subst0_subst0: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
21 (u1,u:?; i:?) (subst0 i u u1 u2) ->
22 (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
23 Intros until 1; XElim H; Intros.
24 (* case 1 : subst0_bref *)
26 (* case 2 : subst0_fst *)
28 (* case 3 : subst0_snd *)
29 IH; SRwBackIn H2; XEAuto.
30 (* case 4 : subst0_both *)
31 Repeat IH; SRwBackIn H4; XEAuto.
34 Theorem subst0_subst0_back: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
35 (u1,u:?; i:?) (subst0 i u u2 u1) ->
36 (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
37 Intros until 1; XElim H; Intros.
38 (* case 1 : subst0_bref *)
40 (* case 2 : subst0_fst *)
42 (* case 3 : subst0_snd *)
43 IH; SRwBackIn H2; XEAuto.
44 (* case 4 : subst0_both *)
45 Repeat IH; SRwBackIn H4; XEAuto.
48 Theorem subst0_trans: (t2,t1,v:?; i:?) (subst0 i v t1 t2) ->
49 (t3:?) (subst0 i v t2 t3) ->
51 Intros until 1; XElim H; Intros;
52 Subst0Gen; Try Rewrite H1; Try Rewrite H3; XAuto.
57 Hints Resolve subst0_trans : ltlc.
59 Tactic Definition Subst0Subst0 :=
61 | [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (subst0 ?4 ?5 ?6 ?1) |- ? ] ->
62 LApply (subst0_subst0 ?2 ?3 ?1 ?0); [ Intros H_x | XAuto ];
63 LApply (H_x ?6 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
65 | [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (subst0 ?4 ?5 ?1 ?6) |- ? ] ->
66 LApply (subst0_subst0_back ?2 ?3 ?1 ?0); [ Intros H_x | XAuto ];
67 LApply (H_x ?6 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];