--- /dev/null
+(* COMMENT
+lemma prototerm_in_root_inv_lcons_oref:
+ ∀p,l,n. l◗p ϵ ▵#n →
+ ∧∧ 𝗱n = l & 𝐞 = p.
+#p #l #n * #q
+<list_append_lcons_sn #H0 destruct -H0
+elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
+/2 width=1 by conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_iref:
+ ∀t,p,l,n. l◗p ϵ ▵𝛕n.t →
+ ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
+#t #p #l #n * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct -H0
+/4 width=4 by ex2_intro, ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_mark:
+ ∀t,p,l. l◗p ϵ ▵ɱ.t →
+ ∧∧ 𝗺 = l & p ϵ ▵t.
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
+/3 width=2 by ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_abst:
+ ∀t,p,l. l◗p ϵ ▵𝛌.t →
+ ∧∧ 𝗟 = l & p ϵ ▵t.
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
+/3 width=2 by ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_appl:
+ ∀u,t,p,l. l◗p ϵ ▵@u.t →
+ ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
+ | ∧∧ 𝗔 = l & p ϵ ▵t.
+#u #t #p #l * #q * * #r #Hr
+<list_append_lcons_sn #H0 destruct
+/4 width=2 by ex_intro, or_introl, or_intror, conj/
+qed-.
+*)
include "delayed_updating/reduction/dbfr.ma".
include "delayed_updating/reduction/ibfr.ma".
-include "delayed_updating/unwind/unwind2_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_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/substitution/fsubst_lift.ma".
include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
include "delayed_updating/substitution/lift_path_structure.ma".
include "delayed_updating/substitution/lift_path_closed.ma".
include "delayed_updating/substitution/lift_rmap_closed.ma".
--- /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/reduction/ibfr_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
+include "ground/arith/pnat_two.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Example of unprotected balanced β-reduction ******************************)
+
+definition l3_t0: prototerm ≝
+ (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.⧣𝟏).
+
+definition l3_t1: prototerm ≝
+ (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣𝟏)).
+
+lemma l3_t01:
+ l3_t0 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝐞] l3_t1.
+@ibfr_abst_hd
+@ibfr_appl_hd
+@ibfr_eq_trans [| @ibfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_abst …))
+@abst_eq_repl
+@(subset_eq_canc_sn … (lift_term_appl … ))
+@appl_eq_repl
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.
interpretation
"balanced focused reduction with immediate updating (prototerm)"
'BlackRightArrowIBF t1 r t2 = (ibfr r t1 t2).
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma ibfr_eq_trans (t) (t1) (t2) (r):
+ t1 ➡𝐢𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐢𝐛𝐟[r] t2.
+#t #t1 #t2 #r
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_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/reduction/ibfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma ibfr_abst_hd (t1) (t2) (r):
+ t1 ➡𝐢𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐢𝐛𝐟[𝗟◗r] 𝛌.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
+ @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+ @fsubst_eq_repl // @lift_term_eq_repl_dx
+ >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
+]
+qed.
+
+lemma ibfr_appl_hd (v) (t1) (t2) (r):
+ t1 ➡𝐢𝐛𝐟[r] t2 → ＠v.t1 ➡𝐢𝐛𝐟[𝗔◗r] ＠v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
+ @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+ @fsubst_eq_repl // @lift_term_eq_repl_dx
+ >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
+]
+qed.
+
+lemma ibfr_appl_sd (v1) (v2) (t) (r):
+ v1 ➡𝐢𝐛𝐟[r] v2 → ＠v1.t ➡𝐢𝐛𝐟[𝗦◗r] ＠v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
+ @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
+ @fsubst_eq_repl // @lift_term_eq_repl_dx
+ >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
+]
+qed.
+
+lemma ibfr_beta_0 (v) (t) (q) (n):
+ q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+ ＠v.𝛌.t ➡𝐢𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←🠡[𝐮❨↑n❩]v]).
+#v #t #q #n #Hn #Ht
+@(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn //
+[ /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+ @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+ @fsubst_eq_repl // <nplus_zero_sn @lift_term_eq_repl_dx
+ >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+ @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+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/fsubst.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+include "ground/lib/subset_equivalence.ma".
+
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma fsubst_abst_hd (t) (u) (p):
+ 𝛌.(t[⋔p←u]) ⇔ (𝛌.t)[⋔𝗟◗p←u].
+#t #u #p @conj #r
+[ #Hr
+ elim (in_comp_inv_abst … Hr) -Hr #s #H0 * *
+ [ #q #Hq #H1 destruct
+ /3 width=3 by ex2_intro, or_introl/
+ | #H1s #H2s destruct
+ @or_intror @conj
+ [ /2 width=1 by in_comp_abst_hd/ ]
+ #s0 <list_append_rcons_dx #Hs0
+ elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
+ /2 width=2 by/
+ ]
+| * *
+ [ #q #Hq #H0 destruct
+ /4 width=3 by in_comp_abst_hd, ex2_intro, or_introl/
+ | #H1r #H2r
+ elim (in_comp_inv_abst … H1r) -H1r #s #H0 #Hs destruct
+ /5 width=2 by in_comp_abst_hd, conj, or_intror/
+ ]
+]
+qed.
+
+lemma fsubst_appl_sd (v) (t) (u) (p):
+ ＠v[⋔p←u].t ⇔ (＠v.t)[⋔𝗦◗p←u].
+#v #t #u #p @conj #r
+[ #Hr
+ elim (in_comp_inv_appl … Hr) -Hr * #s #H0
+ [ * *
+ [ #q #Hq #H1 destruct
+ /3 width=3 by ex2_intro, or_introl/
+ | #H1s #H2s destruct
+ @or_intror @conj
+ [ /2 width=1 by in_comp_appl_sd/ ]
+ #s0 <list_append_rcons_dx #Hs0
+ elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
+ /2 width=2 by/
+ ]
+ | #Hs destruct
+ @or_intror @conj [ /2 width=1 by in_comp_appl_hd/ ]
+ #r <list_append_rcons_dx #H0
+ elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct
+ ]
+| * *
+ [ #q #Hq #H0 destruct
+ /4 width=3 by in_comp_appl_sd, ex2_intro, or_introl/
+ | #H1r #H2r
+ elim (in_comp_inv_appl … H1r) -H1r * #s #H0 #Hs destruct
+ /5 width=2 by in_comp_appl_hd, in_comp_appl_sd, or_intror, conj/
+ ]
+]
+qed.
+
+lemma fsubst_appl_hd (v) (t) (u) (p):
+ ＠v.(t[⋔p←u]) ⇔ (＠v.t)[⋔𝗔◗p←u].
+#v #t #u #p @conj #r
+[ #Hr
+ elim (in_comp_inv_appl … Hr) -Hr * #s #H0
+ [ #Hs destruct
+ @or_intror @conj [ /2 width=1 by in_comp_appl_sd/ ]
+ #r <list_append_rcons_dx #H0
+ elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct
+ | * *
+ [ #q #Hq #H1 destruct
+ /3 width=3 by ex2_intro, or_introl/
+ | #H1s #H2s destruct
+ @or_intror @conj
+ [ /2 width=1 by in_comp_appl_hd/ ]
+ #s0 <list_append_rcons_dx #Hs0
+ elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
+ /2 width=2 by/
+ ]
+ ]
+| * *
+ [ #q #Hq #H0 destruct
+ /4 width=3 by in_comp_appl_hd, ex2_intro, or_introl/
+ | #H1r #H2r
+ elim (in_comp_inv_appl … H1r) -H1r * #s #H0 #Hs destruct
+ /5 width=2 by in_comp_appl_hd, in_comp_appl_sd, or_intror, conj/
+ ]
+]
+qed.
(* Constructions with subset_equivalence ************************************)
+lemma fsubst_empty_rc (t) (u):
+ u ⇔ t[⋔𝐞←u].
+#t #u @conj #p
+[ #Hp /3 width=3 by or_introl, ex2_intro/ ]
+* *
+[ #r #Hr #H0 destruct // ]
+#H1p #H2p elim H2p -H2p //
+qed.
+
lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):
t1 ⊆ t2 → u1 ⊆ u2 → t1[⋔p←u1] ⊆ t2[⋔p←u2].
#t1 #t2 #u1 #u2 #p #Ht #Hu #q * *
+++ /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_prototerm_id.ma".
-include "delayed_updating/substitution/lift_path_uni.ma".
-include "delayed_updating/syntax/prototerm_constructors_eq.ma".
-include "ground/relocation/nap.ma".
-
-(* LIFT FOR PROTOTERM *******************************************************)
-
-lemma lift_term_iref_pap_sn (f) (t:prototerm) (k:pnat):
- (𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t) ⊆ 🠡[f](𝛕k.t).
-#f #t #k #p * #q * #r #Hr #H1 #H2 destruct
-@(ex2_intro … (𝗱k◗𝗺◗r))
-/2 width=1 by in_comp_iref/
-qed-.
-
-lemma lift_term_iref_pap_dx (f) (t) (k:pnat):
- 🠡[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t.
-#f #t #k #p * #q #Hq #H0 destruct
-elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
-<lift_path_d_sn <lift_path_m_sn
-/3 width=1 by in_comp_iref, in_comp_lift_path_term/
-qed-.
-
-lemma lift_term_iref_pap (f) (t) (k:pnat):
- (𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t) ⇔ 🠡[f](𝛕k.t).
-/3 width=1 by conj, lift_term_iref_pap_sn, lift_term_iref_pap_dx/
-qed.
-
-lemma lift_term_iref_nap (f) (t) (n):
- (𝛕↑(f＠§❨n❩).🠡[⇂*[↑n]f]t) ⇔ 🠡[f](𝛕↑n.t).
-#f #t #n
->tr_pap_succ_nap //
-qed.
-
-lemma lift_term_iref_uni (t) (n) (k):
- (𝛕(k+n).t) ⇔ 🠡[𝐮❨n❩](𝛕k.t).
-#t #n #k
-@(subset_eq_trans … (lift_term_iref_pap …))
-<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
-/3 width=1 by iref_eq_repl, lift_term_id/
-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_prototerm_id.ma".
+include "delayed_updating/substitution/lift_path_uni.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+include "ground/relocation/nap.ma".
+
+(* LIFT FOR PROTOTERM *******************************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma lift_term_oref_pap (f) (k):
+ (⧣(f＠⧣❨k❩)) ⇔ 🠡[f]⧣k.
+#f #k @conj #p *
+[ /2 width=1 by in_comp_lift_path_term/
+| #q * #H0 destruct //
+]
+qed.
+
+lemma lift_term_iref_pap_sn (f) (t:prototerm) (k:pnat):
+ (𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t) ⊆ 🠡[f](𝛕k.t).
+#f #t #k #p * #q * #r #Hr #H1 #H2 destruct
+@(ex2_intro … (𝗱k◗𝗺◗r))
+/2 width=1 by in_comp_iref_hd/
+qed-.
+
+lemma lift_term_iref_pap_dx (f) (t) (k:pnat):
+ 🠡[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t.
+#f #t #k #p * #q #Hq #H0 destruct
+elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
+<lift_path_d_sn <lift_path_m_sn
+/3 width=1 by in_comp_iref_hd, in_comp_lift_path_term/
+qed-.
+
+lemma lift_term_iref_pap (f) (t) (k:pnat):
+ (𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t) ⇔ 🠡[f](𝛕k.t).
+/3 width=1 by conj, lift_term_iref_pap_sn, lift_term_iref_pap_dx/
+qed.
+
+lemma lift_term_iref_nap (f) (t) (n):
+ (𝛕↑(f＠§❨n❩).🠡[⇂*[↑n]f]t) ⇔ 🠡[f](𝛕↑n.t).
+#f #t #n
+>tr_pap_succ_nap //
+qed.
+
+lemma lift_term_iref_uni (t) (n) (k):
+ (𝛕(k+n).t) ⇔ 🠡[𝐮❨n❩](𝛕k.t).
+#t #n #k
+@(subset_eq_trans … (lift_term_iref_pap …))
+<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
+/3 width=1 by iref_eq_repl, lift_term_id/
+qed.
+
+lemma lift_term_abst (f) (t):
+ (𝛌.🠡[⫯f]t) ⇔ 🠡[f]𝛌.t.
+#f #t @conj #p #Hp
+[ elim (in_comp_inv_abst … Hp) -Hp #q #H1 * #r #Hr #H2 destruct
+ /3 width=1 by in_comp_lift_path_term, in_comp_abst_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+ elim (in_comp_inv_abst … Hq) -Hq #r #H0 #Hr destruct
+ /3 width=1 by in_comp_lift_path_term, in_comp_abst_hd/
+]
+qed.
+
+lemma lift_term_appl (f) (v) (t):
+ ＠🠡[f]v.🠡[f]t ⇔ 🠡[f]＠v.t.
+#f #v #t @conj #p #Hp
+[ elim (in_comp_inv_appl … Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
+ /3 width=1 by in_comp_lift_path_term, in_comp_appl_sd, in_comp_appl_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+ elim (in_comp_inv_appl … Hq) -Hq * #r #H0 #Hr destruct
+ /3 width=1 by in_comp_lift_path_term, in_comp_appl_sd, in_comp_appl_hd/
+]
+qed.
'Pitchfork t p = (prototerm_grafted p t).
definition prototerm_root: prototerm → prototerm ≝
- λt,q. ∃r. q●r ϵ t.
+ λt,q. ∃r. r ϵ t⋔q.
interpretation
"root (prototerm)"
'UpTriangle t = (prototerm_root t).
+(* Basic inversions *********************************************************)
+
+lemma prototerm_grafted_inv_gen (t) (p) (q):
+ q ϵ t⋔p → p●q ϵ t.
+// qed-.
+
(* Basic constructions ******************************************************)
lemma prototerm_in_comp_root (p) (t):
(* Basic constructions *******************************************************)
-lemma in_comp_iref (t) (q) (k):
+lemma in_comp_oref_hd (k):
+ (𝗱k◗𝐞) ϵ ⧣k.
+// qed.
+
+lemma in_comp_iref_hd (t) (q) (k):
q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
/2 width=3 by ex2_intro/ qed.
+lemma in_comp_abst_hd (t) (q):
+ q ϵ t → 𝗟◗q ϵ 𝛌.t.
+/2 width=3 by ex2_intro/ qed.
+
+lemma in_comp_appl_sd (u) (t) (q):
+ q ϵ u → 𝗦◗q ϵ ＠u.t.
+/3 width=3 by ex2_intro, or_introl/ qed.
+
+lemma in_comp_appl_hd (u) (t) (q):
+ q ϵ t → 𝗔◗q ϵ ＠u.t.
+/3 width=3 by ex2_intro, or_intror/ qed.
+
(* Basic inversions *********************************************************)
lemma in_comp_inv_iref (t) (p) (k):
/2 width=3 by ex2_intro/
qed-.
-(* COMMENT
-lemma prototerm_in_root_inv_lcons_oref:
- ∀p,l,n. l◗p ϵ ▵#n →
- ∧∧ 𝗱n = l & 𝐞 = p.
-#p #l #n * #q
-<list_append_lcons_sn #H0 destruct -H0
-elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
-/2 width=1 by conj/
-qed-.
-
-lemma prototerm_in_root_inv_lcons_iref:
- ∀t,p,l,n. l◗p ϵ ▵𝛕n.t →
- ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
-#t #p #l #n * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct -H0
-/4 width=4 by ex2_intro, ex_intro, conj/
-qed-.
-
-lemma prototerm_in_root_inv_lcons_mark:
- ∀t,p,l. l◗p ϵ ▵ɱ.t →
- ∧∧ 𝗺 = l & p ϵ ▵t.
-#t #p #l * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/3 width=2 by ex_intro, conj/
+lemma in_comp_inv_abst (t) (p):
+ p ϵ 𝛌.t →
+ ∃∃q. 𝗟◗q = p & q ϵ t.
+#t #p * #q #Hq #Hp
+/2 width=3 by ex2_intro/
qed-.
-lemma prototerm_in_root_inv_lcons_abst:
- ∀t,p,l. l◗p ϵ ▵𝛌.t →
- â\88§â\88§ ð\9d\97\9f = l & p ϵ â\96µt.
-#t #p #l * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/3 width=2 by ex_intro, conj/
+lemma in_comp_inv_appl (u) (t) (p):
+ p ϵ ＠u.t →
+ â\88¨â\88¨ â\88\83â\88\83q. ð\9d\97¦â\97\97q = p & q ϵ u
+ | ∃∃q. 𝗔◗q = p & q ϵ t.
+#u #t #p * * #q #Hq #Hp
+/3 width=3 by ex2_intro, or_introl, or_intror/
qed-.
-lemma prototerm_in_root_inv_lcons_appl:
- ∀u,t,p,l. l◗p ϵ ▵@u.t →
- ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
- | ∧∧ 𝗔 = l & p ϵ ▵t.
-#u #t #p #l * #q * * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/4 width=2 by ex_intro, or_introl, or_intror, conj/
-qed-.
-*)
+(* Advanced inversions ******************************************************)
+
+lemma in_comp_inv_abst_hd (t) (p):
+ (𝗟◗p) ϵ 𝛌.t → p ϵ t.
+#t #p #H0
+elim (in_comp_inv_abst … H0) -H0 #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
+
+lemma in_comp_inv_appl_sd (u) (t) (p):
+ (𝗦◗p) ϵ ＠u.t → p ϵ u.
+#u #t #p #H0
+elim (in_comp_inv_appl … H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
+
+lemma in_comp_inv_appl_hd (u) (t) (p):
+ (𝗔◗p) ϵ ＠u.t → p ϵ t.
+#u #t #p #H0
+elim (in_comp_inv_appl … H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-.
t1 ⇔ t2 → 𝛕k.t1 ⇔ 𝛕k.t2.
/2 width=1 by subset_equivalence_ext_f1_bi/
qed.
+
+lemma abst_eq_repl (t1) (t2):
+ t1 ⇔ t2 → 𝛌.t1 ⇔ 𝛌.t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
+
+lemma appl_eq_repl (u1) (u2) (t1) (t2):
+ u1 ⇔ u2 → t1 ⇔ t2 → ＠u1.t1 ⇔ ＠u2.t2.
+/2 width=1 by subset_equivalence_ext_f1_1_bi/
+qed.
+
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_abst_hd (t) (p):
+ t⋔p ⇔ (𝛌.t)⋔(𝗟◗p).
+#t #p @conj #r #Hr
+[ /2 width=3 by ex2_intro/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+ /2 width=1 by in_comp_inv_abst_hd/
+]
+qed.
+
+lemma grafted_appl_sd (v) (t) (p):
+ v⋔p ⇔ (＠v.t)⋔(𝗦◗p).
+#v #t #p @conj #r #Hr
+[ /3 width=3 by ex2_intro, or_introl/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+ /2 width=2 by in_comp_inv_appl_sd/
+]
+qed.
+
+lemma grafted_appl_hd (v) (t) (p):
+ t⋔p ⇔ (＠v.t)⋔(𝗔◗p).
+#v #t #p @conj #r #Hr
+[ /3 width=3 by ex2_intro, or_intror/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+ /2 width=2 by in_comp_inv_appl_hd/
+]
+qed.
(* EQUIVALENCE FOR PROTOTERM ************************************************)
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_empty_dx (t):
+ t ⇔ t⋔𝐞.
+/2 width=1 by conj/
+qed.
+
(* Constructions with prototerm_root ****************************************)
lemma prototerm_root_incl_repl:
+++ /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/unwind/unwind2_prototerm_eq.ma".
-include "delayed_updating/unwind/unwind2_path_append.ma".
-include "delayed_updating/syntax/prototerm_constructors.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-(* Constructions with constructors ******************************************)
-
-lemma unwind2_term_iref_sn (f) (t) (k:pnat):
- ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
-#f #t #k #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱k◗𝗺◗q))
-/2 width=1 by in_comp_iref/
-qed-.
-
-lemma unwind2_term_iref_dx (f) (t) (k:pnat):
- ▼[f](𝛕k.t) ⊆ ▼[f∘𝐮❨k❩]t.
-#f #t #k #p * #q #Hq #H0 destruct
-elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
-/2 width=1 by in_comp_unwind2_path_term/
-qed-.
-
-lemma unwind2_term_iref (f) (t) (k:pnat):
- ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
-/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
-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/unwind/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_path_append.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma unwind2_term_iref_sn (f) (t) (k:pnat):
+ ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
+#f #t #k #p * #q #Hq #H0 destruct
+@(ex2_intro … (𝗱k◗𝗺◗q))
+/2 width=1 by in_comp_iref_hd/
+qed-.
+
+lemma unwind2_term_iref_dx (f) (t) (k:pnat):
+ ▼[f](𝛕k.t) ⊆ ▼[f∘𝐮❨k❩]t.
+#f #t #k #p * #q #Hq #H0 destruct
+elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
+/2 width=1 by in_comp_unwind2_path_term/
+qed-.
+
+lemma unwind2_term_iref (f) (t) (k:pnat):
+ ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
+/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
+qed.
(* Example of unprotected balanced path *************************************)
-definition b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
+definition l3_b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
-lemma b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = b.
+lemma l3_b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = l3_b.
// qed.
-lemma b_balanced: ⊗b ϵ 𝐁.
-<b_unfold <structure_d_dx
+lemma l3_b_balanced: ⊗l3_b ϵ 𝐁.
+<l3_b_unfold <structure_d_dx
/2 width=1 by pbc_empty, pbc_redex/
qed.
-lemma b_closed: b ϵ 𝐂❨Ⓕ,𝟎❩.
+lemma l3_b_closed: l3_b ϵ 𝐂❨Ⓕ,𝟎❩.
/4 width=1 by pcc_A_sn, pcc_empty, pcc_false_d_dx, pcc_L_dx/
qed.
-lemma b_unwind2_rmap_unfold (f):
- (⫯f)∘𝐮❨𝟏❩ = ▶[f]b.
+lemma l3_b_unwind2_rmap_unfold (f):
+ (⫯f)∘𝐮❨𝟏❩ = ▶[f]l3_b.
// qed.
-lemma b_unwind2_rmap_pap_unit (f):
- ↑(f＠⧣❨𝟏❩) = ▶[f]b＠⧣❨𝟏❩.
+lemma l3_b_unwind2_rmap_pap_unit (f):
+ ↑(f＠⧣❨𝟏❩) = ▶[f]l3_b＠⧣❨𝟏❩.
// qed.
projects / helm.git / commitdiff