X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frdeq.ma;h=6cb56dcaf43200dc2c6eebb6751107f973902db0;hp=f2de0dfe67933071afcafeacf99ab266cb4cb126;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma index f2de0dfe6..6cb56dcaf 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma @@ -12,30 +12,30 @@ (* *) (**************************************************************************) -include "static_2/notation/relations/stareqsn_5.ma". +include "static_2/notation/relations/stareqsn_3.ma". include "static_2/syntax/tdeq_ext.ma". include "static_2/static/rex.ma". -(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) +(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***) -definition rdeq (h) (o): relation3 term lenv lenv ≝ - rex (cdeq h o). +definition rdeq: relation3 term lenv lenv ≝ + rex cdeq. interpretation - "degree-based equivalence on referred entries (local environment)" - 'StarEqSn h o T L1 L2 = (rdeq h o T L1 L2). + "sort-irrelevant equivalence on referred entries (local environment)" + 'StarEqSn T L1 L2 = (rdeq T L1 L2). interpretation - "degree-based ranged equivalence (local environment)" - 'StarEqSn h o f L1 L2 = (sex (cdeq_ext h o) cfull f L1 L2). + "sort-irrelevant ranged equivalence (local environment)" + 'StarEqSn f L1 L2 = (sex cdeq_ext cfull f L1 L2). (* Basic properties ***********************************************************) -lemma frees_tdeq_conf_rdeq (h) (o): ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛[h, o] T2 → - ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f. -#h #o #f #L1 #T1 #H elim H -f -L1 -T1 +lemma frees_tdeq_conf_rdeq: ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛ T2 → + ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f. +#f #L1 #T1 #H elim H -f -L1 -T1 [ #f #L1 #s1 #Hf #X #H1 #L2 #_ - elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct + elim (tdeq_inv_sort1 … H1) -H1 #s2 #H destruct /2 width=3 by frees_sort/ | #f #i #Hf #X #H1 >(tdeq_inv_lref1 … H1) -X #Y #H2 @@ -65,130 +65,130 @@ lemma frees_tdeq_conf_rdeq (h) (o): ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ] qed-. -lemma frees_tdeq_conf (h) (o): ∀f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f → - ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f. +lemma frees_tdeq_conf: ∀f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f → + ∀T2. T1 ≛ T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f. /4 width=7 by frees_tdeq_conf_rdeq, sex_refl, ext2_refl/ qed-. -lemma frees_rdeq_conf (h) (o): ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f → - ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f. +lemma frees_rdeq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f → + ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f. /2 width=7 by frees_tdeq_conf_rdeq, tdeq_refl/ qed-. -lemma tdeq_rex_conf (R) (h) (o): s_r_confluent1 … (cdeq h o) (rex R). -#R #h #o #L1 #T1 #T2 #HT12 #L2 * +lemma tdeq_rex_conf (R): s_r_confluent1 … cdeq (rex R). +#R #L1 #T1 #T2 #HT12 #L2 * /3 width=5 by frees_tdeq_conf, ex2_intro/ qed-. -lemma tdeq_rex_div (R) (h) (o): ∀T1,T2. T1 ≛[h, o] T2 → - ∀L1,L2. L1 ⪤[R, T2] L2 → L1 ⪤[R, T1] L2. +lemma tdeq_rex_div (R): ∀T1,T2. T1 ≛ T2 → + ∀L1,L2. L1 ⪤[R, T2] L2 → L1 ⪤[R, T1] L2. /3 width=5 by tdeq_rex_conf, tdeq_sym/ qed-. -lemma tdeq_rdeq_conf (h) (o): s_r_confluent1 … (cdeq h o) (rdeq h o). +lemma tdeq_rdeq_conf: s_r_confluent1 … cdeq rdeq. /2 width=5 by tdeq_rex_conf/ qed-. -lemma tdeq_rdeq_div (h) (o): ∀T1,T2. T1 ≛[h, o] T2 → - ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2. +lemma tdeq_rdeq_div: ∀T1,T2. T1 ≛ T2 → + ∀L1,L2. L1 ≛[T2] L2 → L1 ≛[T1] L2. /2 width=5 by tdeq_rex_div/ qed-. -lemma rdeq_atom (h) (o): ∀I. ⋆ ≛[h, o, ⓪{I}] ⋆. +lemma rdeq_atom: ∀I. ⋆ ≛[⓪{I}] ⋆. /2 width=1 by rex_atom/ qed. -lemma rdeq_sort (h) (o): ∀I1,I2,L1,L2,s. - L1 ≛[h, o, ⋆s] L2 → L1.ⓘ{I1} ≛[h, o, ⋆s] L2.ⓘ{I2}. +lemma rdeq_sort: ∀I1,I2,L1,L2,s. + L1 ≛[⋆s] L2 → L1.ⓘ{I1} ≛[⋆s] L2.ⓘ{I2}. /2 width=1 by rex_sort/ qed. -lemma rdeq_pair (h) (o): ∀I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 → V1 ≛[h, o] V2 → - L1.ⓑ{I}V1 ≛[h, o, #0] L2.ⓑ{I}V2. +lemma rdeq_pair: ∀I,L1,L2,V1,V2. + L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ{I}V1 ≛[#0] L2.ⓑ{I}V2. /2 width=1 by rex_pair/ qed. (* -lemma rdeq_unit (h) (o): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤[cdeq_ext h o, cfull, f] L2 → - L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}. +lemma rdeq_unit: ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤[cdeq_ext, cfull, f] L2 → + L1.ⓤ{I} ≛[#0] L2.ⓤ{I}. /2 width=3 by rex_unit/ qed. *) -lemma rdeq_lref (h) (o): ∀I1,I2,L1,L2,i. - L1 ≛[h, o, #i] L2 → L1.ⓘ{I1} ≛[h, o, #↑i] L2.ⓘ{I2}. +lemma rdeq_lref: ∀I1,I2,L1,L2,i. + L1 ≛[#i] L2 → L1.ⓘ{I1} ≛[#↑i] L2.ⓘ{I2}. /2 width=1 by rex_lref/ qed. -lemma rdeq_gref (h) (o): ∀I1,I2,L1,L2,l. - L1 ≛[h, o, §l] L2 → L1.ⓘ{I1} ≛[h, o, §l] L2.ⓘ{I2}. +lemma rdeq_gref: ∀I1,I2,L1,L2,l. + L1 ≛[§l] L2 → L1.ⓘ{I1} ≛[§l] L2.ⓘ{I2}. /2 width=1 by rex_gref/ qed. -lemma rdeq_bind_repl_dx (h) (o): ∀I,I1,L1,L2.∀T:term. - L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I1} → - ∀I2. I ≛[h, o] I2 → - L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I2}. +lemma rdeq_bind_repl_dx: ∀I,I1,L1,L2.∀T:term. + L1.ⓘ{I} ≛[T] L2.ⓘ{I1} → + ∀I2. I ≛ I2 → + L1.ⓘ{I} ≛[T] L2.ⓘ{I2}. /2 width=2 by rex_bind_repl_dx/ qed-. (* Basic inversion lemmas ***************************************************) -lemma rdeq_inv_atom_sn (h) (o): ∀Y2. ∀T:term. ⋆ ≛[h, o, T] Y2 → Y2 = ⋆. +lemma rdeq_inv_atom_sn: ∀Y2. ∀T:term. ⋆ ≛[T] Y2 → Y2 = ⋆. /2 width=3 by rex_inv_atom_sn/ qed-. -lemma rdeq_inv_atom_dx (h) (o): ∀Y1. ∀T:term. Y1 ≛[h, o, T] ⋆ → Y1 = ⋆. +lemma rdeq_inv_atom_dx: ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆. /2 width=3 by rex_inv_atom_dx/ qed-. (* -lemma rdeq_inv_zero (h) (o): ∀Y1,Y2. Y1 ≛[h, o, #0] Y2 → - ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ - | ∃∃I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 - | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤[cdeq_ext h o, cfull, f] L2 & - Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. -#h #o #Y1 #Y2 #H elim (rex_inv_zero … H) -H * +lemma rdeq_inv_zero: ∀Y1,Y2. Y1 ≛[#0] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I,L1,L2,V1,V2. L1 ≛[V1] L2 & V1 ≛ V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 + | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤[cdeq_ext h o, cfull, f] L2 & + Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. +#Y1 #Y2 #H elim (rex_inv_zero … H) -H * /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/ qed-. *) -lemma rdeq_inv_lref (h) (o): ∀Y1,Y2,i. Y1 ≛[h, o, #↑i] Y2 → - ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ - | ∃∃I1,I2,L1,L2. L1 ≛[h, o, #i] L2 & - Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. +lemma rdeq_inv_lref: ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by rex_inv_lref/ qed-. (* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *) -lemma rdeq_inv_bind (h) (o): ∀p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 → - ∧∧ L1 ≛[h, o, V] L2 & L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. +lemma rdeq_inv_bind: ∀p,I,L1,L2,V,T. L1 ≛[ⓑ{p,I}V.T] L2 → + ∧∧ L1 ≛[V] L2 & L1.ⓑ{I}V ≛[T] L2.ⓑ{I}V. /2 width=2 by rex_inv_bind/ qed-. (* Basic_2A1: uses: lleq_inv_flat *) -lemma rdeq_inv_flat (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → - ∧∧ L1 ≛[h, o, V] L2 & L1 ≛[h, o, T] L2. +lemma rdeq_inv_flat: ∀I,L1,L2,V,T. L1 ≛[ⓕ{I}V.T] L2 → + ∧∧ L1 ≛[V] L2 & L1 ≛[T] L2. /2 width=2 by rex_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma rdeq_inv_zero_pair_sn (h) (o): ∀I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[h, o, #0] Y2 → - ∃∃L2,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y2 = L2.ⓑ{I}V2. +lemma rdeq_inv_zero_pair_sn: ∀I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[#0] Y2 → + ∃∃L2,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y2 = L2.ⓑ{I}V2. /2 width=1 by rex_inv_zero_pair_sn/ qed-. -lemma rdeq_inv_zero_pair_dx (h) (o): ∀I,Y1,L2,V2. Y1 ≛[h, o, #0] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1. +lemma rdeq_inv_zero_pair_dx: ∀I,Y1,L2,V2. Y1 ≛[#0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ{I}V1. /2 width=1 by rex_inv_zero_pair_dx/ qed-. -lemma rdeq_inv_lref_bind_sn (h) (o): ∀I1,Y2,L1,i. L1.ⓘ{I1} ≛[h, o, #↑i] Y2 → - ∃∃I2,L2. L1 ≛[h, o, #i] L2 & Y2 = L2.ⓘ{I2}. +lemma rdeq_inv_lref_bind_sn: ∀I1,Y2,L1,i. L1.ⓘ{I1} ≛[#↑i] Y2 → + ∃∃I2,L2. L1 ≛[#i] L2 & Y2 = L2.ⓘ{I2}. /2 width=2 by rex_inv_lref_bind_sn/ qed-. -lemma rdeq_inv_lref_bind_dx (h) (o): ∀I2,Y1,L2,i. Y1 ≛[h, o, #↑i] L2.ⓘ{I2} → - ∃∃I1,L1. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1}. +lemma rdeq_inv_lref_bind_dx: ∀I2,Y1,L2,i. Y1 ≛[#↑i] L2.ⓘ{I2} → + ∃∃I1,L1. L1 ≛[#i] L2 & Y1 = L1.ⓘ{I1}. /2 width=2 by rex_inv_lref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) -lemma rdeq_fwd_zero_pair (h) (o): ∀I,K1,K2,V1,V2. - K1.ⓑ{I}V1 ≛[h, o, #0] K2.ⓑ{I}V2 → K1 ≛[h, o, V1] K2. +lemma rdeq_fwd_zero_pair: ∀I,K1,K2,V1,V2. + K1.ⓑ{I}V1 ≛[#0] K2.ⓑ{I}V2 → K1 ≛[V1] K2. /2 width=3 by rex_fwd_zero_pair/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *) -lemma rdeq_fwd_pair_sn (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ②{I}V.T] L2 → L1 ≛[h, o, V] L2. +lemma rdeq_fwd_pair_sn: ∀I,L1,L2,V,T. L1 ≛[②{I}V.T] L2 → L1 ≛[V] L2. /2 width=3 by rex_fwd_pair_sn/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *) -lemma rdeq_fwd_bind_dx (h) (o): ∀p,I,L1,L2,V,T. - L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. +lemma rdeq_fwd_bind_dx: ∀p,I,L1,L2,V,T. + L1 ≛[ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[T] L2.ⓑ{I}V. /2 width=2 by rex_fwd_bind_dx/ qed-. (* Basic_2A1: uses: lleq_fwd_flat_dx *) -lemma rdeq_fwd_flat_dx (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 ≛[h, o, T] L2. +lemma rdeq_fwd_flat_dx: ∀I,L1,L2,V,T. L1 ≛[ⓕ{I}V.T] L2 → L1 ≛[T] L2. /2 width=3 by rex_fwd_flat_dx/ qed-. -lemma rdeq_fwd_dx (h) (o): ∀I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} → - ∃∃I1,K1. L1 = K1.ⓘ{I1}. +lemma rdeq_fwd_dx: ∀I2,L1,K2. ∀T:term. L1 ≛[T] K2.ⓘ{I2} → + ∃∃I1,K1. L1 = K1.ⓘ{I1}. /2 width=5 by rex_fwd_dx/ qed-.