From: Ferruccio Guidi Date: Thu, 29 Oct 2015 22:46:45 +0000 (+0000) Subject: - matita: computed auto traces now include the "width" parameter X-Git-Tag: make_still_working~676 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8cd6cc85182245df447a21caf16b6503fa4b3e5;p=helm.git - matita: computed auto traces now include the "width" parameter more characters for use with lambdadelta - ground_2: advances in relocation by trace --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma new file mode 100644 index 000000000..a10c80f17 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( ∁ term 70 t )" + non associative with precedence 70 + for @{ 'Complement $t }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_1.ma deleted file mode 100644 index eb11c1545..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_1.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) - -notation "hvbox( 𝐈 ⦃ term 46 f ⦄ )" - non associative with precedence 45 - for @{ 'IsId $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isidentity_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isidentity_1.ma new file mode 100644 index 000000000..f4cc5d7da --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isidentity_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( 𝐈 ⦃ term 46 f ⦄ )" + non associative with precedence 45 + for @{ 'IsIdentity $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma new file mode 100644 index 000000000..349f2b3bf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )" + non associative with precedence 45 + for @{ 'IsUniform $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma index 0fd397829..02d8ac1eb 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma @@ -139,7 +139,7 @@ lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 #cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/ qed-. -lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥. +lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥. #cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma index d87487c89..6dce9e0a2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma @@ -12,15 +12,19 @@ (* *) (**************************************************************************) -include "ground_2/notation/relations/isid_1.ma". +include "ground_2/notation/relations/isidentity_1.ma". include "ground_2/relocation/trace_after.ma". +include "ground_2/relocation/trace_sle.ma". (* RELOCATION TRACE *********************************************************) definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|. interpretation "test for identity (trace)" - 'IsId cs = (isid cs). + 'IsIdentity cs = (isid cs). + +definition t_reflexive: ∀S:Type[0]. predicate (trace → relation S) ≝ + λS,R. ∀a. ∃∃t. 𝐈⦃t⦄ & R t a a. (* Basic properties *********************************************************) @@ -98,3 +102,13 @@ lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1 | #t1 #t2 #t #_ #_ #H elim (isid_inv_false … H) ] qed-. + +(* Forward on inclusion *****************************************************) + +lemma sle_isid1_fwd: ∀t1,t2. t1 ⊆ t2 → 𝐈⦃t1⦄ → t1 = t2. +#t1 #t2 #H elim H -t1 -t2 // +[ #t1 #t2 #_ #IH #H lapply (isid_inv_true … H) -H + #HT1 @eq_f2 // @IH @HT1 (**) (* full auto fails *) +| #t1 #t2 #b #_ #_ #H elim (isid_inv_false … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma new file mode 100644 index 000000000..bdcb249c5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/notation/relations/isuniform_1.ma". +include "ground_2/relocation/trace_isid.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive isun: predicate trace ≝ +| isun_id : ∀t. 𝐈⦃t⦄ → isun t +| isun_false: ∀t. isun t → isun (Ⓕ@t) +. + +interpretation "test for uniformity (trace)" + 'IsUniform t = (isun t). + +(* Basic inversion lennas ***************************************************) + +fact isun_inv_true_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓣ@u → 𝐈⦃u⦄. +#t * -t +[ #t #Ht #u #H destruct /2 width=1 by isid_inv_true/ +| #t #_ #u #H destruct +] +qed-. + +lemma isun_inv_true: ∀t. 𝐔⦃Ⓣ@t⦄ → 𝐈⦃t⦄. +/2 width=3 by isun_inv_true_aux/ qed-. + +fact isun_inv_false_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓕ@u → 𝐔⦃u⦄. +#t * -t +[ #t #Ht #u #H destruct elim (isid_inv_false … Ht) +| #t #Ht #u #H destruct // +] +qed-. + +lemma isun_inv_false: ∀t. 𝐔⦃Ⓕ@t⦄ → 𝐔⦃t⦄. +/2 width=3 by isun_inv_false_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma new file mode 100644 index 000000000..be738b18e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/relocation/trace_at.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive sle: relation trace ≝ +| sle_empty: sle (◊) (◊) +| sle_true : ∀t1,t2. sle t1 t2 → sle (Ⓣ @ t1) (Ⓣ @ t2) +| sle_false: ∀t1,t2,b. sle t1 t2 → sle (Ⓕ @ t1) (b @ t2) +. + +interpretation + "inclusion (trace)" + 'subseteq t1 t2 = (sle t1 t2). + +(* Basic properties *********************************************************) + +(* Basic forward lemmas *****************************************************) + +lemma sle_fwd_length: ∀t1,t2. t1 ⊆ t2 → |t1| = |t2|. +#t1 #t2 #H elim H -t1 -t2 // +qed-. + +lemma sle_fwd_colength: ∀t1,t2. t1 ⊆ t2 → ∥t1∥ ≤ ∥t2∥. +#t1 #t2 #H elim H -t1 -t2 /2 width=1 by le_S_S/ +#t1 #t2 * /2 width=1 by le_S/ +qed-. + +(* Inversion lemmas on application ******************************************) + +lemma sle_inv_at: ∀t1,t2. t1 ⊆ t2 → + ∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i2 ≤ i1. +#t1 #t2 #H elim H -t1 -t2 +[ #i #i1 #i2 #_ #H2 elim (at_inv_empty … H2) -H2 // +| #t1 #t2 #_ #IH #i #i1 #i2 #H0 #H2 elim (at_inv_true … H2) -H2 * // + #j1 #j2 #H1 #H2 #Hj destruct elim (at_inv_true_succ_sn … H0) -H0 + /3 width=3 by le_S_S/ +| #t1 #t2 * #_ #IH #i #i1 #i2 #H0 #H2 + [ elim (at_inv_true … H2) -H2 * // + #j #j2 #H1 #H2 #Hj2 destruct elim (at_inv_false … H0) -H0 + #j1 #H #Hj1 destruct elim (at_monotonic … Hj1 j) -Hj1 // + #x #H1x #H2x @le_S_S /4 width=3 by lt_to_le, le_to_lt_to_lt/ (**) (* full auto too slow *) + | elim (at_inv_false … H2) elim (at_inv_false … H0) -H0 -H2 + /3 width=3 by le_S_S/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma new file mode 100644 index 000000000..d1697b9cc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.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 "ground_2/notation/functions/complement_1.ma". +include "ground_2/relocation/trace.ma". + +(* RELOCATION TRACE *********************************************************) + +let rec snot (t:trace) on t ≝ match t with +[ nil ⇒ ◊ +| cons b t ⇒ (¬ b) @ snot t +]. + +interpretation + "complement (trace)" + 'Complement t = (snot t). + +(* Basic properties *********************************************************) + +lemma snot_empty: ∁ (◊) = ◊. +// qed. + +lemma snot_inh: ∀t,b. ∁ (b@t) = (¬ b) @ ∁ t. +// qed. + +lemma snot_true: ∀t. ∁ (Ⓣ @ t) = Ⓕ @ ∁ t. +// qed. + +lemma snot_false: ∀t. ∁ (Ⓕ @ t) = Ⓣ @ ∁ t. +// qed. + +lemma snot_length: ∀t. |∁ t| = |t|. +#t elim t -t normalize // +qed. + +lemma snot_colength: ∀t. ∥∁ t∥ = |t| - ∥t∥. +#t elim t -t // +* /2 width=1 by minus_Sn_m/ +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index f23379992..5f3edcf09 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -12,7 +12,8 @@ table { class "green" [ { "multiple relocation" * } { [ { "" * } { - [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_sor ( ? ⋓ ? ≡ ? )" * ] + [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" + "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ] } ] diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index cb443ae46..de78194f0 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -145,7 +145,11 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse try List.assoc "depth" a with Not_found -> "" in - let trace = "/"^(if int_of_string depth > 1 then depth else "")^" by " in + let width = + try List.assoc "width" a + with Not_found -> "" + in + let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in let thms = match !trace_ref with | [] -> "" diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 7d0ab3a8e..5a80b945f 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,8 +1503,9 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ - ["&"; "⅋"; ]; - ["!"; "¡"; "⫯"; "⫰"; ]; + ["&"; "⅋"; ]; + ["|"; "∥"; ]; + ["!"; "¡"; "⫯"; "⫰"; ]; ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ];