2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda-delta/syntax/weight.ma".
13 include "lambda-delta/reduction/pr_lift.ma".
15 (* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
17 (* Confluence lemmas ********************************************************)
19 lemma pr_conf_sort_sort: ∀L,k1. ∃∃T0. L ⊢ (⋆k1) ⇒ T0 & L ⊢ (⋆k1) ⇒ T0.
22 lemma pr_conf_lref_lref: ∀L,i1. ∃∃T0. L ⊢ (#i1) ⇒ T0 & L ⊢ (#i1) ⇒ T0.
25 (* Confluence ***************************************************************)
29 ∀L1,T1. #[L1, T1] < #[L, T] →
30 ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
31 ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
33 ∀K1,U1,T1,K2,U2,T2. K1 ⊢ U1 ⇒ T1 → K2 ⊢ U2 ⇒ T2 →
34 K1 = L → U1 = T → K2 = L → U2 = T →
35 ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
36 #L #T #IH #K1 #U1 #T1 #K2 #U2 #T2
39 (* case 1: sort, sort *)
40 [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 IH //
41 (* case 2: sort, lref (excluded) *)
42 | #K2 #i2 #H1 #H2 #H3 #H4 destruct
43 (* case 3: sort, bind (excluded) *)
44 | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
45 (* case 4: sort, flat (excluded) *)
46 | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
47 (* case 5: sort, beta (excluded) *)
48 | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
49 (* case 6: sort, delta (excluded) *)
50 | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct
51 (* case 7: sort, theta (excluded) *)
52 | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct
53 (* case 8: sort, zeta (excluded) *)
54 | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
55 (* case 9: sort, tau (excluded) *)
56 | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
59 (* case 10: lref, sort (excluded) *)
60 [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
61 (* case 11: lref, sort (excluded) *)
62 | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 IH //
63 (* case 12: lref, bind (excluded) *)
64 | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
65 (* case 13: lref, flat (excluded) *)
66 | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
67 (* case 14: lref, beta (excluded) *)
68 | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
69 (* case 15: lref, delta (excluded) *)
70 | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct
71 (* case 16: lref, theta (excluded) *)
72 | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct
73 (* case 17: lref, zeta (excluded) *)
74 | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
75 (* case 18: lref, tau (excluded) *)
76 | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
79 theorem pr_conf: ∀L,T,T1,T2. L ⊢ T ⇒ T1 → L ⊢ T ⇒ T2 →
80 ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
81 #L #T @(cw_wf_ind … L T) -L T /3 width=12/