X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fs_transition%2Ffqu.ma;h=19dd4d45d0ab14148dbe2405d4f50b2b57ca9615;hp=bff7b2fe9e2561c7f349a58c358153d219d45d58;hb=a454837a256907d2f83d42ced7be847e10361ea9;hpb=b4283c079ed7069016b8d924bbc7e08872440829 diff --git a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma index bff7b2fe9..19dd4d45d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_transition/fqu.ma @@ -28,7 +28,7 @@ include "static_2/relocation/lifts.ma". inductive fqu (b:bool): tri_relation genv lenv term ≝ | fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ{I}V) (#0) G L V | fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②{I}V.T) G L V -| fqu_bind_dx: ∀p,I,G,L,V,T. fqu b G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T +| fqu_bind_dx: ∀p,I,G,L,V,T. b = Ⓣ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T | fqu_clear : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓧ) T | fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ{I}V.T) G L T | fqu_drop : ∀I,G,L,T,U. ⬆*[1] T ≘ U → fqu b G (L.ⓘ{I}) U G L T @@ -44,24 +44,24 @@ interpretation (* Basic properties *********************************************************) -lemma fqu_sort: ∀b,I,G,L,s. ⦃G,L.ⓘ{I},⋆s⦄ ⊐[b] ⦃G,L,⋆s⦄. +lemma fqu_sort: ∀b,I,G,L,s. ⦃G,L.ⓘ{I},⋆s⦄ ⬂[b] ⦃G,L,⋆s⦄. /2 width=1 by fqu_drop/ qed. -lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G,L.ⓘ{I},#↑i⦄ ⊐[b] ⦃G,L,#i⦄. +lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G,L.ⓘ{I},#↑i⦄ ⬂[b] ⦃G,L,#i⦄. /2 width=1 by fqu_drop/ qed. -lemma fqu_gref: ∀b,I,G,L,l. ⦃G,L.ⓘ{I},§l⦄ ⊐[b] ⦃G,L,§l⦄. +lemma fqu_gref: ∀b,I,G,L,l. ⦃G,L.ⓘ{I},§l⦄ ⬂[b] ⦃G,L,§l⦄. /2 width=1 by fqu_drop/ qed. (* Basic inversion lemmas ***************************************************) -fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∀s. T1 = ⋆s → ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s. #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #T #s #H destruct | #I #G #L #V #T #s #H destruct -| #p #I #G #L #V #T #s #H destruct +| #p #I #G #L #V #T #_ #s #H destruct | #p #I #G #L #V #T #_ #s #H destruct | #I #G #L #V #T #s #H destruct | #I #G #L #T #U #HI12 #s #H destruct @@ -69,18 +69,18 @@ fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T ] qed-. -lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ⦃G1,L1,⋆s⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ⦃G1,L1,⋆s⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = ⋆s. /2 width=4 by fqu_inv_sort1_aux/ qed-. -fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∀i. T1 = #i → (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨ ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j. #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #T #i #H destruct /3 width=4 by ex4_2_intro, or_introl/ | #I #G #L #V #T #i #H destruct -| #p #I #G #L #V #T #i #H destruct +| #p #I #G #L #V #T #_ #i #H destruct | #p #I #G #L #V #T #_ #i #H destruct | #I #G #L #V #T #i #H destruct | #I #G #L #T #U #HI12 #i #H destruct @@ -88,18 +88,18 @@ fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T ] qed-. -lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1,L1,#i⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1,L1,#i⦄ ⬂[b] ⦃G2,L2,T2⦄ → (∃∃J,V. G1 = G2 & L1 = L2.ⓑ{J}V & T2 = V & i = 0) ∨ ∃∃J,j. G1 = G2 & L1 = L2.ⓘ{J} & T2 = #j & i = ↑j. /2 width=4 by fqu_inv_lref1_aux/ qed-. -fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∀l. T1 = §l → ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = §l. #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #T #l #H destruct | #I #G #L #V #T #l #H destruct -| #p #I #G #L #V #T #l #H destruct +| #p #I #G #L #V #T #_ #l #H destruct | #p #I #G #L #V #T #_ #l #H destruct | #I #G #L #V #T #s #H destruct | #I #G #L #T #U #HI12 #l #H destruct @@ -107,43 +107,44 @@ fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T ] qed-. -lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ⦃G1,L1,§l⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ⦃G1,L1,§l⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & T2 = §l. /2 width=4 by fqu_inv_gref1_aux/ qed-. -fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∀p,I,V1,U1. T1 = ⓑ{p,I}V1.U1 → ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2 - | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2 + | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2 & b = Ⓣ | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1. #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #T #q #J #V0 #U0 #H destruct | #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro0/ -| #p #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro1/ +| #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro1/ | #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro2/ | #I #G #L #V #T #q #J #V0 #U0 #H destruct | #I #G #L #T #U #HTU #q #J #V0 #U0 #H destruct /3 width=2 by or4_intro3, ex3_intro/ ] qed-. -lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓑ{p,I}V1.U1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓑ{p,I}V1.U1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2 - | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2 + | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2 & b = Ⓣ | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1. /2 width=4 by fqu_inv_bind1_aux/ qed-. -lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2,L2,T2⦄ → +lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓑ{p,I}V1.U1⦄ ⬂ ⦃G2,L2,T2⦄ → ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2 | ∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2 | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓑ{p,I}V1.U1. #p #I #G1 #G2 #L1 #L2 #V1 #U1 #T2 #H elim (fqu_inv_bind1 … H) -H -/3 width=1 by or3_intro0, or3_intro1, or3_intro2/ -* #_ #_ #_ #H destruct +/3 width=1 by or3_intro0, or3_intro2/ +* #HG #HL #HU #H destruct +/3 width=1 by and3_intro, or3_intro1/ qed-. -fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∀I,V1,U1. T1 = ⓕ{I}V1.U1 → ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2 | ∧∧ G1 = G2 & L1 = L2 & U1 = T2 @@ -151,14 +152,14 @@ fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #T #J #V0 #U0 #H destruct | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro0/ -| #p #I #G #L #V #T #J #V0 #U0 #H destruct +| #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct | #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro1/ | #I #G #L #T #U #HTU #J #V0 #U0 #H destruct /3 width=2 by or3_intro2, ex3_intro/ ] qed-. -lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓕ{I}V1.U1⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓕ{I}V1.U1⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2 | ∧∧ G1 = G2 & L1 = L2 & U1 = T2 | ∃∃J. G1 = G2 & L1 = L2.ⓘ{J} & ⬆*[1] T2 ≘ ⓕ{I}V1.U1. @@ -166,31 +167,31 @@ lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1,L1,ⓕ{I}V1.U1⦄ ⊐[b] (* Advanced inversion lemmas ************************************************) -lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ⦃G1,⋆,⓪{I}⦄ ⊐[b] ⦃G2,L2,T2⦄ → ⊥. +lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ⦃G1,⋆,⓪{I}⦄ ⬂[b] ⦃G2,L2,T2⦄ → ⊥. #b * #x #G1 #G2 #L2 #T2 #H [ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H #I [2: #V |3: #i ] #_ #H destruct qed-. -lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ⦃G1,K.ⓘ{I},⋆s⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ⦃G1,K.ⓘ{I},⋆s⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∧∧ G1 = G2 & L2 = K & T2 = ⋆s. #b #I #G1 #G2 #K #L2 #T2 #s #H elim (fqu_inv_sort1 … H) -H #Z #X #H1 #H2 destruct /2 width=1 by and3_intro/ qed-. -lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ⦃G1,K.ⓑ{I}V,#0⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ⦃G1,K.ⓑ{I}V,#0⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∧∧ G1 = G2 & L2 = K & T2 = V. #b #I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H * #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/ qed-. -lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ⦃G1,K.ⓘ{I},#(↑i)⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ⦃G1,K.ⓘ{I},#(↑i)⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∧∧ G1 = G2 & L2 = K & T2 = #i. #b #I #G1 #G2 #K #L2 #T2 #i #H elim (fqu_inv_lref1 … H) -H * #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/ qed-. -lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ⦃G1,K.ⓘ{I},§l⦄ ⊐[b] ⦃G2,L2,T2⦄ → +lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ⦃G1,K.ⓘ{I},§l⦄ ⬂[b] ⦃G2,L2,T2⦄ → ∧∧ G1 = G2 & L2 = K & T2 = §l. #b #I #G1 #G2 #K #L2 #T2 #l #H elim (fqu_inv_gref1 … H) -H #Z #H1 #H2 #H3 destruct /2 width=1 by and3_intro/