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 (file)
index 0000000..c65fcbc
--- /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 (file)
index 0000000..d2be3b3
--- /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 37a2b26186e814e70e9fb5e966bd7294dcfaf013..fd3b4086a933c1ec5421404dcd2be86e2471ba67 100644 (file)
--- 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 "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/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 ************************************************)
 
 
 (* CLOSED CONDITION FOR PATH ************************************************)
 


@@ -180,6 +180,36 @@ theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n):
 ]
 qed.
 
 ]
 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):
 (* 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 (file)
index 0000000..af57be3
--- /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 (file)
index 0000000..65bb510
--- /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 (file)
index 0000000..8092cf8
--- /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 e4c3d743e2d17273430c19d9672a86fe3bd7a70c..6b5eb992a7b64e5c932ff950b8ca00f4b8a7e29c 100644 (file)
--- 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-.
 #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-.