--- /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 x )"
+ non associative with precedence 45
+ for @{ 'PredicateTHook $x }.
include "delayed_updating/syntax/path_depth.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
-inductive dfr (p) (q) (t): predicate preterm ≝
+inductive dfr (p) (q) (t): predicate prototerm ≝
| dfr_beta (b):
- let r ≝ p●𝗔◗b●𝗟◗q◖𝗱(↑❘q❘) in
- r ϵ t → ⊓(⊗b) → dfr p q t (t[⋔r←t⋔(p◖𝗦)])
+ let r ≝ p●𝗔◗b●𝗟◗q in
+ r◖𝗱(↑❘q❘) ϵ t → ⊓(⊗b) → dfr p q t (t[⋔r←𝛗(↑❘q❘).t⋔(p◖𝗦)])
.
interpretation
- "focused balanced reduction with delayed updating (preterm)"
+ "focused balanced reduction with delayed updating (prototerm)"
'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).
(* *)
(**************************************************************************)
-include "delayed_updating/reduction/ifr.ma".
include "delayed_updating/reduction/dfr.ma".
+include "delayed_updating/reduction/ifr.ma".
+include "delayed_updating/substitution/fsubst_lift.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
-lemma dfr_lift_bi (f) (p) (q) (t1) (t2):
+lemma dfr_lift_bi (f) (p) (q) (t1) (t2): Ƭt1 →
t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
-#f #p #q #t1 #t2
-* #b #Hr #Hb
+#f #p #q #t1 #t2 #Ht1
+* -t2 #b #Hr #Hb
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/substitution/lift_preterm.ma".
+include "delayed_updating/substitution/lift_prototerm.ma".
include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
(* IMMEDIATE FOCUSED REDUCTION ************************************************)
-inductive ifr (p) (q) (t): predicate preterm ≝
+inductive ifr (p) (q) (t): predicate prototerm ≝
| ifr_beta (b):
let r ≝ p●𝗔◗b●𝗟◗q in
r◖𝗱(↑❘q❘) ϵ t → ⊓(⊗b) → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)])
.
interpretation
- "focused balanced reduction with immediate updating (preterm)"
+ "focused balanced reduction with immediate updating (prototerm)"
'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2).
(* *)
(**************************************************************************)
-include "ground/xoa/ex_3_1.ma".
-include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm.ma".
include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
(* FOCALIZED SUBSTITUTION ***************************************************)
-definition fsubst (p) (u): preterm → preterm ≝
+definition fsubst (p) (u): prototerm → prototerm ≝
λt,q.
- ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p●r = q
+ ∨∨ ∃∃r. r ϵ u & p●r = q
| ∧∧ q ϵ t & (∀r. p●r = q → ⊥)
.
interpretation
- "focalized substitution (preterm)"
+ "focalized substitution (prototerm)"
'PitchforkLeftArrow t p u = (fsubst p 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 *)
+(* *)
+(**************************************************************************)
+
+include "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/substitution/lift_prototerm.ma".
+include "delayed_updating/substitution/lift_structure.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm_proper.ma".
+
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+lemma lift_fsubst_sn (f) (t) (u) (p): Ꝕu → p ⧸ϵ t →
+ (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
+#f #t #u #p #Hu #Hp #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+ >lift_append_proper_dx
+ /4 width=1 by subset_in_ext_f1_dx, or_introl/
+| * #q #Hq #H1 #H0
+ @(ex2_intro … H1) @or_intror @conj //
+ #r #H2 destruct
+ @H0 -H0 [| <lift_append_proper_dx /2 width=1 by/ ]
+]
+qed-.
+
+lemma lift_fsubst_dx (f) (t) (u) (p): Ꝕu → p ϵ ▵t → structure_injective t →
+ ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u].
+#f #t #u #p #Hu #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+ @or_introl @ex2_intro
+ [|| <lift_append_proper_dx /2 width=1 by/ ]
+ /2 width=3 by ex2_intro/
+| #Hq #H0 #H1 destruct
+ @or_intror @conj [ /2 width=1 by subset_in_ext_f1_dx/ ] *
+ [ <list_append_empty_dx #Hr @(H0 … (𝐞)) -H0
+ <list_append_empty_dx @H2p -H2p /2 width=1 by prototerm_in_comp_root/
+ | #l #r #Hr
+ elim (lift_inv_append_proper_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+ lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
+ ]
+]
+qed-.
+
+lemma lift_fsubst (f) (t) (u) (p): Ꝕu → p ⧸ϵ t → p ϵ ▵t → structure_injective t →
+ (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]).
+/4 width=3 by lift_fsubst_sn, conj, lift_fsubst_dx/ qed.
(* LIFT FOR PATH ***********************************************************)
definition lift_continuation (A:Type[0]) ≝
- path → tr_map → A.
+ tr_map → path → A.
(* Note: inner numeric labels are not liftable, so they are removed *)
-rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ≝
+rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (f) (p) on p ≝
match p with
-[ list_empty ⇒ k (𝐞) f
+[ list_empty ⇒ k f (𝐞)
| list_lcons l q ⇒
match l with
[ label_node_d n ⇒
match q with
- [ list_empty ⇒ lift_gen (A) (λp. k (𝗱(f@❨n❩)◗p)) q (f∘𝐮❨n❩)
- | list_lcons _ _ ⇒ lift_gen (A) k q (f∘𝐮❨n❩)
+ [ list_empty ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (f∘𝐮❨n❩) q
+ | list_lcons _ _ ⇒ lift_gen (A) k (f∘𝐮❨n❩) q
]
- | label_edge_L ⇒ lift_gen (A) (λp. k (𝗟◗p)) q (⫯f)
- | label_edge_A ⇒ lift_gen (A) (λp. k (𝗔◗p)) q f
- | label_edge_S ⇒ lift_gen (A) (λp. k (𝗦◗p)) q f
+ | label_edge_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
+ | label_edge_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
+ | label_edge_S ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
]
].
interpretation
"lift (gneric)"
- 'UpArrow A k p f = (lift_gen A k p f).
+ 'UpArrow A k f p = (lift_gen A k f p).
-definition proj_path (p:path) (f:tr_map) ≝ p.
+definition proj_path: lift_continuation … ≝
+ λf,p.p.
-definition proj_rmap (p:path) (f:tr_map) ≝ f.
+definition proj_rmap: lift_continuation … ≝
+ λf,p.f.
interpretation
"lift (path)"
- 'UpArrow f p = (lift_gen ? proj_path p f).
+ 'UpArrow f p = (lift_gen ? proj_path f p).
interpretation
"lift (relocation map)"
- 'UpArrow p f = (lift_gen ? proj_rmap p f).
+ 'UpArrow p f = (lift_gen ? proj_rmap f p).
(* Basic constructions ******************************************************)
lemma lift_empty (A) (k) (f):
- k (𝐞) f = ↑{A}❨k, 𝐞, f❩.
+ k f (𝐞) = ↑{A}❨k, f, 𝐞❩.
// qed.
lemma lift_d_empty_sn (A) (k) (n) (f):
- ↑❨(λp. k (𝗱(f@❨n❩)◗p)), 𝐞, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱n◗𝐞, f❩.
+ ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), f∘𝐮❨ninj n❩, 𝐞❩ = ↑{A}❨k, f, 𝗱n◗𝐞❩.
// qed.
lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f):
- ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱n◗l◗p, f❩.
+ ↑❨k, f∘𝐮❨ninj n❩, l◗p❩ = ↑{A}❨k, f, 𝗱n◗l◗p❩.
// qed.
lemma lift_L_sn (A) (k) (p) (f):
- ↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩.
+ ↑❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ↑{A}❨k, f, 𝗟◗p❩.
// qed.
lemma lift_A_sn (A) (k) (p) (f):
- ↑❨(λp. k (𝗔◗p)), p, f❩ = ↑{A}❨k, 𝗔◗p, f❩.
+ ↑❨(λg,p. k g (𝗔◗p)), f, p❩ = ↑{A}❨k, f, 𝗔◗p❩.
// qed.
lemma lift_S_sn (A) (k) (p) (f):
- ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩.
+ ↑❨(λg,p. k g (𝗦◗p)), f, p❩ = ↑{A}❨k, f, 𝗦◗p❩.
// qed.
(* Basic constructions with proj_path ***************************************)
+lemma lift_path_empty (f):
+ (𝐞) = ↑[f]𝐞.
+// qed.
+
lemma lift_path_d_empty_sn (f) (n):
𝗱(f@❨n❩)◗𝐞 = ↑[f](𝗱n◗𝐞).
// qed.
(* LIFT FOR PATH ***********************************************************)
definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝
- λk1,k2. ∀p,f. k1 p f = k2 p f.
+ λk1,k2. ∀f,p. k1 f p = k2 f p.
interpretation
"extensional equivalence (lift continuation)"
(* Constructions with lift_exteq ********************************************)
lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
- k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩.
+ k1 ≗{A} k2 → ↑❨k1, f, p❩ = ↑❨k2, f, p❩.
#A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ]
[ #k1 #k2 #f #Hk <lift_empty <lift_empty //
|*: #IH #k1 #k2 #f #Hk /2 width=1 by/
(* Advanced constructions ***************************************************)
lemma lift_lcons_alt (A) (k) (f) (p) (l):
- ↑❨λp2.k(l◗p2),p,f❩ = ↑{A}❨λp2.k((l◗𝐞)●p2),p,f❩.
+ ↑❨λg,p2. k g (l◗p2), f, p❩ = ↑{A}❨λg,p2. k g ((l◗𝐞)●p2), f, p❩.
#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❩.
+ ↑❨λg,p2. k g (p1●l◗p2), f, p❩ = ↑{A}❨λg,p2. k g (p1◖l●p2), f, p❩.
#A #k #f #p1 #p #l
@lift_eq_repl_sn #p2 #g
<list_append_rcons_sn //
(* Advanced constructions with proj_path ************************************)
lemma lift_path_append_sn (p) (f) (q):
- q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
+ q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
#p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
| <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
qed.
lemma lift_path_lcons (f) (p) (l):
- l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
+ l◗↑[f]p = ↑❨(λg,p. proj_path g (l◗p)), f, p❩.
#f #p #l
>lift_lcons_alt <lift_path_append_sn //
qed.
lemma lift_path_L_sn (f) (p):
- 𝗟◗↑[⫯f]p = ↑[f](𝗟◗p).
+ (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
// qed.
lemma lift_path_A_sn (f) (p):
- 𝗔◗↑[f]p = ↑[f](𝗔◗p).
+ (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
// qed.
lemma lift_path_S_sn (f) (p):
- 𝗦◗↑[f]p = ↑[f](𝗦◗p).
+ (𝗦◗↑[f]p) = ↑[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/syntax/preterm.ma".
-include "delayed_updating/substitution/lift.ma".
-
-(* LIFT FOR PRETERM ***********************************************************)
-
-definition lift_preterm (f) (t): preterm ≝
- λp. ∃∃r. r ϵ t & p = ↑[f]r.
-
-interpretation
- "lift (preterm)"
- 'UpArrow f t = (lift_preterm f 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 *)
+(* *)
+(**************************************************************************)
+
+include "delayed_updating/substitution/lift.ma".
+include "delayed_updating/syntax/prototerm.ma".
+include "ground/lib/subset_ext_equivalence.ma".
+
+(* LIFT FOR PROTOTERM *******************************************************)
+
+interpretation
+ "lift (prototerm)"
+ 'UpArrow f t = (subset_ext_f1 ? ? (lift_gen ? proj_path f) t).
include "delayed_updating/substitution/lift_eq.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_proper.ma".
+include "ground/xoa/ex_4_2.ma".
+include "ground/xoa/ex_3_2.ma".
(* LIFT FOR PATH ***********************************************************)
#p @(path_ind_lift … p) -p //
qed.
-(* Properties with proper condition for path ********************************)
+(* Destructions with structure **********************************************)
+
+lemma lift_des_structure (q) (p) (f):
+ ⊗q = ↑[f]p → ⊗q = ⊗p.
+// qed-.
+
+(* Constructions with proper condition for path *****************************)
lemma lift_append_proper_dx (p2) (p1) (f): Ꝕp2 →
(⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
lemma lift_d_empty_dx (n) (p) (f):
(⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#n #p #f <lift_append_proper_dx //
qed.
lemma lift_L_dx (p) (f):
(⊗p)◖𝗟 = ↑[f](p◖𝗟).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p #f <lift_append_proper_dx //
qed.
lemma lift_A_dx (p) (f):
(⊗p)◖𝗔 = ↑[f](p◖𝗔).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p #f <lift_append_proper_dx //
qed.
lemma lift_S_dx (p) (f):
(⊗p)◖𝗦 = ↑[f](p◖𝗦).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p #f <lift_append_proper_dx //
qed.
+
+(* Advanced inversions with proj_path ***************************************)
+
+lemma lift_path_inv_d_sn (k) (q) (p) (f):
+ (𝗱k◗q) = ↑[f]p →
+ ∃∃r,h. 𝐞 = ⊗r & (↑[r]f)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+#k #q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct -IH
+ /2 width=5 by ex4_2_intro/
+| <lift_path_d_lcons_sn #H
+ elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+ /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_L_sn (q) (p) (f):
+ (𝗟◗q) = ↑[f]p →
+ ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[⫯↑[r1]f]r2 & r1●𝗟◗r2 = p.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H
+ elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
+| <lift_path_L_sn #H destruct -IH
+ /2 width=5 by ex3_2_intro/
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_A_sn (q) (p) (f):
+ (𝗔◗q) = ↑[f]p →
+ ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗔◗r2 = p.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H
+ elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct -IH
+ /2 width=5 by ex3_2_intro/
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_S_sn (q) (p) (f):
+ (𝗦◗q) = ↑[f]p →
+ ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗦◗r2 = p.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H
+ elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct -IH
+ /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Inversions with proper condition for path ********************************)
+
+lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): Ꝕq2 →
+ q1●q2 = ↑[f]p →
+ ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
+#q2 #q1 elim q1 -q1
+[ #p #f #Hq2 <list_append_empty_sn #H destruct
+ /2 width=5 by ex3_2_intro/
+| * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
+ [ elim (lift_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
+ elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
+ elim Hq2 -Hq2 //
+ | 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 //
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
+include "delayed_updating/syntax/prototerm_constructors.ma".
+include "delayed_updating/syntax/prototerm_equivalence.ma".
+include "delayed_updating/notation/functions/class_d_phi_0.ma".
include "ground/xoa/or_5.ma".
include "ground/xoa/ex_3_1.ma".
include "ground/xoa/ex_4_2.ma".
include "ground/xoa/ex_4_3.ma".
include "ground/xoa/ex_5_3.ma".
-include "delayed_updating/syntax/preterm_equivalence.ma".
-include "delayed_updating/syntax/preterm_constructors.ma".
-include "delayed_updating/notation/functions/class_d_phi_0.ma".
(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
-inductive bdd: 𝒫❨preterm❩ ≝
+inductive bdd: 𝒫❨prototerm❩ ≝
| bdd_oref: ∀n. bdd (#n)
| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
| bdd_abst: ∀t. bdd t → bdd (𝛌.t)
.
interpretation
- "by-depth delayed (preterm)"
+ "by-depth delayed (prototerm)"
'ClassDPhi = (bdd).
(* Basic inversions *********************************************************)
[ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
[ #H0 #_
- lapply (preterm_root_eq_repl … H0) -H0 #H0
+ lapply (prototerm_root_eq_repl … H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_oref … Hl) -Hl //
+ elim (prototerm_in_root_inv_lcons_oref … Hl) -Hl //
| #u #_ #_ #H0
- lapply (preterm_root_eq_repl … H0) -H0 #H0
+ lapply (prototerm_root_eq_repl … H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_iref … Hl) -Hl //
+ elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl //
]
| * [ #m ] #p #IH #t #Ht
<list_cons_shift <list_cons_shift #Hn #Hl
[ #_ #H0
elim (eq_inv_list_empty_rcons ??? H0)
| #u #Hu #Hp #H0
- lapply (preterm_root_eq_repl … H0) -H0 #H0
+ lapply (prototerm_root_eq_repl … H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
+ elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
/2 width=4 by/
]
| elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
#u #Hu #Hp #H0
- lapply (preterm_root_eq_repl … H0) -H0 #H0
+ lapply (prototerm_root_eq_repl … H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
+ elim (prototerm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
/2 width=4 by/
| elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
#v #u #_ #Hu #Hp #H0
- lapply (preterm_root_eq_repl … H0) -H0 #H0
+ lapply (prototerm_root_eq_repl … H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
+ elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
/2 width=4 by/
| elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
#v #u #Hv #_ #Hp #H0
- lapply (preterm_root_eq_repl … H0) -H0 #H0
+ lapply (prototerm_root_eq_repl … H0) -H0 #H0
lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
- elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
+ elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
/2 width=4 by/
]
]
(* PATH *********************************************************************)
+(* Note: a path is a list of labels *)
definition path ≝ list label.
interpretation
(* *)
(**************************************************************************)
-include "ground/lib/subset.ma".
-include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/pitchfork_2.ma".
-include "delayed_updating/notation/functions/uptriangle_1.ma".
+include "delayed_updating/syntax/prototerm.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/notation/relations/predicate_t_hook_1.ma".
(* PRETERM ******************************************************************)
-(* Note: preterms are subsets of complete paths *)
-definition preterm: Type[0] ≝ 𝒫❨path❩.
+(* Note: different root paths have different structure *)
+definition structure_injective: predicate prototerm ≝
+ λt. ∀p1,p2. p1 ϵ ▵t → p2 ϵ ▵t → ⊗p1 = ⊗p2 → p1 = p2
+.
-definition preterm_grafted: path → preterm → preterm ≝
- λp,t,q. p●q ϵ t.
+(* Note: a preterm is a prototerm satislying the conditions above *)
+record is_preterm (t): Prop ≝
+{
+ is_pt_injective: structure_injective t
+}.
interpretation
- "grafted (preterm)"
- 'Pitchfork t p = (preterm_grafted p t).
-
-definition preterm_root: preterm → preterm ≝
- λt,q. ∃r. q●r ϵ t.
-
-interpretation
- "root (preterm)"
- 'UpTriangle t = (preterm_root t).
-
-(* Basic constructions ******************************************************)
-
-lemma preterm_in_comp_root (p) (t):
- p ϵ t → p ϵ ▵t.
-/2 width=2 by ex_intro/
-qed.
+ "preterm condition (prototerm)"
+ 'PredicateTHook t = (is_preterm 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 *)
-(* *)
-(**************************************************************************)
-
-include "delayed_updating/syntax/preterm.ma".
-include "delayed_updating/notation/functions/hash_1.ma".
-include "delayed_updating/notation/functions/phi_2.ma".
-include "delayed_updating/notation/functions/lamda_1.ma".
-include "delayed_updating/notation/functions/at_2.ma".
-
-(* CONSTRUCTORS FOR PRETERM *************************************************)
-
-definition preterm_node_0 (l): preterm ≝
- λp. l◗𝐞 = p.
-
-definition preterm_node_1 (l): preterm → preterm ≝
- λt,p. ∃∃q. q ϵ t & l◗q = p.
-
-definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
- λt1,t2,p.
- ∨∨ ∃∃q. q ϵ t1 & l1◗q = p
- | ∃∃q. q ϵ t2 & l2◗q = p.
-
-interpretation
- "outer variable reference by depth (preterm)"
- 'Hash n = (preterm_node_0 (label_node_d n)).
-
-interpretation
- "inner variable reference by depth (preterm)"
- 'Phi n t = (preterm_node_1 (label_node_d n) t).
-
-interpretation
- "name-free functional abstraction (preterm)"
- 'Lamda t = (preterm_node_1 label_edge_L t).
-
-interpretation
- "application (preterm)"
- 'At u t = (preterm_node_2 label_edge_S label_edge_A u t).
-
-(* Basic Inversions *********************************************************)
-
-lemma preterm_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 preterm_in_root_inv_lcons_iref:
- ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
- ∧∧ 𝗱n = l & p ϵ ▵t.
-#t #p #l #n * #q
-<list_append_lcons_sn * #r #Hr #H0 destruct
-/3 width=2 by ex_intro, conj/
-qed-.
-
-lemma preterm_in_root_inv_lcons_abst:
- ∀t,p,l. l◗p ϵ ▵𝛌.t →
- ∧∧ 𝗟 = l & p ϵ ▵t.
-#t #p #l * #q
-<list_append_lcons_sn * #r #Hr #H0 destruct
-/3 width=2 by ex_intro, conj/
-qed-.
-
-lemma preterm_in_root_inv_lcons_appl:
- ∀u,t,p,l. l◗p ϵ ▵@u.t →
- ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
- | ∧∧ 𝗔 = l & p ϵ ▵t.
-#u #t #p #l * #q
-<list_append_lcons_sn * * #r #Hr #H0 destruct
-/4 width=2 by ex_intro, or_introl, or_intror, 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 "ground/lib/subset_equivalence.ma".
-include "delayed_updating/syntax/preterm.ma".
-
-(* EQUIVALENCE FOR PRETERM **************************************************)
-
-(* Constructions with preterm_root ******************************************)
-
-lemma preterm_root_incl_repl:
- ∀t1,t2. t1 ⊆ t2 → ▵t1 ⊆ ▵t2.
-#t1 #t2 #Ht #p * #q #Hq
-/3 width=2 by ex_intro/
-qed.
-
-lemma preterm_root_eq_repl:
- ∀t1,t2. t1 ⇔ t2 → ▵t1 ⇔ ▵t2.
-#t1 #t2 * #H1 #H2
-/3 width=3 by conj, preterm_root_incl_repl/
-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 "ground/lib/subset.ma".
+include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/pitchfork_2.ma".
+include "delayed_updating/notation/functions/uptriangle_1.ma".
+
+(* PROTOTERM ****************************************************************)
+
+(* Note: a prototerm is a subset of complete paths *)
+definition prototerm: Type[0] ≝ 𝒫❨path❩.
+
+definition prototerm_grafted: path → prototerm → prototerm ≝
+ λp,t,q. p●q ϵ t.
+
+interpretation
+ "grafted (prototerm)"
+ 'Pitchfork t p = (prototerm_grafted p t).
+
+definition prototerm_root: prototerm → prototerm ≝
+ λt,q. ∃r. q●r ϵ t.
+
+interpretation
+ "root (prototerm)"
+ 'UpTriangle t = (prototerm_root t).
+
+(* Basic constructions ******************************************************)
+
+lemma prototerm_in_comp_root (p) (t):
+ p ϵ t → p ϵ ▵t.
+/2 width=2 by ex_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/syntax/prototerm.ma".
+include "delayed_updating/notation/functions/hash_1.ma".
+include "delayed_updating/notation/functions/phi_2.ma".
+include "delayed_updating/notation/functions/lamda_1.ma".
+include "delayed_updating/notation/functions/at_2.ma".
+
+(* CONSTRUCTORS FOR PROTOTERM ***********************************************)
+
+definition prototerm_node_0 (l): prototerm ≝
+ λp. l◗𝐞 = p.
+
+definition prototerm_node_1 (l): prototerm → prototerm ≝
+ λt,p. ∃∃q. q ϵ t & l◗q = p.
+
+definition prototerm_node_2 (l1) (l2): prototerm → prototerm → prototerm ≝
+ λt1,t2,p.
+ ∨∨ ∃∃q. q ϵ t1 & l1◗q = p
+ | ∃∃q. q ϵ t2 & l2◗q = p.
+
+interpretation
+ "outer variable reference by depth (prototerm)"
+ 'Hash n = (prototerm_node_0 (label_node_d n)).
+
+interpretation
+ "inner variable reference by depth (prototerm)"
+ 'Phi n t = (prototerm_node_1 (label_node_d n) t).
+
+interpretation
+ "name-free functional abstraction (prototerm)"
+ 'Lamda t = (prototerm_node_1 label_edge_L t).
+
+interpretation
+ "application (prototerm)"
+ 'At u t = (prototerm_node_2 label_edge_S label_edge_A u t).
+
+(* Basic Inversions *********************************************************)
+
+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
+<list_append_lcons_sn * #r #Hr #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
+<list_append_lcons_sn * #r #Hr #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
+<list_append_lcons_sn * * #r #Hr #H0 destruct
+/4 width=2 by ex_intro, or_introl, or_intror, 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 "ground/lib/subset_equivalence.ma".
+include "delayed_updating/syntax/prototerm.ma".
+
+(* EQUIVALENCE FOR PROTOTERM ************************************************)
+
+(* Constructions with prototerm_root ****************************************)
+
+lemma prototerm_root_incl_repl:
+ ∀t1,t2. t1 ⊆ t2 → ▵t1 ⊆ ▵t2.
+#t1 #t2 #Ht #p * #q #Hq
+/3 width=2 by ex_intro/
+qed.
+
+lemma prototerm_root_eq_repl:
+ ∀t1,t2. t1 ⇔ t2 → ▵t1 ⇔ ▵t2.
+#t1 #t2 * #H1 #H2
+/3 width=3 by conj, prototerm_root_incl_repl/
+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_proper.ma".
+include "ground/lib/subset_ext_equivalence.ma".
+
+(* PROPER CONDITION FOR PROTOTERM *******************************************)
+
+interpretation
+ "proper condition (prototerm)"
+ 'PredicatePTail t = (subset_ext_p1 path ppc t).
+
+(* Basic constructions ******************************************************)
+
+lemma tpc_i (t):
+ (𝐞 ⧸ϵ t) → Ꝕt.
+#t #Ht * //
+#H elim (Ht H)
+qed.
+
+(* Basic inversions *********************************************************)
+
+lemma tpc_e (t): Ꝕt → 𝐞 ϵ t → ⊥.
+/2 width=5 by subset_in_inv_ext_p1_dx/ qed-.
projects / helm.git / commitdiff