--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
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 ************************************************)
]
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):
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
#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-.
projects / helm.git / commitdiff