From: Ferruccio Guidi Date: Wed, 23 Nov 2022 08:33:26 +0000 (+0100) Subject: wip in delayed_updating X-Git-Tag: make_still_working~24 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e6ef5581641345f1c5c72f3c8b6040a9c6e5aecb wip in delayed_updating guard condition --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.ma new file mode 100644 index 000000000..c65fcbc5d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( 𝐆 )" + non associative with precedence 70 + for @{ 'ClassG }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma new file mode 100644 index 000000000..d2be3b32f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/substitution/lift_path.ma". +include "delayed_updating/syntax/path_guard.ma". + +(* LIFT FOR PATH ************************************************************) + +(* Constructions with pgc ***************************************************) + +lemma lift_path_guard (f) (p): + p ϵ 𝐆 → 🠡[f]p ϵ 𝐆. +#f #p #H0 elim H0 -p // +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma index 37a2b2618..fd3b4086a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma @@ -14,11 +14,11 @@ include "delayed_updating/syntax/path.ma". include "delayed_updating/notation/functions/class_c_2.ma". -include "ground/arith/nat_plus.ma". -include "ground/arith/nat_pred_succ.ma". +include "ground/arith/nat_plus_pred.ma". include "ground/lib/subset.ma". include "ground/lib/bool_and.ma". include "ground/generated/insert_eq_1.ma". +include "ground/xoa/ex_3_2.ma". (* CLOSED CONDITION FOR PATH ************************************************) @@ -180,6 +180,36 @@ theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n): ] qed. +(* Inversions with path_append **********************************************) + +lemma pcc_false_inv_append_bi (x) (m) (n): + x ϵ 𝐂❨Ⓕ,m+n❩ → + ∃∃p,q. p ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & p●q = x. +#x #m #n #Hx +@(insert_eq_1 … (m+n) … Hx) -Hx #y #Hy +generalize in match n; -n +generalize in match m; -m +elim Hy -x -y [|*: #x #y [ #k #_ ] #Hx #IH ] #m #n #Hy destruct +[ elim (eq_inv_nplus_zero … Hy) -Hy #H1 #H2 destruct + /2 width=5 by pcc_empty, ex3_2_intro/ +| elim (IH m (n+k)) -IH // #p #q #Hp #Hq #H0 destruct -Hx + /3 width=5 by pcc_false_d_dx, ex3_2_intro/ +| elim (IH m n) -IH // #p #q #Hp #Hq #H0 destruct -Hx + /3 width=5 by pcc_m_dx, ex3_2_intro/ +| elim (eq_inv_succ_nplus_dx … (sym_eq … Hy)) -Hy * #H1 #H2 (**) (* sym_eq *) + [ destruct -IH + /3 width=5 by pcc_empty, pcc_L_dx, ex3_2_intro/ + | elim (IH m (↓n)) -IH // #p #q #Hp #Hq #H0 destruct -Hx + /3 width=5 by pcc_L_dx, ex3_2_intro/ + ] +| elim (IH m n) -IH // #p #q #Hp #Hq #H0 destruct -Hx + /3 width=5 by pcc_A_dx, ex3_2_intro/ +| elim (IH m n) -IH // #p #q #Hp #Hq #H0 destruct -Hx + /3 width=5 by pcc_S_dx, ex3_2_intro/ +] +qed-. + + (* Constructions with path_lcons ********************************************) lemma pcc_m_sn (o) (q) (n): diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma new file mode 100644 index 000000000..af57be335 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path_closed.ma". +include "delayed_updating/syntax/path_guard.ma". + +(* CLOSED CONDITION FOR PATH ************************************************) + +axiom list_ind_pippo (A) (Q:predicate …): + (∀l. (∀m. (∃p. p⨁{A}m = l) → Q m) → Q l) → ∀l. Q l. + +(* Destructions with pgc ****************************************************) + +lemma path_closed_des_guard (x) (n): + x ϵ 𝐂❨Ⓕ,n❩ → + ∃∃p,q. p ϵ 𝐆 & q ϵ 𝐂❨Ⓕ,𝟎❩ & p●q = x. +#x @(list_ind_pippo … x) -x +#x #IH #n #H0 @(insert_eq_1 … x … H0) -H0 +#y * -y -n +[|*: #y #n [ #k #_ ] #Hy ] #H0 destruct +[ /2 width=5 by pgc_empty, pcc_empty, ex3_2_intro/ +| elim (pcc_false_inv_append_bi … Hy) -Hy #r #s #Hr #Hs #H0 destruct + elim (IH … Hr) -IH -Hr [| /2 width=2 by ex_intro/ ] + #p #q #Hp #Hq #H0 destruct + @(ex3_2_intro … Hp) -Hp [1,3: // ] + /3 width=2 by pcc_append_bi, pcc_false_d_dx/ +| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ] + #p #q #Hp #Hq #H0 destruct + /3 width=5 by pcc_m_dx, ex3_2_intro/ +| @(ex3_2_intro … (y◖𝗟) (𝐞)) // +| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ] + #p #q #Hp #Hq #H0 destruct + /3 width=5 by pcc_A_dx, ex3_2_intro/ +| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ] + #p #q #Hp #Hq #H0 destruct + /3 width=5 by pcc_S_dx, ex3_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma new file mode 100644 index 000000000..65bb51044 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path.ma". +include "delayed_updating/notation/functions/class_g_0.ma". +include "ground/lib/subset.ma". + +(* GUARD CONDITION FOR PATH *************************************************) + +inductive pgc: predicate path ≝ +| pgc_empty: (𝐞) ϵ pgc +| pgc_L_dx (p): p◖𝗟 ϵ pgc +. + +interpretation + "guard condition (path)" + 'ClassG = (pgc). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma new file mode 100644 index 000000000..8092cf8e3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path_guard.ma". +include "delayed_updating/syntax/path_structure.ma". + +(* GUARD CONDITION FOR PATH *************************************************) + +(* Constructions with structure *********************************************) + +lemma path_guard_structure (p): + p ϵ 𝐆 → ⊗p ϵ 𝐆. +#p #H0 elim H0 -p // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma index e4c3d743e..6b5eb992a 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma @@ -96,3 +96,12 @@ lemma list_ind_append_dx (A) (Q:predicate …): #a #l >(list_append_empty_sn … (a⨮l)) /2 width=1 by/ qed-. + +lemma list_ind_append_sn (A) (Q:predicate …): + Q (ⓔ{A}) → + (∀l1,l2. Q l2 -> Q (l1⨁l2)) → + ∀l. Q l. +#A #Q #IH1 #IH2 * // +#a #l >(list_append_empty_dx … (a⨮l)) +/2 width=1 by/ +qed-.