--- /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 70 t )"
+ non associative with precedence 70
+ for @{ 'BlackDownTriangle $t }.
(* NOTATION FOR DELAYED UPDATING ********************************************)
-notation "hvbox( ▼[ term 46 t1 ] break term 70 t2 )"
+notation "hvbox( ▼[ term 46 t1 ] break term 70 t2 )"
non associative with precedence 70
for @{ 'BlackDownTriangle $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 70 t )"
+ non associative with precedence 70
+ for @{ 'BlackRightTriangle $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( ♭ term 70 p )"
+ non associative with precedence 70
+ for @{ 'Flat $p }.
. replace.sh . "/substitution/" "/unwind/"
. replace.sh . ↑ ▼
+
+266D;MUSIC FLAT SIGN;So;0;ON;;;;;N;FLAT;;;;
+266E;MUSIC NATURAL SIGN;So;0;ON;;;;;N;NATURAL;;;;
+266F;MUSIC SHARP SIGN;Sm;0;ON;;;;;N;SHARP;;;;
include "delayed_updating/notation/functions/uparrow_4.ma".
include "delayed_updating/notation/functions/uparrow_2.ma".
include "delayed_updating/syntax/path.ma".
-include "ground/relocation/tr_uni.ma".
-include "ground/relocation/tr_pap_tls.ma".
+include "ground/relocation/tr_id_pap.ma".
(* LIFT FOR PATH ***********************************************************)
[ list_empty ⇒ k f (𝐞)
| list_lcons l q ⇒
match l with
- [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q
+ [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐢) q
| label_m ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q
| label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
| label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
// qed.
lemma lift_d_sn (A) (k) (p) (n) (f):
- ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
+ ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
// qed.
lemma lift_m_sn (A) (k) (p) (f):
// qed.
lemma lift_rmap_d_sn (f) (p) (n):
- ↑[p](⇂*[ninj n]f) = ↑[𝗱n◗p]f.
+ ↑[p]𝐢 = ↑[𝗱n◗p]f.
// qed.
lemma lift_rmap_m_sn (f) (p):
lemma lift_rmap_append (p2) (p1) (f):
↑[p2]↑[p1]f = ↑[p1●p2]f.
#p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
-[ <lift_rmap_m_sn <lift_rmap_m_sn //
+[ <lift_rmap_d_sn <lift_rmap_d_sn //
+| <lift_rmap_m_sn <lift_rmap_m_sn //
| <lift_rmap_A_sn <lift_rmap_A_sn //
| <lift_rmap_S_sn <lift_rmap_S_sn //
]
(* Advanced constructions with proj_rmap and path_rcons *********************)
lemma lift_rmap_d_dx (f) (p) (n):
- ⇂*[ninj n](↑[p]f) = ↑[p◖𝗱n]f.
+ (𝐢) = ↑[p◖𝗱n]f.
// qed.
lemma lift_rmap_m_dx (f) (p):
// qed.
lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
- ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩+↑[p]f@❨n❩.
+ m = ↑[p◖𝗱n]f@❨m❩.
// qed.
include "delayed_updating/substitution/lift_eq.ma".
include "ground/relocation/tr_compose_pap.ma".
include "ground/relocation/tr_compose_pn.ma".
-include "ground/relocation/tr_compose_tls.ma".
(* LIFT FOR PATH ***********************************************************)
lemma lift_path_after (p) (f1) (f2):
↑[f2]↑[f1]p = ↑[f2∘f1]p.
-#p elim p -p [| * ] // [ #n ] #p #IH #f1 #f2
-[ <lift_path_d_sn <lift_path_d_sn <lift_path_d_sn //
-| <lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
- >tr_compose_push_bi //
-]
+#p elim p -p [| * ] // #p #IH #f1 #f2
+<lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
+>tr_compose_push_bi //
qed.
(* *)
(**************************************************************************)
-include "delayed_updating/substitution/lift_prototerm_id.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
include "delayed_updating/substitution/lift_uni.ma".
include "delayed_updating/syntax/prototerm_constructors.ma".
qed.
lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
- (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
-#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
-@(ex2_intro … (𝗱n◗𝗺◗r))
+ (𝛗f@❨n❩.t) ⊆ ↑[f](𝛗n.t).
+#f #t #n #p * #q #Hq #H0 destruct
+@(ex2_intro … (𝗱n◗𝗺◗q))
/2 width=1 by in_comp_iref/
qed-.
lemma lift_iref_dx (f) (t) (n:pnat):
- ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t.
+ ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.t.
#f #t #n #p * #q #Hq #H0 destruct
elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
-/3 width=1 by in_comp_iref, in_comp_lift_bi/
+/2 width=1 by in_comp_iref/
qed-.
lemma lift_iref (f) (t) (n:pnat):
- (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
+ (𝛗f@❨n❩.t) ⇔ ↑[f](𝛗n.t).
/3 width=1 by conj, lift_iref_sn, lift_iref_dx/
qed.
lemma lift_iref_uni (t) (m) (n):
(𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t).
-#t #m #n
-@(subset_eq_trans … (lift_iref …))
-<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
-/3 width=1 by lift_iref_bi, lift_term_id/
-qed.
+// qed.
(**************************************************************************)
include "delayed_updating/substitution/lift.ma".
-(*
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-*)
include "ground/relocation/tr_pap_eq.ma".
include "ground/relocation/tr_pn_eq.ma".
-include "ground/lib/stream_tls_eq.ma".
(* LIFT FOR PATH ***********************************************************)
#k1 #k2 #Hk #f1 #f2 #Hf
[ <lift_empty <lift_empty /2 width=1 by/
| <lift_d_sn <lift_d_sn <(tr_pap_eq_repl … Hf)
- /3 width=3 by stream_tls_eq_repl, compose_repl_fwd_sn/
+ /3 width=1 by stream_eq_refl/
| /3 width=1 by/
| /3 width=1 by tr_push_eq_repl/
| /3 width=1 by/
qed.
lemma lift_path_d_sn (f) (p) (n):
- (𝗱(f@❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
+ (𝗱(f@❨n❩)◗↑[𝐢]p) = ↑[f](𝗱n◗p).
// qed.
lemma lift_path_m_sn (f) (p):
lemma lift_path_S_sn (f) (p):
(𝗦◗↑[f]p) = ↑[f](𝗦◗p).
// qed.
+
+lemma lift_path_id (p):
+ p = ↑[𝐢]p.
+#p elim p -p //
+* [ #n ] #p #IH //
+[ <lift_path_d_sn //
+| <lift_path_L_sn //
+]
+qed.
+
+lemma lift_path_append (p2) (p1) (f):
+ (↑[f]p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
+#p2 #p1 elim p1 -p1 //
+* [ #n1 ] #p1 #IH #f
+[ <lift_path_d_sn <lift_path_d_sn <IH //
+| <lift_path_m_sn <lift_path_m_sn <IH //
+| <lift_path_L_sn <lift_path_L_sn <IH //
+| <lift_path_A_sn <lift_path_A_sn <IH //
+| <lift_path_S_sn <lift_path_S_sn <IH //
+]
+qed.
+
+lemma lift_path_d_dx (n) (p) (f):
+ (↑[f]p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
+#n #p #f <lift_path_append //
+qed.
+
+lemma lift_path_m_dx (p) (f):
+ (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_L_dx (p) (f):
+ (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_A_dx (p) (f):
+ (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_S_dx (p) (f):
+ (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
+#p #f <lift_path_append //
+qed.
+
(* COMMENT
(* Advanced constructions with proj_rmap and stream_tls *********************)
--- /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_eq.ma".
+include "ground/lib/list_length.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Constructions with list_length ******************************************)
+
+lemma lift_path_length (p) (f):
+ ❘p❘ = ❘↑[f]p❘.
+#p elim p -p // * [ #n ] #p #IH #f //
+[ <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+]
+>list_length_lcons >list_length_lcons //
+qed.
| @subset_equivalence_ext_f1_exteq /2 width=5/
]
qed.
+
+lemma lift_term_id_sn (t):
+ t ⊆ ↑[𝐢]t.
+#t #p #Hp
+>(lift_path_id p)
+/2 width=1 by in_comp_lift_bi/
+qed-.
+
+lemma lift_term_id_dx (t):
+ ↑[𝐢]t ⊆ t.
+#t #p * #q #Hq #H destruct //
+qed-.
+
+lemma lift_term_id (t):
+ t ⇔ ↑[𝐢]t.
+/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/
+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_eq.ma".
+include "delayed_updating/syntax/path_structure.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Constructions with structure ********************************************)
+
+lemma structure_lift (p) (f):
+ ⊗p = ⊗↑[f]p.
+#p elim p -p //
+* [ #n ] #p #IH #f //
+[ <lift_path_m_sn <structure_m_sn <structure_m_sn //
+| <lift_path_L_sn <structure_L_sn <structure_L_sn //
+]
+qed.
+
+lemma lift_structure (p) (f):
+ ⊗p = ↑[f]⊗p.
+#p elim p -p //
+* [ #n ] #p #IH #f //
+qed.
(* *)
(**************************************************************************)
-include "delayed_updating/substitution/lift_id.ma".
+include "delayed_updating/substitution/lift_eq.ma".
include "ground/relocation/tr_uni_pap.ma".
-include "ground/relocation/tr_uni_tls.ma".
(* LIFT FOR PATH ***********************************************************)
lemma lift_path_d_sn_uni (p) (m) (n):
(𝗱(n+m)◗p) = ↑[𝐮❨m❩](𝗱(n)◗p).
-#p #m #n
-<lift_path_d_sn <tr_uni_pap >nsucc_pnpred
-<tr_tls_succ_uni //
-qed.
+// qed.
projects / helm.git / commitdiff