matita/matita/lib/lambda-delta/reduction/pr_pr.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda-delta/syntax/weight.ma".
  13 include "lambda-delta/reduction/pr_lift.ma".
  14
  15 (* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
  16
  17 (* Confluence lemmas ********************************************************)
  18
  19 lemma pr_conf_sort_sort: ∀L,k1. ∃∃T0. L ⊢ (⋆k1) ⇒ T0 & L ⊢ (⋆k1) ⇒ T0.
  20 /2/ qed.
  21
  22 lemma pr_conf_lref_lref: ∀L,i1. ∃∃T0. L ⊢ (#i1) ⇒ T0 & L ⊢ (#i1) ⇒ T0.
  23 /2/ qed.
  24
  25 lemma pr_conf_bind_bind:
  26    ∀L,I1,V11,V12,T11,T12,V22,T22. (
  27       ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) →
  28       ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
  29       ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
  30    ) →
  31    L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 →
  32    L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 →
  33    ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0.
  34 #L #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
  35 elim (IH … HV1 … HV2) [2: /2/ ] #V #HV1 #HV2
  36 elim (IH … HT1 … HT2) [2: normalize // ] -HT1 HT2 T11 IH #T #HT1 #HT2
  37 @ex2_1_intro [2: @pr_bind [3: @HV1 |1: skip |4:
  38
  39 (* Confluence ***************************************************************)
  40
  41 lemma pr_conf_aux:
  42    ∀L,T. (
  43       ∀L1,T1. #[L1, T1] < #[L, T] →
  44       ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
  45       ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
  46          ) →
  47    ∀K1,U1,T1,K2,U2,T2. K1 ⊢ U1 ⇒ T1 → K2 ⊢ U2 ⇒ T2 →
  48    K1 = L → U1 = T → K2 = L → U2 = T →
  49    ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
  50 #L #T #IH #K1 #U1 #T1 #K2 #U2 #T2
  51 * -K1 U1 T1
  52 [ #K1 #k1 * -K2 U2 T2
  53 (* case 1: sort, sort *)
  54   [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 //
  55 (* case 2: sort, lref (excluded) *)
  56   | #K2 #i2 #H1 #H2 #H3 #H4 destruct
  57 (* case 3: sort, bind (excluded) *)
  58   | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
  59 (* case 4: sort, flat (excluded) *)
  60   | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
  61 (* case 5: sort, beta (excluded) *)
  62   | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
  63 (* case 6: sort, delta (excluded) *)
  64   | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct
  65 (* case 7: sort, theta (excluded) *)
  66   | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct
  67 (* case 8: sort, zeta (excluded) *)
  68   | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
  69 (* case 9: sort, tau (excluded) *)
  70   | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
  71   ]
  72 | #K1 #i1 * -K2 U2 T2
  73 (* case 10: lref, sort (excluded) broken *)
  74   [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
  75 (* case 11: lref, sort (excluded) *)
  76   | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 //
  77 (* case 12: lref, bind (excluded) *)
  78   | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
  79 (* case 13: lref, flat (excluded) *)
  80   | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
  81 (* case 14: lref, beta (excluded) *)
  82   | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
  83 (* case 15: lref, delta (excluded) *)
  84   | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct
  85 (* case 16: lref, theta (excluded) *)
  86   | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct
  87 (* case 17: lref, zeta (excluded) *)
  88   | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
  89 (* case 18: lref, tau (excluded) *)
  90   | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
  91   ]
  92 | #K1 #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -K2 U2 T2
  93 (* case 19: bind, sort (excluded) broken *)
  94   [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
  95 (* case 20: bind, lref (excluded) *)
  96   | #K2 #i2 #H1 #H2 #H3 #H4 destruct
  97 (* case 21: bind, bind *)
  98   | #K2 #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 #H3 #H4
  99     destruct -T K1 K2 I2 V21 T21;
 100
 101
 102 theorem pr_conf: ∀L,T,T1,T2. L ⊢ T ⇒ T1 → L ⊢ T ⇒ T2 →
 103                  ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
 104 #L #T @(cw_wf_ind … L T) -L T /3 width=12/
 105 qed.
 106
 107 lemma pr_conf_bind_bind:
 108    ∀L,I1,V11,V12,T11,T12,V22,T22. (
 109       ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) →
 110       ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
 111       ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
 112    ) →
 113    L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 →
 114    L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 →
 115    ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0.