X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Freduction%2Ftpr_defs.ma;h=a8aac61df77fbbd9db92268c3fa9b391ca7c6b09;hb=81cf2dd18ed76a214ab610447d0c5861998b3d96;hp=bddd93017bf8851b2e731b81c3d0c9ce964db7b5;hpb=dd88a8fa58d50833118cadd96ba8e3bcf70340a4;p=helm.git diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma index bddd93017..a8aac61df 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma @@ -45,23 +45,190 @@ lemma tpr_refl: ∀T. T ⇒ T. #I elim I -I /2/ qed. -(* The basic inversion lemmas ***********************************************) +(* Basic inversion lemmas ***************************************************) + +lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k. +#U1 #U2 * -U1 U2 +[ #k0 #k #H destruct -k0 // +| #i #k #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct +| #V #T #T1 #T2 #_ #_ #k #H destruct +| #V #T1 #T2 #_ #k #H destruct +] +qed. + +lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k. +/2/ qed. + +lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i. +#U1 #U2 * -U1 U2 +[ #k #i #H destruct +| #j #i #H destruct -j // +| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct +| #V #T #T1 #T2 #_ #_ #i #H destruct +| #V #T1 #T2 #_ #i #H destruct +] +qed. + +lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i. +/2/ qed. + +lemma tpr_inv_abbr1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abbr} V1. T1 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2 + | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕚{Abbr} V2. T + | ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2. +#U1 #U2 * -U1 U2 +[ #k #V #T #H destruct +| #i #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/ +| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct +| #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/ +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct +| #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/ +| #V #T1 #T2 #_ #V0 #T0 #H destruct +] +qed. + +lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2 + | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕚{Abbr} V2. T + | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2. +/2/ qed. + +lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. +#U1 #U2 * -U1 U2 +[ #k #V #T #H destruct +| #i #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/ +| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct +| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct +| #V #T1 #T2 #_ #V0 #T0 #H destruct +] +qed. + +lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. +/2/ qed. + +lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕓{I} V2. T2 + | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕚{Abbr} V2. T & I = Abbr + | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr. +#V1 #T1 #U2 * #H +[ elim (tpr_inv_abbr1 … H) -H * /3 width=7/ +| /3/ +] +qed. + +lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕚{Appl} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕚{Abst} W. T1 & + U2 = 𝕓{Abbr} V2. T2 + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕚{Abbr} W1. T1 & + U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. +#U1 #U2 * -U1 U2 +[ #k #V #T #H destruct +| #i #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/ +| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/ +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H + destruct -V1 T0 /3 width=12/ +| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct +| #V #T1 #T2 #_ #V0 #T0 #H destruct +] +qed. + +lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕚{Appl} V1. U0 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕚{Appl} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕚{Abst} W. T1 & + U2 = 𝕓{Abbr} V2. T2 + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕚{Abbr} W1. T1 & + U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. +/2/ qed. + +lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 → + (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2) + ∨ T1 ⇒ U2. +#U1 #U2 * -U1 U2 +[ #k #V #T #H destruct +| #i #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/ +| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct +| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct +| #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/ +] +qed. + +lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 → + (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2) + ∨ T1 ⇒ U2. +/2/ qed. + +lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕗{I} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕚{Abst} W. T1 & + U2 = 𝕓{Abbr} V2. T2 & I = Appl + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕚{Abbr} W1. T1 & + U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2 & + I = Appl + | (U0 ⇒ U2 ∧ I = Cast). +#V1 #U0 #U2 * #H +[ elim (tpr_inv_appl1 … H) -H * /3 width=12/ +| elim (tpr_inv_cast1 … H) -H [1: *] /3 width=5/ +] +qed. lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → ∨∨ T1 = #i | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & - T1 = 𝕓{Abbr} V. T - | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T. -#T1 #T2 #H elim H -H T1 T2 + T1 = 𝕚{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T. +#T1 #T2 * -T1 T2 [ #k #i #H destruct | #j #i /2/ -| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #V1 #V2 #T1 #T2 #T #_ #_ #_ #_ #_ #i #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct -| #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/ -| #V #T1 #T2 #HT12 #_ #i #H destruct /3/ +| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct +| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct +| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct +| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/ +| #V #T1 #T2 #HT12 #i #H destruct /3/ ] qed.