From 16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 20 Feb 2012 18:59:54 +0000 Subject: [PATCH] initial properies of the "same top term constructor" predicate --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 1 - .../Basic_2/computation/cprs_tstc.ma | 36 ++++++++ .../lambda_delta/Basic_2/computation/csn.ma | 2 +- .../Basic_2/computation/csn_cr.ma | 19 ++++- .../Basic_2/computation/csn_lcpr.ma | 4 +- .../Basic_2/computation/csn_lift.ma | 42 ++++++---- .../Basic_2/computation/csn_vector.ma | 50 +++++++++++ .../lambda_delta/Basic_2/grammar/term.ma | 18 ++-- .../lambda_delta/Basic_2/grammar/thom.ma | 5 -- .../lambda_delta/Basic_2/grammar/tstc.ma | 83 +++++++++++++++++++ .../lambda_delta/Basic_2/grammar/tstc_tstc.ma | 32 +++++++ .../contribs/lambda_delta/Basic_2/notation.ma | 4 + .../lambda_delta/Ground_2/xoa.conf.xml | 1 + .../contribs/lambda_delta/Ground_2/xoa.ma | 8 ++ .../lambda_delta/Ground_2/xoa_notation.ma | 10 +++ matita/matita/predefined_virtuals.ml | 2 +- 16 files changed, 285 insertions(+), 32 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/csn_vector.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_tstc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index 6e8799876..ae211d291 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -291,7 +291,6 @@ sn3/props sn3_cdelta sn3/props sn3_appl_lref sn3/props sn3_appl_abbr sn3/props sn3_appl_cast -sn3/props sn3_appl_appl sn3/props sn3_appl_beta sn3/props sn3_appl_appls sn3/props sn3_appls_lref diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc.ma new file mode 100644 index 000000000..e19eb68b8 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/grammar/tstc.ma". +include "Basic_2/reducibility/cpr_lift.ma". +include "Basic_2/reducibility/lcpr_cpr.ma". +include "Basic_2/computation/cprs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Forward lemmas involving same top term constructor ***********************) + +lemma cpr_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡ U → + ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨ + L ⊢ ⓓV. ⓐV2. T ➡* U. +#L #V1 #V #T #U #H #V2 #HV12 +elim (cpr_inv_appl1 … H) -H * +[ -HV12 #V0 #X #_ #_ #H destruct /2 width=1/ +| -HV12 #V0 #W #T1 #T2 #_ #_ #H destruct +| #V0 #V3 #W1 #W2 #T1 #T2 #HV10 #HW12 #HT12 #HV03 #H1 #H2 destruct + lapply (cpr_lift (L.ⓓW1) … HV12 … HV03 … HV10) -V0 -HV12 /2 width=1/ #HV23 + lapply (lcpr_cpr_trans (L. ⓓW1) … HT12) -HT12 /2 width=1/ #HT12 + /4 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma index f5d8b7390..043fa9a27 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma @@ -62,7 +62,7 @@ lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓣW. @csn_intro #X #H1 #H2 elim (cpr_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct - elim (eq_false_inv_tpair … H2) -H2 + elim (eq_false_inv_tpair_sn … H2) -H2 [ /3 width=3/ | -HLW0 * #H destruct /3 width=1/ ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma index bbdfd773e..e71d2bd3e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma @@ -13,10 +13,27 @@ (**************************************************************************) include "Basic_2/computation/acp_cr.ma". -include "Basic_2/computation/csn_lift.ma". +include "Basic_2/computation/csn_lcpr.ma". +include "Basic_2/computation/csn_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) (* Advanced properties ******************************************************) +(* +lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. +#L #V1s #V2s * -V1s -V2s /2 width=1/ +#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/ +#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV +lapply (csn_appl_theta … HV12 … H) -H -HV12 #H +lapply (csn_fwd_pair_sn … H) #HV1 +@csn_appl_simple // #X #H1 #H2 +whd in ⊢ (? ? %); +*) +(* +lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. +#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/ +*) axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma index 30368a428..77ae2f9db 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma @@ -35,7 +35,7 @@ elim (cpr_inv_abbr1 … H1) -H1 * [ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1 lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1 - elim (eq_false_inv_tpair … H2) -H2 + elim (eq_false_inv_tpair_sn … H2) -H2 [ #HV1 @IHV // /2 width=1/ -HV1 @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ | -IHV -HLV1 * #H destruct /3 width=1/ @@ -88,7 +88,7 @@ elim (cpr_inv_appl1 … HL) -HL * elim (lift_total V0 0 1) #V5 #HV05 elim (term_eq_dec (ⓓV.ⓐV2.T) (ⓓV4.ⓐV5.T3)) [ -IHVT #H0 destruct - elim (eq_false_inv_tpair … H) -H + elim (eq_false_inv_tpair_sn … H) -H [ -HLV10 -HLV34 -HV3 -HLT3 -HVT >(lift_inj … HV12 … HV05) -V5 #H elim (H ?) // diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma index 2e816b72c..de29660f0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma @@ -72,29 +72,39 @@ lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L @csn_intro #X #H1 #H2 elim (cpr_inv_abst1 … H1 I V) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct -elim (eq_false_inv_tpair … H2) -H2 +elim (eq_false_inv_tpair_sn … H2) -H2 [ /3 width=5/ | -HLW0 * #H destruct /3 width=1/ ] qed. -(* -axiom eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2. - (②{I} V1. T1 = ②{I} V2. T2 → False) → - (T1 = T2 → False) ∨ (T1 = T2 ∧ (V1 = V2 → False)). - -#I #V1 #T1 #V2 #T2 #H -elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct -@or_intror @conj // #HT12 destruct /2 width=1/ -qed-. -lemma csn_appl_simple: ∀L,T. L ⊢ ⬇* T → 𝐒[T] → ∀V. L ⊢ ⬇* V → L ⊢ ⬇* ⓐV. T. -#L #T #H elim H -T #T #_ #IHT #HT #V #H @(csn_ind … H) -V #V #HV #IHV +(* Basic_1: was only: sn3_appl_appl *) +lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) → + 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. +#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 @csn_intro #X #H1 #H2 elim (cpr_inv_appl1_simple … H1 ?) // -H1 -#V0 #T0 #HLV0 #HLT0 #H destruct +#V0 #T0 #HLV0 #HLT10 #H destruct elim (eq_false_inv_tpair_dx … H2) -H2 -[ -IHV #HT0 @IHT -IHT // -HLT0 /2 width=1/ -HT0 /2 width=3/ -| -HV -HT -IHT -HLT0 * #H #HV0 destruct /3 width=1/ +[ -IHV -HT1 #HT10 + @(csn_cpr_trans … (ⓐV.T0)) /2 width=1/ -HLV0 + @IHT1 -IHT1 // /2 width=1/ +| -HLT10 * #H #HV0 destruct + @IHV -IHV // -HT1 /2 width=1/ -HV0 + #T2 #HLT02 #HT02 + @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0 + @IHT1 -IHT1 // -HLT02 /2 width=1/ +] +qed. + +(* Basic_1: was only: sn3_appl_appls *) +lemma csn_appl_appls_simple: ∀L,V. L ⊢ ⬇* V → ∀Vs,T1. + (∀T2. L ⊢ ⒶVs.T1 ➡ T2 → (ⒶVs.T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) → + 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1. +#L #V #HV #Vs elim Vs -Vs +[ @csn_appl_simple // +| #V0 #Vs #_ #T1 #HT1 #_ + @csn_appl_simple // -HV @HT1 ] qed. -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_vector.ma new file mode 100644 index 000000000..bddaaa89d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_vector.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/grammar/term_vector.ma". +include "Basic_2/computation/csn.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) + +inductive csnv (L:lenv): predicate (list term) ≝ +| csnv_nil: csnv L ◊ +| csn_cons: ∀Ts,T. L ⊢ ⬇* T → csnv L Ts → csnv L (T :: Ts) +. + +interpretation + "context-sensitive strong normalization (term vector)" + 'SN L Ts = (csnv L Ts). + +(* Basic inversion lemmas ***************************************************) + +fact csnv_inv_cons_aux: ∀L,Ts. L ⊢ ⬇* Ts → ∀U,Us. Ts = U :: Us → + L ⊢ ⬇* U ∧ L ⊢ ⬇* Us. +#L #Ts * -Ts +[ #U #Us #H destruct +| #Ts #T #HT #HTs #U #Us #H destruct /2 width=1/ +] +qed. + +lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts. +/2 width=3/ qed-. + +include "Basic_2/computation/csn_cpr.ma". + +lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T. +#L #T #Vs elim Vs -Vs /2 width=1/ +#V #Vs #IHVs #HVs +lapply (csn_fwd_pair_sn … HVs) #HV +lapply (csn_fwd_flat_dx … HVs) -HVs #HVs +elim (IHVs HVs) -IHVs -HVs /3 width=1/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma index 32f8272dc..6e8370d49 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -81,24 +81,32 @@ lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False. ] qed-. -lemma eq_false_inv_tpair: ∀I,V1,T1,V2,T2. - (②{I} V1. T1 = ②{I} V2. T2 → False) → - (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)). +lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2. + (②{I} V1. T1 = ②{I} V2. T2 → False) → + (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)). #I #V1 #T1 #V2 #T2 #H elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct @or_intror @conj // #HT12 destruct /2 width=1/ qed-. +lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2. + (②{I} V1. T1 = ②{I} V2. T2 → False) → + (T1 = T2 → False) ∨ (T1 = T2 ∧ (V1 = V2 → False)). +#I #V1 #T1 #V2 #T2 #H +elim (term_eq_dec T1 T2) /3 width=1/ #HT12 destruct +@or_intror @conj // #HT12 destruct /2 width=1/ +qed-. + lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2. (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →False) → (W1 = W2 → False) ∨ (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → False)). #V1 #V2 #W1 #W2 #T1 #T2 #H -elim (eq_false_inv_tpair … H) -H +elim (eq_false_inv_tpair_sn … H) -H [ #HV12 elim (term_eq_dec W1 W2) /3 width=1/ #H destruct @or_intror @conj // #H destruct /2 width=1/ | * #H1 #H2 destruct - elim (eq_false_inv_tpair … H2) -H2 /3 width=1/ + elim (eq_false_inv_tpair_sn … H2) -H2 /3 width=1/ * #H #HT12 destruct @or_intror @conj // #H destruct /2 width=1/ ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma index 153492028..5b90bd1d3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma @@ -76,8 +76,3 @@ lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & I = Appl & T2 = ⓐW2. U2. /2 width=4/ qed-. - -(* Basic_1: removed theorems 7: - iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans - iso_flats_lref_bind_false iso_flats_flat_bind_false -*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma new file mode 100644 index 000000000..26bb95386 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/grammar/term.ma". + +(* SAME TOP TERM CONSTRUCTOR ************************************************) + +inductive tstc: relation term ≝ + | tstc_atom: ∀I. tstc (⓪{I}) (⓪{I}) + | tstc_pair: ∀I,V1,V2,T1,T2. tstc (②{I} V1. T1) (②{I} V2. T2) +. + +interpretation "same top constructor (term)" 'Iso T1 T2 = (tstc T1 T2). + +(* Basic properties *********************************************************) + +(* Basic_1: was: iso_refl *) +lemma tstc_refl: ∀T. T ≃ T. +#T elim T -T // +qed. + +lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1. +#T1 #T2 #H elim H -T1 -T2 // +qed. + +(* Basic inversion lemmas ***************************************************) + +fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}. +#T1 #T2 * -T1 -T2 // +#J #V1 #V2 #T1 #T2 #I #H destruct +qed. + +(* Basic_1: was: iso_gen_sort iso_gen_lref *) +lemma tstc_inv_atom1: ∀I,T2. ⓪{I} ≃ T2 → T2 = ⓪{I}. +/2 width=3/ qed-. + +fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≃ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 → + ∃∃W2,U2. T2 = ②{I}W2. U2. +#T1 #T2 * -T1 -T2 +[ #J #I #W1 #U1 #H destruct +| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/ +] +qed. + +(* Basic_1: was: iso_gen_head *) +lemma tstc_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≃ T2 → + ∃∃W2,U2. T2 = ②{I}W2. U2. +/2 width=5/ qed-. + +fact tstc_inv_atom2_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}. +#T1 #T2 * -T1 -T2 // +#J #V1 #V2 #T1 #T2 #I #H destruct +qed. + +lemma tstc_inv_atom2: ∀I,T1. T1 ≃ ⓪{I} → T1 = ⓪{I}. +/2 width=3/ qed-. + +fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≃ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 → + ∃∃W1,U1. T1 = ②{I}W1. U1. +#T1 #T2 * -T1 -T2 +[ #J #I #W2 #U2 #H destruct +| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3/ +] +qed. + +lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≃ ②{I}W2.U2 → + ∃∃W1,U1. T1 = ②{I}W1. U1. +/2 width=5/ qed-. + +(* Basic_1: removed theorems 2: + iso_flats_lref_bind_false iso_flats_flat_bind_false +*) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_tstc.ma new file mode 100644 index 000000000..a32d045b5 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_tstc.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/grammar/tstc.ma". + +(* SAME TOP TERM CONSTRUCTOR ************************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: iso_trans *) +theorem tstc_trans: ∀T1,T. T1 ≃ T → ∀T2. T ≃ T2 → T1 ≃ T2. +#T1 #T * -T1 -T // +#I #V1 #V #T1 #T #X #H +elim (tstc_inv_pair1 … H) -H #V2 #T2 #H destruct // +qed. + +theorem tstc_canc_sn: ∀T,T1. T ≃ T1 → ∀T2. T ≃ T2 → T1 ≃ T2. +/3 width=3/ qed. + +theorem tstc_canc_dx: ∀T1,T. T1 ≃ T → ∀T2. T2 ≃ T → T1 ≃ T2. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 08ff46477..7d05a2f67 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -112,6 +112,10 @@ notation "hvbox( L ⊢ break term 90 T1 ≈ break T2 )" non associative with precedence 45 for @{ 'Hom $L $T1 $T2 }. +notation "hvbox( T1 ≃ break T2 )" + non associative with precedence 45 + for @{ 'Iso $T1 $T2 }. + notation "hvbox( T1 break [ d , break e ] ≼ break T2 )" non associative with precedence 45 for @{ 'SubEq $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml index a90d256fe..2a2da2a5c 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml @@ -14,6 +14,7 @@ xoa xoa_notation basics/pts.ma + 1 2 2 1 2 2 2 3 diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma index 1ff53beb4..5a3a40024 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma @@ -16,6 +16,14 @@ include "basics/pts.ma". +(* multiple existental quantifier (1, 2) *) + +inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ + | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? +. + +interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). + (* multiple existental quantifier (2, 1) *) inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma index 80c20da30..edd014ef0 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma @@ -14,6 +14,16 @@ (* This file was generated by xoa.native: do not edit *********************) +(* multiple existental quantifier (1, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. + (* multiple existental quantifier (2, 1) *) notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)" diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index cbedfcbf6..a94fbd552 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1504,7 +1504,7 @@ let load_predefined_virtuals () = let predefined_classes = [ ["-"; "÷"; "⊢"; ]; - ["="; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; + ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "➾"; "⇨"; "➡"; "⇉"; "⥤"; "⥰"; ] ; ["⇑"; "⇧"; "⬆"; ] ; -- 2.39.2