include "delayed_updating/reduction/dfr.ma".
include "delayed_updating/reduction/ifr.ma".
-(*
-include "delayed_updating/unwind/unwind2_constructors.ma".
-include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
-include "delayed_updating/unwind/unwind2_preterm_eq.ma".
-include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_head.ma".
-*)
+
+include "delayed_updating/substitution/fsubst_lift.ma".
include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_constructors.ma".
include "delayed_updating/substitution/lift_prototerm_eq.ma".
include "delayed_updating/substitution/lift_path_head.ma".
-
-include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-
+include "delayed_updating/substitution/lift_rmap_head.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
(* Constructions with lift **************************************************)
-(*
-lemma pippo (f) (r):
- ↑[↑[r]f](rᴿ) = (↑[f]r)ᴿ.
-#f #r @(list_ind_rcons … r) -r //
-#p * [ #n ] #IH
-[ <reverse_rcons <lift_path_d_sn <lift_rmap_d_dx
- <lift_path_d_dx <reverse_rcons
- <IH
-*)
-theorem dfr_lift_bi (f) (p) (q) (t1) (t2): (*t1 ϵ 𝐓 → *)
+theorem dfr_lift_bi (f) (p) (q) (t1) (t2):
t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]p,↑[↑[p◖𝗔◖𝗟]f]q] ↑[f]t2.
#f #p #q #t1 #t2
* #n * #H1n #Ht1 #Ht2
<(lift_path_head … H1n) -H1n //
| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1n
<lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
@(subset_eq_trans … Ht2) -t2
-(*
- @(subset_eq_trans … (unwind2_term_fsubst …))
- [ @fsubst_eq_repl [ // | // ]
- @(subset_eq_trans … (unwind2_term_iref …))
- @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
- [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
- @(subset_eq_trans … (unwind2_lift_term_after …))
- @unwind2_term_eq_repl_sn
+ @(subset_eq_trans … (lift_term_fsubst …))
+ @fsubst_eq_repl [ // | // ]
+ @(subset_eq_trans … (lift_term_iref …))
+ @iref_eq_repl
+ @(subset_eq_canc_sn … (lift_term_grafted_S …))
+ @lift_term_eq_repl_sn
(* Note: crux of the proof begins *)
- @nstream_eq_inv_ext #m
- <tr_compose_pap <tr_compose_pap
- <tr_uni_pap <tr_uni_pap <tr_pap_plus
- >list_append_rcons_sn in H1n; <reverse_append #H1n
- lapply (unwind2_rmap_append_pap_closed f … H1n) #H2n
- >nrplus_inj_dx in ⊢ (???%); <H2n -H2n
- lapply (tls_unwind2_rmap_append_closed f … H1n) #H2n
- <(tr_pap_eq_repl … H2n) -H2n -H1n //
+ >list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx
+ /2 width=1 by tls_lift_rmap_append_closed/
(* Note: crux of the proof ends *)
- | //
- | /2 width=2 by ex_intro/
- | //
- ]
]
qed.
-*)
\ No newline at end of file
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/syntax/prototerm_eq.ma".
include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/syntax/path_reverse.ma".
include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".
(* IMMEDIATE FOCUSED REDUCTION ************************************************)
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/substitution/lift_prototerm_eq.ma".
-(*
-include "delayed_updating/syntax/preterm.ma".
-include "delayed_updating/syntax/prototerm_proper.ma".
-*)
+
(* FOCALIZED SUBSTITUTION ***************************************************)
(* Constructions with lift for preterm **************************************)
/2 width=3 by ex2_intro/
| #Hq #H0 #H1 destruct
@or_intror @conj [ /2 width=1 by in_comp_lift_path_term/ ] -Hq #r #Hr
- elim (lift_path_inv_append_dx … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
+ elim (lift_path_inv_append_sn … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
lapply (lift_path_inj … Hs1) -Hs1 #H1 destruct
/2 width=2 by/
]
(* LIFT FOR PROTOTERM *******************************************************)
-lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
+lemma lift_term_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))
/2 width=1 by in_comp_iref/
qed-.
-lemma lift_iref_dx (f) (t) (n:pnat):
+lemma lift_term_iref_dx (f) (t) (n:pnat):
↑[f](𝛕n.t) ⊆ 𝛕f@⧣❨n❩.↑[⇂*[n]f]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_path_term/
qed-.
-lemma lift_iref (f) (t) (n:pnat):
+lemma lift_term_iref (f) (t) (n:pnat):
(𝛕f@⧣❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛕n.t).
-/3 width=1 by conj, lift_iref_sn, lift_iref_dx/
+/3 width=1 by conj, lift_term_iref_sn, lift_term_iref_dx/
qed.
-lemma lift_iref_uni (t) (m) (n):
+lemma lift_term_iref_uni (t) (m) (n):
(𝛕(n+m).t) ⇔ ↑[𝐮❨m❩](𝛕n.t).
#t #m #n
-@(subset_eq_trans … (lift_iref …))
+@(subset_eq_trans … (lift_term_iref …))
<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
/3 width=1 by iref_eq_repl, lift_term_id/
qed.
include "ground/relocation/tr_pap_pap.ma".
include "ground/relocation/tr_pap_eq.ma".
include "ground/relocation/tr_pn_eq.ma".
+include "ground/lib/stream_tls_plus.ma".
include "ground/lib/stream_tls_eq.ma".
+include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_rplus_pplus.ma".
(* LIFT FOR PATH ************************************************************)
#f #p <lift_path_append //
qed.
-(* Advanced inversions ******************************************************)
+(* Advanced constructions with proj_rmap ************************************)
+
+lemma lift_rmap_eq_repl (p):
+ stream_eq_repl … (λf1,f2. ↑[p]f1 ≗ ↑[p]f2).
+#p elim p -p //
+* [ #n ] #p #IH #f1 #f2 #Hf
+[ /3 width=1 by stream_tls_eq_repl/
+| /2 width=1 by/
+| /3 width=1 by tr_push_eq_repl/
+| /2 width=1 by/
+| /2 width=1 by/
+]
+qed.
+
+lemma tls_lift_rmap_d_dx (f) (p) (m) (n):
+ ⇂*[m+n]↑[p]f ≗ ⇂*[m]↑[p◖𝗱n]f.
+#f #p #m #n
+<lift_rmap_d_dx >nrplus_inj_dx >nrplus_inj_sn //
+qed.
+
+(* Advanced inversions with proj_path ***************************************)
lemma lift_path_inv_empty (f) (p):
(𝐞) = ↑[f]p → 𝐞 = p.
/2 width=3 by ex2_intro/
qed-.
-lemma lift_path_inv_append_dx (q2) (q1) (p) (f):
+lemma lift_path_inv_append_sn (q2) (q1) (p) (f):
q1●q2 = ↑[f]p →
∃∃p1,p2. q1 = ↑[f]p1 & q2 = ↑[↑[p1]f]p2 & p1●p2 = p.
#q2 #q1 elim q1 -q1
[ <list_append_empty_sn #H0 destruct
/2 width=5 by ex3_2_intro/
| <list_append_lcons_sn #H0
- elim (lift_path_inv_d_sn … H0) -H0 #r1 #m1 #_ #_ #H0 #_ -IH
- elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
- elim Hq2 -Hq2 //
- | elim (lift_path_inv_m_sn … H)
- | elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
- elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
- @(ex3_2_intro … (r1●𝗟◗p1)) //
- <structure_append <Hr1 -Hr1 //
- | elim (lift_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
- elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
- @(ex3_2_intro … (r1●𝗔◗p1)) //
- <structure_append <Hr1 -Hr1 //
- | elim (lift_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
- elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
- @(ex3_2_intro … (r1●𝗦◗p1)) //
- <structure_append <Hr1 -Hr1 //
- ]
+ elim (lift_path_inv_d_sn … H0) -H0 #r1 #m1 #H1 #H0 #H2 destruct
+ elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+ elim (lift_path_inv_m_sn … H0) -H0 #r1 #H0 #H1 destruct
+ elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+ elim (lift_path_inv_L_sn … H0) -H0 #r1 #H0 #H1 destruct
+ elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+ elim (lift_path_inv_A_sn … H0) -H0 #r1 #H0 #H1 destruct
+ elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+ elim (lift_path_inv_S_sn … H0) -H0 #r1 #H0 #H1 destruct
+ elim (IH … H0) -IH -H0 #p1 #p2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
]
qed-.
-(* Main inversions **********************************************************)
+(* Main inversions with proj_path *******************************************)
theorem lift_path_inj (q:path) (p) (f):
↑[f]q = ↑[f]p → q = p.
<(lift_path_inv_empty … H0) -H0 //
| <lift_path_d_sn #H0
elim (lift_path_inv_d_sn … H0) -H0 #r #h #H0
- <(tr_pap_inj ????? H0) -h [1,3: // ] #Hr #H0 destruct
+ >(tr_pap_inj ???? H0) -k [1,3: // ] #Hr #H0 destruct
| <lift_path_m_sn #H0
elim (lift_path_inv_m_sn … H0) -H0 #r #Hr #H0 destruct
| <lift_path_L_sn #H0
<(IH … Hr) -r -IH //
qed-.
-(* COMMENT
-
-(* Advanced constructions with proj_rmap and stream_tls *********************)
-
-lemma lift_rmap_tls_d_dx (f) (p) (m) (n):
- ⇂*[m+n]↑[p]f ≗ ⇂*[m]↑[p◖𝗱n]f.
-#f #p #m #n
-<lift_rmap_d_dx >nrplus_inj_dx
-/2 width=1 by tr_tls_compose_uni_dx/
-qed.
-
-*)
| @subset_equivalence_ext_f1_exteq /2 width=5/
]
qed.
+
+lemma lift_term_grafted_sn (f) (t) (p):
+ ↑[↑[p]f](t⋔p) ⊆ (↑[f]t)⋔(↑[f]p).
+#f #t #p #q * #r #Hr #H0 destruct
+@(ex2_intro … Hr) -Hr
+<lift_path_append_sn //
+qed-.
+
+lemma lift_term_grafted_dx (f) (t) (p):
+ (↑[f]t)⋔(↑[f]p) ⊆ ↑[↑[p]f](t⋔p).
+#f #t #p #q * #r #Hr #H0
+elim (lift_path_inv_append_sn … (sym_eq … H0)) -H0
+#p0 #q0 #Hp0 #Hq0 #H0 destruct
+lapply (lift_path_inj … Hp0) -Hp0 #Hp0 destruct
+/2 width=1 by in_comp_lift_path_term/
+qed-.
+
+lemma lift_term_grafted (f) (t) (p):
+ ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(↑[f]p).
+/3 width=1 by lift_term_grafted_sn, lift_term_grafted_dx, conj/ qed.
+
+lemma lift_term_grafted_S (f) (t) (p):
+ ↑[↑[p]f](t⋔(p◖𝗦)) ⇔ (↑[f]t)⋔((↑[f]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/substitution/lift_eq.ma".
+include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_reverse.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* LIFT MAP FOR PATH ********************************************************)
+
+(* Constructions with path_head *********************************************)
+
+lemma tls_plus_lift_rmap_reverse_closed (f) (q) (p) (n) (k):
+ q = (↳[n]q)●p →
+ ⇂*[k]↑[pᴿ]f ≗ ⇂*[n+k]↑[qᴿ]f.
+#f #q elim q -q
+[ #p #n #k #Hp
+ elim (eq_inv_list_empty_append … Hp) -Hp #Hn #H0 destruct
+ <path_head_empty in Hn; #Hn
+ <(eq_inv_empty_labels … Hn) -n //
+| #l #q #IH #p #n @(nat_ind_succ … n) -n //
+ #n #_ #k cases l [ #m ]
+ [ <path_head_d_sn <list_append_lcons_sn #Hp
+ elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp <nrplus_inj_sn
+ <reverse_lcons
+ @(stream_eq_trans … (tls_lift_rmap_d_dx …))
+ >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
+ >nsucc_unfold /2 width=1 by/
+ | <path_head_m_sn <list_append_lcons_sn #Hp
+ elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ <reverse_lcons <lift_rmap_m_dx /2 width=1 by/
+ | <path_head_L_sn <list_append_lcons_sn #Hp
+ elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ <reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
+ | <path_head_A_sn <list_append_lcons_sn #Hp
+ elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ <reverse_lcons <lift_rmap_A_dx /2 width=2 by/
+ | <path_head_S_sn <list_append_lcons_sn #Hp
+ elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ <reverse_lcons <lift_rmap_S_dx /2 width=2 by/
+ ]
+]
+qed-.
+
+lemma tls_lift_rmap_append_closed (f) (p) (q) (n):
+ qᴿ = ↳[n](p●q)ᴿ →
+ ↑[p]f ≗ ⇂*[n]↑[p●q]f.
+#f #p #q #n #H0
+>(reverse_reverse p) >(reverse_reverse q)
+/2 width=1 by tls_plus_lift_rmap_reverse_closed/
+qed.