From 488387490fb12d92f56ebcac2fc68d83a0d266ec Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 18 Sep 2019 18:39:16 +0200 Subject: [PATCH] update in static_2 + preorder on applicability domains + minor bug fixes --- .../lambdadelta/basic_2/dynamic/cnv_eval.ma | 2 +- .../lambdadelta/static_2/syntax/ac.ma | 16 ++++- .../lambdadelta/static_2/syntax/acle.ma | 58 +++++++++++++++++++ .../lambdadelta/static_2/syntax/acle_acle.ma | 26 +++++++++ .../lambdadelta/static_2/web/static_2_src.tbl | 1 + 5 files changed, 99 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma index efd2c3cce..d87201dad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma @@ -56,7 +56,7 @@ theorem cnv_dec (h) (a) (G) (L) (T): ac_props a → elim (dec_min (R_cpmuwe h G L T) … Hn) -Hn [| /2 width=2 by cnv_R_cpmuwe_dec/ ] #n0 #_ -n elim (ac_dec … Ha n0) -Ha - [ * #n #Hn #Ha * #X0 #HX0 #_ + [ * #n #Ha #Hn * #X0 #HX0 #_ elim (abst_dec X0) [ * #p #W #U0 #H destruct elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma index 1c411bb41..aef4c4452 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma @@ -17,7 +17,7 @@ include "static_2/notation/functions/one_0.ma". include "static_2/notation/functions/two_0.ma". include "static_2/notation/functions/omega_0.ma". -(* APPLICABILITY CONDITION *************************************************) +(* APPLICABILITY CONDITION **************************************************) (* applicability condition specification *) record ac: Type[0] ≝ { @@ -27,7 +27,7 @@ record ac: Type[0] ≝ { (* applicability condition postulates *) record ac_props (a): Prop ≝ { - ac_dec: ∀m. Decidable (∃∃n. m ≤ n & ad a n) + ac_dec: ∀m. Decidable (∃∃n. ad a n & m ≤ n) }. (* Notable specifications ***************************************************) @@ -54,6 +54,16 @@ interpretation "zero (applicability domain)" lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props …. #m elim (le_dec m k) #Hm [ /3 width=3 by or_introl, ex2_intro/ -| @or_intror * #n #Hmn #H destruct /2 width=1 by/ +| @or_intror * #n #Hn #Hmn destruct /2 width=1 by/ +] +qed. + +definition ac_le (k): ac ≝ mk_ac (λn. n ≤ k). + +lemma ac_le_props (k): ac_props (ac_le k) ≝ mk_ac_props …. +#m elim (le_dec m k) #Hm +[ /3 width=3 by or_introl, ex2_intro/ +| @or_intror * #n #Hn #Hmn + /3 width=3 by transitive_le/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma new file mode 100644 index 000000000..30a025356 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/ac.ma". + +(* APPLICABILITY CONDITION PREORDER *****************************************) + +definition acle: relation ac ≝ + λa1,a2. ∀m. ad a1 m → ∃∃n. ad a2 n & m ≤ n. + +interpretation "preorder (applicability domain)" + 'subseteq a1 a2 = (acle a1 a2). + +(* Basic properties *********************************************************) + +lemma acle_refl: reflexive … acle. +/2 width=3 by ex2_intro/ qed. + +lemma acle_omega (a): a ⊆ 𝛚. +/2 width=1 by acle_refl/ +qed. + +lemma acle_one (a): ∀n. ad a n → 𝟏 ⊆ a. +#a #n #Ha #m #Hm destruct +/2 width=3 by ex2_intro/ +qed. + +lemma acle_eq_monotonic_le (k1) (k2): + k1 ≤ k2 → (ac_eq k1) ⊆ (ac_eq k2). +#k1 #k2 #Hk #m #Hm destruct +/2 width=3 by ex2_intro/ +qed. + +lemma acle_le_monotonic_le (k1) (k2): + k1 ≤ k2 → (ac_le k1) ⊆ (ac_le k2). +#k1 #k2 #Hk #m #Hm +/3 width=3 by acle_refl, transitive_le/ +qed. + +lemma acle_eq_le (k): (ac_eq k) ⊆ (ac_le k). +#k #m #Hm destruct +/2 width=1 by acle_refl, le_n/ +qed. + +lemma acle_le_eq (k): (ac_le k) ⊆ (ac_eq k). +#k #m #Hm /2 width=3 by ex2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma new file mode 100644 index 000000000..9b8998900 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/acle.ma". + +(* APPLICABILITY CONDITION PREORDER *****************************************) + +(* Main properties **********************************************************) + +theorem acle_trans: Transitive … acle. +#a1 #a #Ha1 #a2 #Ha2 #m1 #Hm1 +elim (Ha1 … Hm1) -Ha1 -Hm1 #m #Ha #Hm1 +elim (Ha2 … Ha) -Ha2 -Ha #m2 #Ha2 #Hm2 +/3 width=5 by transitive_le, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index db531a271..0a962c3f8 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -103,6 +103,7 @@ table { class "red" [ { "syntax" * } { [ { "applicability condition" * } { + [ [ "preorder" ] "acle" + "( ? ⊆ ? )" "acle_acle" * ] [ [ "properties" ] "ac" + "( 𝟏 )" + "( 𝟐 )" + "( 𝛚 )" * ] } ] -- 2.39.2