--- /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 n ] break term 70 p )"
+ non associative with precedence 70
+ for @{ 'DownArrowRightSharp $n $p }.
--- /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_labels.ma".
+include "delayed_updating/notation/functions/downarrowrightsharp_2.ma".
+include "ground/arith/pnat_plus.ma".
+
+(* HEAD BY DEPTH FOR PATH ***************************************************)
+
+rec definition path_dhd (m) (p) on p: path ≝
+match p with
+[ list_empty ⇒ 𝗟∗∗m
+| list_lcons l q ⇒
+ match l with
+ [ label_d n ⇒ l◗(path_dhd (m+n) q)
+ | label_m ⇒ l◗(path_dhd m q)
+ | label_L ⇒
+ match m with
+ [ punit ⇒ l◗𝐞
+ | psucc o ⇒ l◗(path_dhd o q)
+ ]
+ | label_A ⇒ l◗(path_dhd m q)
+ | label_S ⇒ l◗(path_dhd m q)
+ ]
+].
+
+interpretation
+ "head by depth (reversed path)"
+ 'DownArrowRightSharp n p = (path_dhd n p).
+
+(* basic constructions ****************************************************)
+
+lemma path_dhd_empty (n:pnat):
+ (𝗟∗∗n) = ↳⧣[n]𝐞.
+// qed.
+
+lemma path_dhd_d_sn (p) (n) (m):
+ (𝗱m◗↳⧣[n+m]p) = ↳⧣[n](𝗱m◗p).
+// qed.
+
+lemma path_dhd_m_sn (p) (n):
+ (𝗺◗↳⧣[n]p) = ↳⧣[n](𝗺◗p).
+// qed.
+
+lemma path_dhd_L_sn_unit (p):
+ (𝗟◗𝐞) = ↳⧣[𝟏](𝗟◗p).
+// qed.
+
+lemma path_dhd_L_sn_succ (p) (n):
+ (𝗟◗↳⧣[n]p) = ↳⧣[↑n](𝗟◗p).
+// qed.
+
+lemma path_dhd_A_sn (p) (n):
+ (𝗔◗↳⧣[n]p) = ↳⧣[n](𝗔◗p).
+// qed.
+
+lemma path_dhd_S_sn (p) (n):
+ (𝗦◗↳⧣[n]p) = ↳⧣[n](𝗦◗p).
+// 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_dhd.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+
+(* HEAD BY DEPTH FOR PATH ***************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma path_dhd_structure_L_sn (p) (q):
+ let r ≝ 𝗟◗p in
+ ⊗r = ↳⧣[♭⊗r]((⊗r)●q).
+#p elim p -p //
+* [ #n ] #p #IH #q //
+ [ <structure_L_sn //
+ | <structure_A_sn <list_append_lcons_sn
+ <path_head_A_sn //
+ | <structure_S_sn //
+ ]
+]
+*)
\ No newline at end of file
#f #p #q #t1 #t2 #H0t1
* #n * #H1n #Ht1 #Ht2
@(ex_intro … (↑♭⊗q)) @and3_intro
-[ -H0t1 -H1n -Ht1 -Ht2
- >list_append_rcons_sn <reverse_append
- >nsucc_unfold >depth_reverse >depth_L_dx >reverse_lcons
+[ -H0t1 -Ht1 -Ht2
>structure_L_sn >structure_reverse
- <path_head_structure //
+ >H1n >path_head_structure_depth <H1n -H1n //
| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
<unwind2_path_d_dx <depth_structure
>list_append_rcons_sn in H1n; <reverse_append #H1n
(**************************************************************************)
include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/syntax/path_depth_labels.ma".
include "delayed_updating/syntax/path_height_labels.ma".
+include "delayed_updating/syntax/path_depth_labels.ma".
(* HEAD FOR PATH ************************************************************)
| <path_head_A_sn <height_A_sn <depth_A_sn //
| <path_head_S_sn <height_S_sn <depth_S_sn //
]
-qed.
+qed-. (**) (* gets in the way with auto *)
(* *)
(**************************************************************************)
-include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_depth.ma".
+include "delayed_updating/syntax/path_head_depth.ma".
+include "delayed_updating/syntax/path_structure_labels.ma".
(* HEAD FOR PATH ************************************************************)
(* Constructions with structure *********************************************)
-axiom path_head_structure (p) (q):
- ⊗p = ↳[♭⊗p]((⊗p)●q).
-(*
-#p elim p -p
-[ #q <path_head_zero //
-| * [ #n ] #p #IH #q
- [ <structure_d_sn //
- | <structure_m_sn //
- | <structure_L_sn
- | <structure_A_sn <list_append_lcons_sn
- <path_head_A_sn //
- | <structure_S_sn //
- ]
+lemma path_head_structure_height (p) (m):
+ ⊗↳[m]p = ↳[m+♯↳[m]p]⊗p.
+#p elim p -p //
+#l #p #IH #m @(nat_ind_succ … m) -m //
+#m #_ cases l [ #n ]
+[ <height_d_sn <structure_d_sn //
+| <structure_m_sn //
+| <structure_L_sn //
+| <height_A_sn <structure_A_sn <nplus_succ_sn <path_head_A_sn //
+| <height_S_sn <structure_S_sn <nplus_succ_sn <path_head_S_sn //
]
-*)
\ No newline at end of file
+qed.
+
+lemma path_head_structure_depth (p) (m):
+ ⊗↳[m]p = ↳[♭↳[m]p]⊗p.
+#p #m
+<path_head_depth //
+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/syntax/path_labels.ma".
+
+(* STRUCTURE FOR PATH *******************************************************)
+
+(* Constructions with labels ************************************************)
+
+lemma structure_labels_L (n):
+ (𝗟∗∗n) = ⊗(𝗟∗∗n).
+#n @(nat_ind_succ … n) -n //
+qed.
+++ /dev/null
-include "ground/relocation/tr_uni_pap.ma".
-include "ground/relocation/tr_compose_pap.ma".
-include "ground/notation/functions/applysucc_2.ma".
-include "ground/arith/nat_lt.ma".
-include "ground/arith/nat_plus_rplus.ma".
-include "ground/arith/nat_pred_succ.ma".
-
-lemma nlt_npsucc_bi (n1) (n2):
- n1 < n2 → npsucc n1 < npsucc n2.
-#n1 #n2 #Hn elim Hn -n2 //
-#n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
-qed.
-
-definition tr_nap (f) (l:nat): nat ≝
- ↓(f＠⧣❨↑l❩).
-
-interpretation
- "functional non-negative application (total relocation maps)"
- 'ApplySucc f l = (tr_nap f l).
-
-lemma tr_nap_unfold (f) (l):
- ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
-// qed.
-
-lemma tr_compose_nap (f2) (f1) (l):
- f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
-#f2 #f1 #l
-<tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
-<tr_compose_pap <npsucc_pred //
-qed.
-
-lemma tr_uni_nap (n) (m):
- m + n = 𝐮❨n❩@↑❨m❩.
-#n #m
-<tr_nap_unfold
-<tr_uni_pap <nrplus_npsucc_sn //
-qed.
-
-lemma tr_nap_push (f):
- ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
-#f #l
-<tr_nap_unfold <tr_nap_unfold
-<tr_pap_push <pnpred_psucc //
-qed.
-
-lemma tr_nap_pushs_lt (f) (n) (m):
- m < n → m = (⫯*[n]f)@↑❨m❩.
-#f #n #m #Hmn
-<tr_nap_unfold <tr_pap_pushs_le
-/2 width=1 by nlt_npsucc_bi/
-qed-.
include "delayed_updating/unwind/unwind2_rmap_labels.ma".
include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-include "delayed_updating/unwind/xap.ma".
include "delayed_updating/syntax/path_head_depth.ma".
+include "ground/relocation/xap.ma".
include "ground/lib/stream_eq_eq.ma".
include "ground/arith/nat_le_plus.ma".
♭p = ninj (▶[f](p●q)＠⧣❨n❩).
#f #p #q #n #Hn
>tr_xap_ninj >Hn in ⊢ (??%?);
->(unwind2_rmap_head_append_xap_closed … Hn) -Hn //
+>(unwind2_rmap_head_append_xap_closed … Hn) -Hn
+<path_head_depth //
qed.
lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (k):
+++ /dev/null
-include "delayed_updating/unwind/nap.ma".
-include "ground/notation/functions/apply_2.ma".
-include "ground/relocation/tr_compose_pn.ma".
-
-definition tr_xap (f) (l:nat): nat ≝
- (⫯f)@↑❨l❩.
-
-interpretation
- "functional extended application (total relocation maps)"
- 'Apply f l = (tr_xap f l).
-
-lemma tr_xap_unfold (f) (l):
- (⫯f)@↑❨l❩ = f＠❨l❩.
-// qed.
-
-lemma tr_xap_zero (f):
- (𝟎) = f＠❨𝟎❩.
-// qed.
-
-lemma tr_xap_ninj (f) (p):
- ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
-// qed.
-
-lemma tr_compose_xap (f2) (f1) (l):
- f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
-#f2 #f1 #l
-<tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
->tr_compose_nap >tr_compose_push_bi //
-qed.
-
-lemma tr_uni_xap_succ (n) (m):
- ↑m + n = 𝐮❨n❩＠❨↑m❩.
-#n #m
-<tr_xap_unfold
-<tr_nap_push <tr_uni_nap //
-qed.
-
-lemma tr_uni_xap (n) (m):
- 𝐮❨n❩＠❨m❩ ≤ m+n.
-#n #m @(nat_ind_succ … m) -m //
-qed.
-
-lemma tr_xap_push (f) (l):
- ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
-#f #l
-<tr_xap_unfold <tr_xap_unfold
-<tr_nap_push //
-qed.
-
-lemma tr_xap_pushs_le (f) (n) (m):
- m ≤ n → m = (⫯*[n]f)＠❨m❩.
-#f #n #m #Hmn
-<tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
-/2 width=1 by nlt_succ_dx/
-qed-.
lemma nrplus_succ_shift (p) (n): ↑p + n = p + ↑n.
// qed.
-lemma nrplus_succ_sn (p) (n): ↑(p+n) = ↑p + n.
-// qed.
-
lemma nrplus_unit_sn (n): ↑n = 𝟏 + n.
#n @(nat_ind_succ … n) -n //
qed.
--- /dev/null
+include "ground/relocation/tr_uni_pap.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/notation/functions/applysucc_2.ma".
+include "ground/arith/nat_lt.ma".
+include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_pred_succ.ma".
+
+lemma nlt_npsucc_bi (n1) (n2):
+ n1 < n2 → npsucc n1 < npsucc n2.
+#n1 #n2 #Hn elim Hn -n2 //
+#n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
+qed.
+
+definition tr_nap (f) (l:nat): nat ≝
+ ↓(f＠⧣❨↑l❩).
+
+interpretation
+ "functional non-negative application (total relocation maps)"
+ 'ApplySucc f l = (tr_nap f l).
+
+lemma tr_nap_unfold (f) (l):
+ ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
+// qed.
+
+lemma tr_compose_nap (f2) (f1) (l):
+ f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
+#f2 #f1 #l
+<tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+<tr_compose_pap <npsucc_pred //
+qed.
+
+lemma tr_uni_nap (n) (m):
+ m + n = 𝐮❨n❩@↑❨m❩.
+#n #m
+<tr_nap_unfold
+<tr_uni_pap <nrplus_npsucc_sn //
+qed.
+
+lemma tr_nap_push (f):
+ ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
+#f #l
+<tr_nap_unfold <tr_nap_unfold
+<tr_pap_push <pnpred_psucc //
+qed.
+
+lemma tr_nap_pushs_lt (f) (n) (m):
+ m < n → m = (⫯*[n]f)@↑❨m❩.
+#f #n #m #Hmn
+<tr_nap_unfold <tr_pap_pushs_le
+/2 width=1 by nlt_npsucc_bi/
+qed-.
--- /dev/null
+include "ground/relocation/nap.ma".
+include "ground/notation/functions/apply_2.ma".
+include "ground/relocation/tr_compose_pn.ma".
+
+definition tr_xap (f) (l:nat): nat ≝
+ (⫯f)@↑❨l❩.
+
+interpretation
+ "functional extended application (total relocation maps)"
+ 'Apply f l = (tr_xap f l).
+
+lemma tr_xap_unfold (f) (l):
+ (⫯f)@↑❨l❩ = f＠❨l❩.
+// qed.
+
+lemma tr_xap_zero (f):
+ (𝟎) = f＠❨𝟎❩.
+// qed.
+
+lemma tr_xap_ninj (f) (p):
+ ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
+// qed.
+
+lemma tr_compose_xap (f2) (f1) (l):
+ f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
+#f2 #f1 #l
+<tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
+>tr_compose_nap >tr_compose_push_bi //
+qed.
+
+lemma tr_uni_xap_succ (n) (m):
+ ↑m + n = 𝐮❨n❩＠❨↑m❩.
+#n #m
+<tr_xap_unfold
+<tr_nap_push <tr_uni_nap //
+qed.
+
+lemma tr_uni_xap (n) (m):
+ 𝐮❨n❩＠❨m❩ ≤ m+n.
+#n #m @(nat_ind_succ … m) -m //
+qed.
+
+lemma tr_xap_push (f) (l):
+ ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
+#f #l
+<tr_xap_unfold <tr_xap_unfold
+<tr_nap_push //
+qed.
+
+lemma tr_xap_pushs_le (f) (n) (m):
+ m ≤ n → m = (⫯*[n]f)＠❨m❩.
+#f #n #m #Hmn
+<tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
+/2 width=1 by nlt_succ_dx/
+qed-.
projects / helm.git / commitdiff