pack-ground pack-2a pack-2b \
home up-home \
-PACKAGES := ground basic_2A static_2 basic_2 apps_2 alpha_1
+PACKAGES := ground basic_2A static_2 basic_2 apps_2 alpha_1 delayed_updating
LDWS := $(shell find -name "*.ldw.xml")
TBLS := $(shell find -name "*.tbl")
--- /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( ↥[ term 46 t1 ] break term 75 t2 )"
+ non associative with precedence 75
+ for @{ 'BarUpArrow $t1 $t2 }.
--- /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( ↥❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+ non associative with precedence 75
+ for @{ 'BarUpArrow $S $k $p $f }.
+
+notation > "hvbox( ↥❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+ non associative with precedence 75
+ for @{ 'BarUpArrow ? $k $p $f }.
+
+notation > "hvbox( ↥{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
+ non associative with precedence 75
+ for @{ 'BarUpArrow $S $k $p $f }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( @ break term 76 u. break term 75 t )"
+notation "hvbox( @ break term 76 u . break term 75 t )"
non associative with precedence 75
for @{ 'At $u $t }.
+++ /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( hd ◖ break tl )"
- left associative with precedence 47
- for @{ 'BlackHalfCircleLeft $hd $tl }.
+++ /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( hd ◗ break tl )"
- right associative with precedence 47
- for @{ 'BlackHalfCircleRight $hd $tl }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( 𝛌 . break term 75 t )"
+notation "hvbox( 𝛌. break term 75 t )"
non associative with precedence 75
for @{ 'Lamda $t }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( ↑ [ term 46 t1 ] break term 75 t2 )"
+notation "hvbox( ↑[ term 46 t1 ] break term 75 t2 )"
non associative with precedence 75
for @{ 'UpArrow $t1 $t2 }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation < "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+notation < "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )"
non associative with precedence 75
for @{ 'UpArrow $S $k $p $f }.
-notation > "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+notation > "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )"
non associative with precedence 75
for @{ 'UpArrow ? $k $p $f }.
-notation > "hvbox( ↑ { term 46 S } ❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
+notation > "hvbox( ↑{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
non associative with precedence 75
for @{ 'UpArrow $S $k $p $f }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( t1 ➡ 'd' 'f' [ break term 46 p, break term 46 q ] break term 46 t2 )"
+notation "hvbox( t1 ➡'d''f'[ break term 46 p, break term 46 q ] break term 46 t2 )"
non associative with precedence 45
for @{ 'BlackRightArrow $t1 $p $q $t2 }.
(* *)
(**************************************************************************)
-include "ground/xoa/ex_3_1.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/substitution/fsubst.ma".
(* LIFT FOR PATH ***********************************************************)
+definition lift_continuation (A:Type[0]) ≝
+ path → tr_map → A.
+
(* Note: inner numeric labels are not liftable, so they are removed *)
-rec definition lift_gen (A:Type[0]) (k:?→?→A) (p) (f) on p ≝
+rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ≝
match p with
[ list_empty ⇒ k 𝐞 f
| list_lcons l q ⇒
(* Basic constructions ******************************************************)
-lemma lift_L (A) (k) (p) (f):
+lemma lift_empty (A) (k) (f):
+ k 𝐞 f = ↑{A}❨k, 𝐞, f❩.
+// qed.
+
+lemma lift_d_empty_sn (A) (k) (n) (f):
+ ↑❨(λp. k (𝗱❨f@❨n❩❩◗p)), 𝐞, f❩ = ↑{A}❨k, 𝗱❨n❩◗𝐞, f❩.
+// qed.
+
+lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f):
+ ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱❨n❩◗l◗p, f❩.
+// qed.
+
+lemma lift_L_sn (A) (k) (p) (f):
↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩.
// qed.
-(* Basic constructions with proj_path ***************************************)
-
-lemma lift_append (p) (f) (q):
- q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
-#p elim p -p
-[ //
-| #l #p #IH #f #q cases l
- [
- | <lift_L in ⊢ (???%);
- >(list_append_rcons_sn ? q) in ⊢ (???(??(λ_.%)??));
-
- <IH
- normalize >IH
- | //
-
-(* Constructions with append ************************************************)
-
-theorem lift_append_A (p2) (p1) (f):
- (↑[f]p1)●𝗔◗↑[↑[p1]f]p2 = ↑[f](p1●𝗔◗p2).
-#p2 #p1 elim p1 -p1
-[ #f normalize
+lemma lift_A_sn (A) (k) (p) (f):
+ ↑❨(λp. k (𝗔◗p)), p, f❩ = ↑{A}❨k, 𝗔◗p, f❩.
+// qed.
+
+lemma lift_S_sn (A) (k) (p) (f):
+ ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩.
+// 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/substitution/lift.ma".
+include "ground/notation/relations/ringeq_3.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝
+ λk1,k2. ∀p,f. k1 p f = k2 p f.
+
+interpretation
+ "extensional equivalence (lift continuation)"
+ 'RingEq A k1 k2 = (lift_exteq A k1 k2).
+
+(* Constructions with lift_exteq ********************************************)
+
+lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
+ k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩.
+#A #p elim p -p
+[ #k1 #k2 #f #Hk <lift_empty <lift_empty //
+| * [ #n * [| #l0 ]] [|*: #q ] #IH #k1 #k2 #f #Hk /2 width=1 by/
+]
+qed-.
+
+(* Advanced constructions ***************************************************)
+
+lemma lift_lcons_alt (A) (k) (f) (p) (l):
+ ↑❨λp2.k(l◗p2),p,f❩ = ↑{A}❨λp2.k((l◗𝐞)●p2),p,f❩.
+#A #k #f #p #l
+@lift_eq_repl_sn #p2 #g // (**) (* auto fails with typechecker failure *)
+qed.
+
+lemma lift_append_rcons_sn (A) (k) (f) (p1) (p) (l):
+ ↑❨λp2.k(p1●l◗p2),p,f❩ = ↑{A}❨λp2.k(p1◖l●p2),p,f❩.
+#A #k #f #p1 #p #l
+@lift_eq_repl_sn #p2 #g
+<list_append_rcons_sn //
+qed.
+
+(* Basic constructions with proj_path ***************************************)
+
+lemma lift_append_sn (p) (f) (q):
+ q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
+#p elim p -p
+[ //
+| * [ #n * [| #l ]] [|*: #p ] #IH #f #q
+ [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+ | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+ | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+ | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+ | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+ ]
+]
+qed.
+
+lemma lift_lcons (f) (p) (l):
+ l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
+#f #p #l
+>lift_lcons_alt <lift_append_sn //
+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_structure.ma".
+include "delayed_updating/substitution/lift_eq.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Constructions with structure ********************************************)
+
+lemma lift_d_empty_dx (n) (p) (f):
+ (⊗p)◖𝗱❨(↑[p◖𝗱❨n❩]f)@❨n❩❩ = ↑[f](p◖𝗱❨n❩).
+#n #p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| <list_cons_shift <list_cons_comm <list_cons_comm //
+| <lift_d_lcons_sn <lift_d_lcons_sn //
+| <lift_L_sn <lift_L_sn <lift_lcons <IH //
+| <lift_A_sn <lift_A_sn <lift_lcons <IH //
+| <lift_S_sn <lift_S_sn <lift_lcons <IH //
+]
+qed.
+
+lemma lift_L_dx (p) (f):
+ (⊗p)◖𝗟 = ↑[f](p◖𝗟).
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| <lift_d_lcons_sn //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma lift_A_dx (p) (f):
+ (⊗p)◖𝗔 = ↑[f](p◖𝗔).
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| <lift_d_lcons_sn //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma lift_S_dx (p) (f):
+ (⊗p)◖𝗦 = ↑[f](p◖𝗦).
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| <lift_d_lcons_sn //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma structure_lift (p) (f):
+ ⊗p = ⊗↑[f]p.
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma lift_structure (p) (f):
+ ⊗p = ↑[f]⊗p.
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| //
+| <structure_L_sn <lift_L_sn <lift_lcons //
+| <structure_A_sn <lift_A_sn <lift_lcons //
+| <structure_S_sn <lift_S_sn <lift_lcons //
+]
+qed.
include "ground/lib/list_rcons.ma".
include "ground/notation/functions/element_e_0.ma".
include "ground/notation/functions/black_circle_2.ma".
+include "ground/notation/functions/black_halfcircleright_2.ma".
+include "ground/notation/functions/black_halfcircleleft_2.ma".
include "delayed_updating/syntax/label.ma".
-include "delayed_updating/notation/functions/black_halfcircleright_2.ma".
-include "delayed_updating/notation/functions/black_halfcircleleft_2.ma".
(* PATH *********************************************************************)
(* STRUCTURE FOR PATH *******************************************************)
-rec definition path_structure (p) on p ≝
+rec definition structure (p) on p ≝
match p with
[ list_empty ⇒ 𝐞
| list_lcons l q ⇒
match l with
- [ label_node_d n ⇒ path_structure q
- | label_edge_L ⇒ 𝗟◗path_structure q
- | label_edge_A ⇒ 𝗔◗path_structure q
- | label_edge_S ⇒ 𝗦◗path_structure q
+ [ label_node_d n ⇒ structure q
+ | label_edge_L ⇒ 𝗟◗structure q
+ | label_edge_A ⇒ 𝗔◗structure q
+ | label_edge_S ⇒ 𝗦◗structure q
]
].
interpretation
"structure (path)"
- 'CircledTimes p = (path_structure p).
+ 'CircledTimes p = (structure p).
+
+(* Basic constructions ******************************************************)
+
+lemma structure_empty:
+ 𝐞 = ⊗𝐞.
+// qed.
+
+lemma structure_d_sn (p) (n):
+ ⊗p = ⊗(𝗱❨n❩◗p).
+// qed.
+
+lemma structure_L_sn (p):
+ 𝗟◗⊗p = ⊗(𝗟◗p).
+// qed.
+
+lemma structure_A_sn (p):
+ 𝗔◗⊗p = ⊗(𝗔◗p).
+// qed.
+
+lemma structure_S_sn (p):
+ 𝗦◗⊗p = ⊗(𝗦◗p).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem structure_idem (p):
+ ⊗p = ⊗⊗p.
+#p elim p -p [| * [ #n ] #p #IH ] //
+qed.
+
+theorem structure_append (p1) (p2):
+ ⊗p1●⊗p2 = ⊗(p1●p2).
+#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+[||*: <list_append_lcons_sn ] //
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma structure_d_dx (p) (n):
+ ⊗p = ⊗(p◖𝗱❨n❩).
+#p #n <structure_append //
+qed.
+
+lemma structure_L_dx (p):
+ (⊗p)◖𝗟 = ⊗(p◖𝗟).
+#p <structure_append //
+qed.
+
+lemma structure_A_dx (p):
+ (⊗p)◖𝗔 = ⊗(p◖𝗔).
+#p <structure_append //
+qed.
+
+lemma structure_S_dx (p):
+ (⊗p)◖𝗦 = ⊗(p◖𝗦).
+#p <structure_append //
+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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( hd ◖ break tl )"
+ left associative with precedence 47
+ for @{ 'BlackHalfCircleLeft $hd $tl }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( hd ◗ break tl )"
+ right associative with precedence 47
+ for @{ 'BlackHalfCircleRight $hd $tl }.
projects / helm.git / commitdiff