7 Require subst0_confluence.
13 Section pr0_confluence. (*************************************************)
15 Tactic Definition SSubstInv :=
17 | [ H0: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] ->
18 Inversion H0; Clear H0
19 | [ H0: (pr0 (TTail (Bind ?) ? ?) ?) |- ? ] ->
20 Inversion H0; Clear H0
21 | _ -> EqFalse Orelse LiftGen Orelse Pr0Gen.
23 Tactic Definition SSubstBack :=
25 | [ H0: Abst = ?1; H1:? |- ? ] ->
26 Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
27 | [ H0: Abbr = ?1; H1:? |- ? ] ->
28 Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
29 | [ H0: (? ?) = ?1; H1:? |- ? ] ->
30 Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
31 | [ H0: (? ? ? ?) = ?1; H1:? |- ? ] ->
32 Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1.
34 Tactic Definition SSubst :=
36 [ H0: ?1 = ?; H1:? |- ? ] ->
37 Rewrite H0 in H1 Orelse Rewrite H0 Orelse Clear H0 ?1.
39 Tactic Definition XSubst :=
40 Repeat (SSubstInv Orelse SSubstBack Orelse SSubst).
42 Tactic Definition IH :=
44 | [ H0: (pr0 ?1 ?2); H1: (pr0 ?1 ?3) |- ? ] ->
45 LApply (H ?1); [ Intros H_x | XEAuto ];
46 LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
47 LApply (H_x ?3); [ Clear H_x; Intros H_x | XAuto ];
48 XElim H_x; Clear H0 H1; Intros.
50 (* case pr0_cong pr0_upsilon pr0_refl ***************************************)
52 Remark pr0_cong_upsilon_refl: (b:?) ~ b = Abst ->
53 (u0,u3:?) (pr0 u0 u3) ->
54 (t4,t5:?) (pr0 t4 t5) ->
55 (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
56 (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) &
57 (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
59 Apply ex2_intro with x:=(TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) x) t5)); XAuto.
62 (* case pr0_cong pr0_upsilon pr0_cong ***************************************)
64 Remark pr0_cong_upsilon_cong: (b:?) ~ b = Abst ->
65 (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
66 (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
67 (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
68 (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) &
69 (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
71 Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
74 (* case pr0_cong pr0_upsilon pr0_delta **************************************)
76 Remark pr0_cong_upsilon_delta: ~ Abbr = Abst ->
77 (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
78 (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
79 (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
80 (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
81 (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
82 (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
84 (* case 1: x0 is a lift *)
85 Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
86 (* case 2: x0 is not a lift *)
87 Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x2)); XEAuto.
90 (* case pr0_cong pr0_upsilon pr0_zeta ***************************************)
92 Remark pr0_cong_upsilon_zeta: (b:?) ~ b = Abst ->
93 (u0,u3:?) (pr0 u0 u3) ->
94 (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
95 (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
96 (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) &
97 (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
98 Intros; LiftTailRwBack; XEAuto.
101 (* case pr0_cong pr0_delta **************************************************)
103 Remark pr0_cong_delta: (u3,t5,w:?) (subst0 (0) u3 t5 w) ->
104 (u2,x:?) (pr0 u2 x) -> (pr0 u3 x) ->
105 (t3,x0:?) (pr0 t3 x0) -> (pr0 t5 x0) ->
106 (EX t:T | (pr0 (TTail (Bind Abbr) u2 t3) t) &
107 (pr0 (TTail (Bind Abbr) u3 w) t)).
108 Intros; Pr0Subst0; XEAuto.
111 (* case pr0_upsilon pr0_upsilon *********************************************)
113 Remark pr0_upsilon_upsilon: (b:?) ~ b = Abst ->
114 (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
115 (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
116 (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
117 (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) &
118 (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)).
120 Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x0) x2)); XAuto.
123 (* case pr0_delta pr0_delta *************************************************)
125 Remark pr0_delta_delta: (u2,t3,w:?) (subst0 (0) u2 t3 w) ->
126 (u3,t5,w0:?) (subst0 (0) u3 t5 w0) ->
127 (x:?) (pr0 u2 x) -> (pr0 u3 x) ->
128 (x0:?) (pr0 t3 x0) -> (pr0 t5 x0) ->
129 (EX t:T | (pr0 (TTail (Bind Abbr) u2 w) t) &
130 (pr0 (TTail (Bind Abbr) u3 w0) t)).
131 Intros; Pr0Subst0; Pr0Subst0; Try Subst0Confluence; XSubst; XEAuto.
134 (* case pr0_delta pr0_epsilon ***********************************************)
136 Remark pr0_delta_epsilon: (u2,t3,w:?) (subst0 (0) u2 t3 w) ->
137 (t4:?) (pr0 (lift (1) (0) t4) t3) ->
138 (t2:?) (EX t:T | (pr0 (TTail (Bind Abbr) u2 w) t) & (pr0 t2 t)).
139 Intros; Pr0Gen; XSubst; Subst0Gen.
142 (* main *********************************************************************)
144 Hints Resolve pr0_cong_upsilon_refl pr0_cong_upsilon_cong : ltlc.
145 Hints Resolve pr0_cong_upsilon_delta pr0_cong_upsilon_zeta : ltlc.
146 Hints Resolve pr0_cong_delta : ltlc.
147 Hints Resolve pr0_upsilon_upsilon : ltlc.
148 Hints Resolve pr0_delta_delta pr0_delta_epsilon : ltlc.
152 (*#* #caption "confluence with itself: Church-Rosser property" *)
153 (*#* #cap #cap t0, t1, t2, t *)
155 Theorem pr0_confluence: (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
156 (EX t | (pr0 t1 t) & (pr0 t2 t)).
160 XElimUsing tlt_wf_ind t0; Intros.
161 Inversion H0; Inversion H1; Clear H0 H1;
162 XSubst; Repeat IH; XDEAuto 4.
167 Tactic Definition Pr0Confluence :=
169 [ H1: (pr0 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
170 LApply (pr0_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
171 LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];