--- /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( 𝐈 )"
+ non associative with precedence 70
+ for @{ 'ClassI }.
| #g <lift_rmap_structure <depth_structure
>tr_pushs_swap <tr_pap_pushs_le //
| lapply (in_comp_lift_bi f … Ht1) -Ht1 -H0t1 -Hb -Ht2
- <lift_d_empty_dx //
+ <lift_path_d_empty_dx //
| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (lift_fsubst …))
| * #q #Hq #H1 #H0
@(ex2_intro … H1) @or_intror @conj // *
[ <list_append_empty_dx #H2 destruct
- elim (lift_root f q) #r #_ #Hr /2 width=2 by/
+ elim (lift_path_root f q) #r #_ #Hr /2 width=2 by/
| #l #r #H2 destruct
@H0 -H0 [| <lift_append_proper_dx /2 width=3 by ppc_lcons/ ]
]
]
qed.
+(* Advanced constructions with proj_rmap and path_rcons *********************)
+
+lemma lift_rmap_m_dx (f) (p):
+ ↑[p]f = ↑[p◖𝗺]f.
+// qed.
+
+lemma lift_rmap_L_dx (f) (p):
+ (⫯↑[p]f) = ↑[p◖𝗟]f.
+// qed.
+
+lemma lift_rmap_A_dx (f) (p):
+ ↑[p]f = ↑[p◖𝗔]f.
+// qed.
+
+lemma lift_rmap_S_dx (f) (p):
+ ↑[p]f = ↑[p◖𝗦]f.
+// qed.
+
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate …):
include "delayed_updating/substitution/lift_structure.ma".
include "delayed_updating/substitution/lift_prototerm.ma".
+lemma pippo (p):
+ ⊗p ϵ 𝐈.
+#p @(list_ind_rcons … p) -p
+[ <structure_empty //
+| #p * [ #n ] #IH
+ [ <structure_d_dx //
+ | <structure_m_dx //
+ | <structure_L_dx //
+ | <structure_A_dx //
+ | <structure_S_dx //
+ ]
+]
+qed.
+
(* LIFT FOR PRETERM *********************************************************)
(* Constructions with subset_equivalence ************************************)
-lemma lift_grafted_S_sn (f) (t) (p):
- ↑[↑[p]f](t⋔(p◖𝗦)) ⊆ (↑[f]t)⋔((⊗p)◖𝗦).
-#f #t #p #q * #r #Hr #H0 destruct
+lemma lift_grafted_sn (f) (t) (p): p ϵ 𝐈 →
+ ↑[↑[p]f](t⋔p) ⊆ (↑[f]t)⋔(⊗p).
+#f #t #p #Hp #q * #r #Hr #H0 destruct
@(ex2_intro … Hr) -Hr
-<list_append_rcons_sn <list_append_rcons_sn
-<lift_append_proper_dx //
+<lift_append_inner_sn //
qed-.
-lemma lift_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
- (↑[f]t)⋔((⊗p)◖𝗦) ⊆ ↑[↑[p]f](t⋔(p◖𝗦)).
-#f #t #p #Hp #Ht #q * #r #Hr
-<list_append_rcons_sn #H0
-elim (lift_inv_append_proper_dx … (sym_eq … H0)) -H0 //
+lemma lift_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+ (↑[f]t)⋔(⊗p) ⊆ ↑[↑[p]f](t⋔p).
+#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
+elim (lift_inv_append_inner_sn … (sym_eq … H0)) -H0 //
#p0 #q0 #Hp0 #Hq0 #H0 destruct
<(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
-elim (lift_path_inv_S_sn … (sym_eq … Hq0)) -Hq0
-#r1 #r2 #Hr1 #Hr2 #H0 destruct
-lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
-[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
/2 width=1 by in_comp_lift_bi/
qed-.
-lemma lift_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
- ↑[↑[p]f](t⋔(p◖𝗦)) ⇔ (↑[f]t)⋔((⊗p)◖𝗦).
-/3 width=1 by lift_grafted_S_sn, conj, lift_grafted_S_dx/ qed.
+lemma lift_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+ ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(⊗p).
+/3 width=1 by lift_grafted_sn, conj, lift_grafted_dx/ qed.
+
+(*
+
+-lemma lift_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ ������ →
+- (↑[f]t)⋔((⊗p)◖������) ⊆ ↑[↑[p]f](t⋔(p◖������)).
+-#f #t #p #Hp #Ht #q * #r #Hr
+-<list_append_rcons_sn #H0
+-elim (lift_inv_append_proper_dx … (sym_eq … H0)) -H0 //
++lemma lift_grafted_dx (f) (t) (p): p ϵ ������ → p ϵ ▵t → t ϵ ������ →
++ (↑[f]t)⋔(⊗p) ⊆ ↑[↑[p]f](t⋔p).
++#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
++elim (lift_inv_append_inner_sn … (sym_eq … H0)) -H0 //
+ #p0 #q0 #Hp0 #Hq0 #H0 destruct
+ <(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+-elim (lift_path_inv_S_sn … (sym_eq … Hq0)) -Hq0
+-#r1 #r2 #Hr1 #Hr2 #H0 destruct
+-lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
+-[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
+ /2 width=1 by in_comp_lift_bi/
+ qed-.
+
+-lemma lift_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ ������ →
+- ↑[↑[p]f](t⋔(p◖������)) ⇔ (↑[f]t)⋔((⊗p)◖������).
+-/3 width=1 by lift_grafted_S_sn, conj, lift_grafted_S_dx/ qed.
++lemma lift_grafted (f) (t) (p): p ϵ ������ → p ϵ ▵t → t ϵ ������ →
++ ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(⊗p).
++/3 width=1 by lift_grafted_sn, conj, lift_grafted_dx/ qed.
+
+*)
include "delayed_updating/substitution/lift_eq.ma".
include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_inner.ma".
include "delayed_updating/syntax/path_proper.ma".
include "ground/xoa/ex_4_2.ma".
]
qed-.
-(* Advanced constructions with structure ************************************)
+(* Constructions with inner condition for path ******************************)
-lemma lift_d_empty_dx (n) (p) (f):
+lemma lift_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
+ (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
+#p1 @(list_ind_rcons … p1) -p1 // #p1 *
+[ #n ] #_ #p2 #f #Hp1
+[ elim (pic_inv_d_dx … Hp1)
+| <list_append_rcons_sn <lift_append_proper_dx //
+| <list_append_rcons_sn <lift_append_proper_dx //
+ <structure_L_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+ <structure_A_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+ <structure_S_dx <list_append_rcons_sn //
+]
+qed-.
+
+(* Advanced constructions with proj_path ************************************)
+
+lemma lift_path_d_empty_dx (n) (p) (f):
(⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
#n #p #f <lift_append_proper_dx //
qed.
-lemma lift_m_dx (p) (f):
+lemma lift_path_m_dx (p) (f):
⊗p = ↑[f](p◖𝗺).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_L_dx (p) (f):
+lemma lift_path_L_dx (p) (f):
(⊗p)◖𝗟 = ↑[f](p◖𝗟).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_A_dx (p) (f):
+lemma lift_path_A_dx (p) (f):
(⊗p)◖𝗔 = ↑[f](p◖𝗔).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_S_dx (p) (f):
+lemma lift_path_S_dx (p) (f):
(⊗p)◖𝗦 = ↑[f](p◖𝗦).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_root (f) (p):
+lemma lift_path_root (f) (p):
∃∃r. 𝐞 = ⊗r & ⊗p●r = ↑[f]p.
#f #p @(list_ind_rcons … p) -p
[ /2 width=3 by ex2_intro/
]
]
qed-.
+
+(* Inversions with inner condition for path *********************************)
+
+lemma lift_inv_append_inner_sn (q1) (q2) (p) (f):
+ q1 ϵ 𝐈 → q1●q2 = ↑[f]p →
+ ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
+#q1 @(list_ind_rcons … q1) -q1
+[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
+ /2 width=5 by ex3_2_intro/
+| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
+ [ elim (pic_inv_d_dx … Hq2)
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_m_sn … (sym_eq … H2))
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
+ [ <structure_append <structure_L_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
+ [ <structure_append <structure_A_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
+ [ <structure_append <structure_S_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ ]
+]
+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.ma".
+include "delayed_updating/notation/functions/class_i_0.ma".
+include "ground/lib/subset.ma".
+
+(* INNER CONDITION FOR PATH *************************************************)
+
+definition pic: predicate path ≝
+ λp. ∀q,n. q◖𝗱n = p → ⊥
+.
+
+interpretation
+ "inner condition (path)"
+ 'ClassI = (pic).
+
+(* Basic constructions ******************************************************)
+
+lemma pic_empty: 𝐞 ϵ 𝐈.
+#q #n #H0
+elim (eq_inv_list_empty_rcons ??? (sym_eq … H0))
+qed.
+
+lemma pic_m_dx (p): p◖𝗺 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+lemma pic_L_dx (p): p◖𝗟 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+lemma pic_A_dx (p): p◖𝗔 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+lemma pic_S_dx (p): p◖𝗦 ϵ 𝐈.
+#p #q #n #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+qed.
+
+(* Basic inversions ********************************************************)
+
+lemma pic_inv_d_dx (p) (n):
+ p◖𝗱n ϵ 𝐈 → ⊥.
+#p #n #H0 @H0 -H0 //
+qed-.
(* Basic inversions ********************************************************)
+lemma ppc_inv_empty:
+ (𝐞) ϵ 𝐏 → ⊥.
+#H0 @H0 -H0 //
+qed-.
+
lemma ppc_inv_lcons (p):
p ϵ 𝐏 → ∃∃l,q. l◗q = p.
*
-[ #H elim H -H //
+[ #H0 elim (ppc_inv_empty … H0)
| #l #q #_ /2 width=3 by ex1_2_intro/
]
qed-.
lemma eq_inv_list_empty_rcons (A):
∀l,a. ⓔ = l⨭{A}a → ⊥.
-#A #l #a #H
-elim (eq_inv_list_empty_append … H) -H #_ #H destruct
+#A #l #a #H0
+elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+lemma eq_inv_list_rcons_bi (A):
+ ∀a1,a2,l1,l2. l1 ⨭{A} a1 = l2 ⨭ a2 →
+ ∧∧ l1 = l2 & a1 = a2.
+#A #a1 #a2 #l1 elim l1 -l1 [| #b1 #l1 #IH ] *
+[ <list_append_empty_sn <list_append_empty_sn #H destruct
+ /2 width=1 by conj/
+| #b2 #l2 <list_append_empty_sn <list_append_lcons_sn #H destruct -H
+ elim (eq_inv_list_empty_rcons ??? e0)
+| <list_append_lcons_sn <list_append_empty_sn #H destruct -H
+ elim (eq_inv_list_empty_rcons ??? (sym_eq … e0))
+| #b2 #l2 <list_append_lcons_sn <list_append_lcons_sn #H destruct -H
+ elim (IH … e0) -IH -e0 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
qed-.
(* Advanced eliminations ****************************************************)
projects / helm.git / commitdiff