--- /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( p ᴿ )"
+ non associative with precedence 71
+ for @{ 'NEcR $p }.
--- /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_depth.ma".
+include "delayed_updating/syntax/path_reverse.ma".
+
+(* DEPTH FOR PATH ***********************************************************)
+
+(* Constructions with reverse ***********************************************)
+
+lemma depth_reverse (p):
+ ♭p = ♭pᴿ.
+#p elim p -p //
+* [ #n ] #p #IH <reverse_lcons
+[ <depth_d_sn <depth_d_dx //
+| <depth_m_sn <depth_m_dx //
+| <depth_L_sn <depth_L_dx //
+| <depth_A_sn <depth_A_dx //
+| <depth_S_sn <depth_S_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/syntax/path.ma".
+include "delayed_updating/notation/functions/nec_r_1.ma".
+
+(* REVERSE FOR PATH *********************************************************)
+
+rec definition reverse (p) on p: path ≝
+match p with
+[ list_empty ⇒ 𝐞
+| list_lcons l q ⇒ (reverse q)◖l
+].
+
+interpretation
+ "reverse (path)"
+ 'NEcR p = (reverse p).
+
+(* Basic constructions ******************************************************)
+
+lemma reverse_empty: 𝐞 = 𝐞ᴿ.
+// qed.
+
+lemma reverse_lcons (p) (l): pᴿ◖l = (l◗p)ᴿ.
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem reverse_append (p1) (p2):
+ (p2ᴿ)●(p1ᴿ) = (p1●p2)ᴿ.
+#p1 elim p1 -p1 //
+#l1 #p1 #IH #p2
+<list_append_lcons_sn <reverse_lcons <reverse_lcons //
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma reverse_rcons (p) (l):
+ l◗(pᴿ) = (p◖l)ᴿ.
+#p #l
+<reverse_append //
+qed.
+
+(* Main constructions *******************************************************)
+
+theorem reverse_reverse (p):
+ p = pᴿᴿ.
+#p elim p -p //
+#l #p #IH
+<reverse_lcons <reverse_rcons //
+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_structure.ma".
+include "delayed_updating/syntax/path_reverse.ma".
+
+(* STRUCTURE FOR PATH *******************************************************)
+
+(* Constructions with reverse ***********************************************)
+
+lemma structure_reverse (p):
+ (⊗p)ᴿ = ⊗(pᴿ).
+#p elim p -p //
+* [ #n ] #p #IH <reverse_lcons //
+[ <structure_d_sn <structure_d_dx //
+| <structure_m_sn <structure_m_dx //
+]
+qed.
--- /dev/null
+METAVARIABLES
+
+ b : balanced path
+ f, g : update function
+ h, k : reference index by depth
+ l : label
+ m, n : natural number
+ p, q, r, s: path
+ t, u, v, w: term
+++ /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( p ᴿ )"
- non associative with precedence 71
- for @{ 'NEcR $p }.
(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
inductive bdd: 𝒫❨prototerm❩ ≝
-| bdd_oref: ∀n. bdd (⧣n)
-| bdd_iref: ∀t,n. bdd t → bdd (𝛕n.t)
+| bdd_oref: ∀k. bdd (⧣k)
+| bdd_iref: ∀t,k. bdd t → bdd (𝛕k.t)
| bdd_abst: ∀t. bdd t → bdd (𝛌.t)
| bdd_appl: ∀u,t. bdd u → bdd t → bdd (＠u.t)
| bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
interpretation
"variable reference by depth (label)"
- 'NodeLabelD p = (label_d p).
+ 'NodeLabelD k = (label_d k).
interpretation
"mark (label)"
(* PATH *********************************************************************)
-(* Note: a path is a list of labels *)
+(* Note: a path is a list of labels *)
+(* Note: constructed from the leaf (right end) to the root (left end) *)
definition path ≝ list label.
interpretation
'ElementE = (list_empty label).
interpretation
- "left cons (paths)"
- 'BlackHalfCircleRight l p = (list_lcons label l p).
+ "right cons (paths)"
+ 'BlackHalfCircleLeft p l = (list_lcons label l p).
interpretation
"append (paths)"
- 'BlackCircle l1 l2 = (list_append label l1 l2).
+ 'BlackCircle p q = (list_append label q p).
interpretation
- "right cons (paths)"
- 'BlackHalfCircleLeft p l = (list_append label p (list_lcons label l (list_empty label))).
+ "left cons (paths)"
+ 'BlackHalfCircleRight l p = (list_append label p (list_lcons label l (list_empty label))).
lemma depth_empty: 𝟎 = ♭𝐞.
// qed.
-lemma depth_d_sn (q) (n): ♭q = ♭(𝗱n◗q).
+lemma depth_d_dx (p) (k):
+ ♭p = ♭(p◖𝗱k).
// qed.
-lemma depth_m_sn (q): ♭q = ♭(𝗺◗q).
+lemma depth_m_dx (p):
+ ♭p = ♭(p◖𝗺).
// qed.
-lemma depth_L_sn (q): ↑♭q = ♭(𝗟◗q).
+lemma depth_L_dx (p):
+ ↑♭p = ♭(p◖𝗟).
// qed.
-lemma depth_A_sn (q): ♭q = ♭(𝗔◗q).
+lemma depth_A_dx (p):
+ ♭p = ♭(p◖𝗔).
// qed.
-lemma depth_S_sn (q): ♭q = ♭(𝗦◗q).
+lemma depth_S_dx (p):
+ ♭p = ♭(p◖𝗦).
// qed.
(* Main constructions *******************************************************)
-theorem depth_append (p1) (p2):
- (♭p2)+(♭p1) = ♭(p1●p2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <depth_d_sn <depth_d_sn //
-| <depth_m_sn <depth_m_sn //
-| <depth_L_sn <depth_L_sn //
-| <depth_A_sn <depth_A_sn //
-| <depth_S_sn <depth_S_sn //
+theorem depth_append (p) (q):
+ (♭p)+(♭q) = ♭(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_m_dx <depth_m_dx //
+| <depth_L_dx <depth_L_dx //
+| <depth_A_dx <depth_A_dx //
+| <depth_S_dx <depth_S_dx //
]
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma depth_d_dx (p) (n):
- ♭p = ♭(p◖𝗱n).
+lemma depth_d_sn (p) (k):
+ ♭p = ♭(𝗱k◗p).
// qed.
-lemma depth_m_dx (p):
- ♭p = ♭(p◖𝗺).
+lemma depth_m_sn (p):
+ ♭p = ♭(𝗺◗p).
// qed.
-lemma depth_L_dx (p):
- ↑♭p = ♭(p◖𝗟).
+lemma depth_L_sn (p):
+ ↑♭p = ♭(𝗟◗p).
// qed.
-lemma depth_A_dx (p):
- ♭p = ♭(p◖𝗔).
+lemma depth_A_sn (p):
+ ♭p = ♭(𝗔◗p).
// qed.
-lemma depth_S_dx (p):
- ♭p = ♭(p◖𝗦).
+lemma depth_S_sn (p):
+ ♭p = ♭(𝗦◗p).
// qed.
lemma depth_labels_L (n):
n = ♭(𝗟∗∗n).
#n @(nat_ind_succ … n) -n //
-#n #IH <labels_succ <depth_L_sn //
+#n #IH <labels_succ <depth_L_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/syntax/path_depth.ma".
-include "delayed_updating/syntax/path_reverse.ma".
-
-(* DEPTH FOR PATH ***********************************************************)
-
-(* Constructions with reverse ***********************************************)
-
-lemma depth_reverse (p):
- ♭p = ♭pᴿ.
-#p elim p -p //
-* [ #n ] #p #IH <reverse_lcons
-[ <depth_d_sn <depth_d_dx //
-| <depth_m_sn <depth_m_dx //
-| <depth_L_sn <depth_L_dx //
-| <depth_A_sn <depth_A_dx //
-| <depth_S_sn <depth_S_dx //
-]
-qed.
(* HEAD FOR PATH ************************************************************)
-rec definition path_head (m) (p) on p: path ≝
-match m with
+rec definition path_head (n) (p) on p: path ≝
+match n with
[ nzero ⇒ 𝐞
-| ninj o ⇒
+| ninj m ⇒
match p with
- [ list_empty ⇒ 𝗟∗∗m
+ [ list_empty ⇒ 𝗟∗∗n
| list_lcons l q ⇒
match l with
- [ label_d n ⇒ l◗(path_head (m+n) q)
- | label_m ⇒ l◗(path_head m q)
- | label_L ⇒ l◗(path_head (↓o) q)
- | label_A ⇒ l◗(path_head m q)
- | label_S ⇒ l◗(path_head m q)
+ [ label_d k ⇒ (path_head (n+k) q)◖l
+ | label_m ⇒ (path_head n q)◖l
+ | label_L ⇒ (path_head (↓m) q)◖l
+ | label_A ⇒ (path_head n q)◖l
+ | label_S ⇒ (path_head n q)◖l
]
]
].
interpretation
- "head (reversed path)"
+ "head (path)"
'DownArrowRight n p = (path_head n p).
(* basic constructions ****************************************************)
(𝗟∗∗n) = ↳[n]𝐞.
* // qed.
-lemma path_head_d_sn (p) (n) (m:pnat):
- (𝗱m◗↳[↑n+m]p) = ↳[↑n](𝗱m◗p).
+lemma path_head_d_dx (p) (n) (k:pnat):
+ (↳[↑n+k]p)◖𝗱k = ↳[↑n](p◖𝗱k).
// qed.
-lemma path_head_m_sn (p) (n):
- (𝗺◗↳[↑n]p) = ↳[↑n](𝗺◗p).
+lemma path_head_m_dx (p) (n):
+ (↳[↑n]p)◖𝗺 = ↳[↑n](p◖𝗺).
// qed.
-lemma path_head_L_sn (p) (n):
- (𝗟◗↳[n]p) = ↳[↑n](𝗟◗p).
+lemma path_head_L_dx (p) (n):
+ (↳[n]p)◖𝗟 = ↳[↑n](p◖𝗟).
#p #n
whd in ⊢ (???%); //
qed.
-lemma path_head_A_sn (p) (n):
- (𝗔◗↳[↑n]p) = ↳[↑n](𝗔◗p).
+lemma path_head_A_dx (p) (n):
+ (↳[↑n]p)◖𝗔 = ↳[↑n](p◖𝗔).
// qed.
-lemma path_head_S_sn (p) (n):
- (𝗦◗↳[↑n]p) = ↳[↑n](𝗦◗p).
+lemma path_head_S_dx (p) (n):
+ (↳[↑n]p)◖𝗦 = ↳[↑n](p◖𝗦).
// qed.
(* Basic inversions *********************************************************)
lemma eq_inv_path_empty_head (p) (n):
(𝐞) = ↳[n]p → 𝟎 = n.
*
-[ #
m <path_head_empty #H0
- <(eq_inv_empty_labels … H0) -m //
-| * [ #n ] #p #n @(nat_ind_succ … n) -n // #m #_
- [ <path_head_d_sn
- | <path_head_m_sn
- | <path_head_L_sn
- | <path_head_A_sn
- | <path_head_S_sn
+[ #
n <path_head_empty #H0
+ <(eq_inv_empty_labels … H0) -n //
+| * [ #k ] #p #n @(nat_ind_succ … n) -n // #n #_
+ [ <path_head_d_dx
+ | <path_head_m_dx
+ | <path_head_L_dx
+ | <path_head_A_dx
+ | <path_head_S_dx
] #H0 destruct
]
qed-.
-(* Constructions with list_append *******************************************)
+(* Constructions with path_append *******************************************)
lemma path_head_refl_append (p) (q) (n):
- q = ↳[n]q → q = ↳[n](q●p).
+ q = ↳[n]q → q = ↳[n](p●q).
#p #q elim q -q
[ #n #Hn <(eq_inv_path_empty_head … Hn) -Hn //
| #l #q #IH #n @(nat_ind_succ … n) -n
- [ #Hq | #n #_ cases l [ #m ] ]
+ [ #Hq | #n #_ cases l [ #k ] ]
[ lapply (eq_inv_path_head_zero_dx … Hq) -Hq #Hq destruct
- | <path_head_d_sn <path_head_d_sn
- | <path_head_m_sn <path_head_m_sn
- | <path_head_L_sn <path_head_L_sn
- | <path_head_A_sn <path_head_A_sn
- | <path_head_S_sn <path_head_S_sn
+ | <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
] #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
/3 width=1 by eq_f/
]
qed-.
-(* Inversions with list_append **********************************************)
+(* Inversions with path_append **********************************************)
lemma eq_inv_path_head_refl_append (p) (q) (n):
- q = ↳[n](q●p) → q = ↳[n]q.
+ q = ↳[n](p●q) → q = ↳[n]q.
#p #q elim q -q
[ #n #Hn <(eq_inv_path_empty_head … Hn) -p //
| #l #q #IH #n @(nat_ind_succ … n) -n //
- #n #_ cases l [ #m ]
- [ <path_head_d_sn <path_head_d_sn
- | <path_head_m_sn <path_head_m_sn
- | <path_head_L_sn <path_head_L_sn
- | <path_head_A_sn <path_head_A_sn
- | <path_head_S_sn <path_head_S_sn
+ #n #_ cases l [ #k ]
+ [ <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
] #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
/3 width=1 by eq_f/
n + ♯(↳[n]p) = ♭↳[n]p.
#p elim p -p // #l #p #IH
#n @(nat_ind_succ … n) -n // #n #_
-cases l [ #m ]
-[ <path_head_d_sn <height_d_sn <depth_d_sn //
-| <path_head_m_sn <height_m_sn <depth_m_sn //
-| <path_head_L_sn <height_L_sn <depth_L_sn
+cases l [ #k ]
+[ <path_head_d_dx <height_d_dx <depth_d_dx <IH //
+| <path_head_m_dx <height_m_dx <depth_m_dx //
+| <path_head_L_dx <height_L_dx <depth_L_dx
<nplus_succ_sn //
-| <path_head_A_sn <height_A_sn <depth_A_sn //
-| <path_head_S_sn <height_S_sn <depth_S_sn //
+| <path_head_A_dx <height_A_dx <depth_A_dx //
+| <path_head_S_dx <height_S_dx <depth_S_dx //
]
qed-. (**) (* gets in the way with auto *)
(* Constructions with structure *********************************************)
-lemma path_head_structure_height (p) (m):
- ⊗↳[m]p = ↳[m+♯↳[m]p]⊗p.
+lemma path_head_structure_height (p) (n):
+ ⊗↳[n]p = ↳[n+♯↳[n]p]⊗p.
#p elim p -p //
-#l #p #IH #m @(nat_ind_succ … m) -m //
-#m #_ cases l [ #n ]
-[ <height_d_sn <structure_d_sn //
-| <structure_m_sn //
-| <structure_L_sn //
-| <height_A_sn <structure_A_sn <nplus_succ_sn <path_head_A_sn //
-| <height_S_sn <structure_S_sn <nplus_succ_sn <path_head_S_sn //
+#l #p #IH #n @(nat_ind_succ … n) -n //
+#n #_ cases l [ #k ]
+[ <height_d_dx <structure_d_dx //
+| <structure_m_dx //
+| <structure_L_dx //
+| <height_A_dx <structure_A_dx <nplus_succ_sn <path_head_A_dx //
+| <height_S_dx <structure_S_dx <nplus_succ_sn <path_head_S_dx //
]
qed.
-lemma path_head_structure_depth (p) (m):
- ⊗↳[m]p = ↳[♭↳[m]p]⊗p.
-#p #m
+lemma path_head_structure_depth (p) (n):
+ ⊗↳[n]p = ↳[♭↳[n]p]⊗p.
+#p #n
<path_head_depth //
qed.
[ list_empty ⇒ 𝟎
| list_lcons l q ⇒
match l with
- [ label_d n ⇒ n + height q
+ [ label_d k ⇒ height q + k
| label_m ⇒ height q
| label_L ⇒ height q
| label_A ⇒ height q
lemma height_empty: 𝟎 = ♯𝐞.
// qed.
-lemma height_d_sn (q) (n): ninj n+♯q = ♯(𝗱n◗q).
+lemma height_d_dx (p) (k:pnat):
+ (♯p)+k = ♯(p◖𝗱k).
// qed.
-lemma height_m_sn (q): ♯q = ♯(𝗺◗q).
+lemma height_m_dx (p):
+ (♯p) = ♯(p◖𝗺).
// qed.
-lemma height_L_sn (q): ♯q = ♯(𝗟◗q).
+lemma height_L_dx (p):
+ (♯p) = ♯(p◖𝗟).
// qed.
-lemma height_A_sn (q): ♯q = ♯(𝗔◗q).
+lemma height_A_dx (p):
+ (♯p) = ♯(p◖𝗔).
// qed.
-lemma height_S_sn (q): ♯q = ♯(𝗦◗q).
+lemma height_S_dx (p):
+ (♯p) = ♯(p◖𝗦).
// qed.
(* Main constructions *******************************************************)
-theorem height_append (p1) (p2):
- (♯p2+♯p1) = ♯(p1●p2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <height_d_sn <height_d_sn //
-| <height_m_sn <height_m_sn //
-| <height_L_sn <height_L_sn //
-| <height_A_sn <height_A_sn //
-| <height_S_sn <height_S_sn //
+theorem height_append (p) (q):
+ (♯p+♯q) = ♯(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <height_d_dx <height_d_dx //
+| <height_m_dx <height_m_dx //
+| <height_L_dx <height_L_dx //
+| <height_A_dx <height_A_dx //
+| <height_S_dx <height_S_dx //
]
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma height_d_dx (p) (n):
- (♯p)+(ninj n) = ♯(p◖𝗱n).
+lemma height_d_sn (p) (k:pnat):
+ k+♯p = ♯(𝗱k◗p).
// qed.
-lemma height_m_dx (p):
- (♯p) = ♯(p◖𝗺).
+lemma height_m_sn (p):
+ ♯p = ♯(𝗺◗p).
// qed.
-lemma height_L_dx (p):
- (♯p) = ♯(p◖𝗟).
+lemma height_L_sn (p):
+ ♯p = ♯(𝗟◗p).
// qed.
-lemma height_A_dx (p):
- (♯p) = ♯(p◖𝗔).
+lemma height_A_sn (p):
+ ♯p = ♯(𝗔◗p).
// qed.
-lemma height_S_dx (p):
- (♯p) = ♯(p◖𝗦).
+lemma height_S_sn (p):
+ ♯p = ♯(𝗦◗p).
// qed.
lemma height_labels_L (n):
(𝟎) = ♯(𝗟∗∗n).
#n @(nat_ind_succ … n) -n //
-#n #IH <labels_succ <height_L_sn //
+#n #IH <labels_succ <height_L_dx //
qed.
(* INNER CONDITION FOR PATH *************************************************)
definition pic: predicate path ≝
- λp. ∀q,n. q◖𝗱n = p → ⊥
+ λp. ∀q,k. q◖𝗱k = p → ⊥
.
interpretation
(* Basic constructions ******************************************************)
-lemma pic_empty: 𝐞 ϵ 𝐈.
-#q #n #H0
-elim (eq_inv_list_empty_rcons ??? (sym_eq … H0))
+lemma pic_empty:
+ (𝐞) ϵ 𝐈.
+#q #k #H0 destruct
qed.
-lemma pic_m_dx (p): p◖𝗺 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_m_dx (p):
+ p◖𝗺 ϵ 𝐈.
+#p #q #k #H0 destruct
qed.
-lemma pic_L_dx (p): p◖𝗟 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_L_dx (p):
+ p◖𝗟 ϵ 𝐈.
+#p #q #k #H0 destruct
qed.
-lemma pic_A_dx (p): p◖𝗔 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_A_dx (p):
+ p◖𝗔 ϵ 𝐈.
+#p #q #k #H0 destruct
qed.
-lemma pic_S_dx (p): p◖𝗦 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_S_dx (p):
+ p◖𝗦 ϵ 𝐈.
+#p #q #k #H0 destruct
qed.
(* Basic inversions ********************************************************)
-lemma pic_inv_d_dx (p) (n):
- p◖𝗱n ϵ 𝐈 → ⊥.
-#p #n #H0 @H0 -H0 //
+lemma pic_inv_d_dx (p) (k):
+ p◖𝗱k ϵ 𝐈 → ⊥.
+#p #k #H0 @H0 -H0 //
qed-.
// qed.
lemma labels_succ (l) (n):
- l◗(l∗∗n) = l∗∗(↑n).
+ (l∗∗n)◖l = l∗∗(↑n).
#l #n
<labels_unfold <labels_unfold <niter_succ //
qed.
(* Basic constructions ******************************************************)
-lemma ppc_lcons (l) (q): l◗q ϵ 𝐏.
-#l #q #H0 destruct
+lemma ppc_rcons (p) (l):
+ p◖l ϵ 𝐏.
+#p #l #H0 destruct
qed.
-lemma ppc_rcons (l) (q): q◖l ϵ 𝐏.
-#l #q #H
-elim (eq_inv_list_empty_rcons ??? H)
+lemma ppc_lcons (p) (l):
+ l◗p ϵ 𝐏.
+#p #l #H0
+elim (eq_inv_list_empty_rcons ??? H0)
qed.
(* Basic inversions ********************************************************)
#H0 @H0 -H0 //
qed-.
-lemma ppc_inv_lcons (p):
- p ϵ 𝐏 → ∃∃l,q. l◗q = p.
+lemma ppc_inv_rcons (p):
+ p ϵ 𝐏 → ∃∃q,l. q◖l = p.
*
[ #H0 elim (ppc_inv_empty … H0)
| #l #q #_ /2 width=3 by ex1_2_intro/
]
qed-.
-lemma ppc_inv_rcons (p):
- p ϵ 𝐏 → ∃∃q,l. q◖l = p.
+lemma ppc_inv_lcons (p):
+ p ϵ 𝐏 → ∃∃q,l. l◗q = p.
#p @(list_ind_rcons … p) -p
[ #H0 elim (ppc_inv_empty … H0)
| #q #l #_ #_ /2 width=3 by ex1_2_intro/
+++ /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/nec_r_1.ma".
-
-(* REVERSE FOR PATH *********************************************************)
-
-rec definition reverse (p) on p: path ≝
-match p with
-[ list_empty ⇒ 𝐞
-| list_lcons l q ⇒ (reverse q)◖l
-].
-
-interpretation
- "reverse (path)"
- 'NEcR p = (reverse p).
-
-(* Basic constructions ******************************************************)
-
-lemma reverse_empty: 𝐞 = 𝐞ᴿ.
-// qed.
-
-lemma reverse_lcons (p) (l): pᴿ◖l = (l◗p)ᴿ.
-// qed.
-
-(* Main constructions *******************************************************)
-
-theorem reverse_append (p1) (p2):
- (p2ᴿ)●(p1ᴿ) = (p1●p2)ᴿ.
-#p1 elim p1 -p1 //
-#l1 #p1 #IH #p2
-<list_append_lcons_sn <reverse_lcons <reverse_lcons //
-qed.
-
-(* Constructions with list_rcons ********************************************)
-
-lemma reverse_rcons (p) (l):
- l◗(pᴿ) = (p◖l)ᴿ.
-#p #l
-<reverse_append //
-qed.
-
-(* Main constructions *******************************************************)
-
-theorem reverse_reverse (p):
- p = pᴿᴿ.
-#p elim p -p //
-#l #p #IH
-<reverse_lcons <reverse_rcons //
-qed.
[ list_empty ⇒ 𝐞
| list_lcons l q ⇒
match l with
- [ label_d n ⇒ structure q
+ [ label_d k ⇒ structure q
| label_m ⇒ structure q
- | label_L ⇒ 𝗟◗structure q
- | label_A ⇒ 𝗔◗structure q
- | label_S ⇒ 𝗦◗structure q
+ | label_L ⇒ (structure q)◖𝗟
+ | label_A ⇒ (structure q)◖𝗔
+ | label_S ⇒ (structure q)◖𝗦
]
].
𝐞 = ⊗𝐞.
// qed.
-lemma structure_d_sn (p) (n):
- ⊗p = ⊗(𝗱n◗p).
+lemma structure_d_dx (p) (k):
+ ⊗p = ⊗(p◖𝗱k).
// qed.
-lemma structure_m_sn (p):
- ⊗p = ⊗(𝗺◗p).
+lemma structure_m_dx (p):
+ ⊗p = ⊗(p◖𝗺).
// qed.
-lemma structure_L_sn (p):
- (𝗟◗⊗p) = ⊗(𝗟◗p).
+lemma structure_L_dx (p):
+ (⊗p)◖𝗟 = ⊗(p◖𝗟).
// qed.
-lemma structure_A_sn (p):
- (𝗔◗⊗p) = ⊗(𝗔◗p).
+lemma structure_A_dx (p):
+ (⊗p)◖𝗔 = ⊗(p◖𝗔).
// qed.
-lemma structure_S_sn (p):
- (𝗦◗⊗p) = ⊗(𝗦◗p).
+lemma structure_S_dx (p):
+ (⊗p)◖𝗦 = ⊗(p◖𝗦).
// qed.
(* Main constructions *******************************************************)
theorem structure_idem (p):
⊗p = ⊗⊗p.
-#p elim p -p [| * [ #n ] #p #IH ] //
+#p elim p -p [| * [ #k ] #p #IH ] //
qed.
-theorem structure_append (p1) (p2):
- ⊗p1●⊗p2 = ⊗(p1●p2).
-#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+theorem structure_append (p) (q):
+ ⊗p●⊗q = ⊗(p●q).
+#p #q elim q -q [| * [ #k ] #q #IH ]
[||*: <list_append_lcons_sn ] //
qed.
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma structure_d_dx (p) (n):
- ⊗p = ⊗(p◖𝗱n).
+lemma structure_d_sn (p) (k):
+ ⊗p = ⊗(𝗱k◗p).
#p #n <structure_append //
qed.
-lemma structure_m_dx (p):
- ⊗p = ⊗(p◖𝗺).
+lemma structure_m_sn (p):
+ ⊗p = ⊗(𝗺◗p).
#p <structure_append //
qed.
-lemma structure_L_dx (p):
- (⊗p)◖𝗟 = ⊗(p◖𝗟).
+lemma structure_L_sn (p):
+ (𝗟◗⊗p) = ⊗(𝗟◗p).
#p <structure_append //
qed.
-lemma structure_A_dx (p):
- (⊗p)◖𝗔 = ⊗(p◖𝗔).
+lemma structure_A_sn (p):
+ (𝗔◗⊗p) = ⊗(𝗔◗p).
#p <structure_append //
qed.
-lemma structure_S_dx (p):
- (⊗p)◖𝗦 = ⊗(p◖𝗦).
+lemma structure_S_sn (p):
+ (𝗦◗⊗p) = ⊗(𝗦◗p).
#p <structure_append //
qed.
lemma depth_structure (p):
♭p = ♭⊗p.
#p elim p -p //
-* [ #n ] #p #IH //
-[ <structure_L_sn <depth_L_sn <depth_L_sn //
-| <structure_A_sn <depth_A_sn <depth_A_sn //
-| <structure_S_sn <depth_S_sn <depth_S_sn //
+* [ #k ] #p #IH //
+[ <structure_L_dx <depth_L_dx <depth_L_dx //
+| <structure_A_dx <depth_A_dx <depth_A_dx //
+| <structure_S_dx <depth_S_dx <depth_S_dx //
]
qed.
lemma structure_pic (p):
⊗p ϵ 𝐈.
-#p @(list_ind_rcons … p) -p
+#p elim p -p
[ <structure_empty //
-| #p * [ #n ] #IH
+| * [ #k ] #p #IH
[ <structure_d_dx //
| <structure_m_dx //
| <structure_L_dx //
+++ /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_structure.ma".
-include "delayed_updating/syntax/path_reverse.ma".
-
-(* STRUCTURE FOR PATH *******************************************************)
-
-(* Constructions with reverse ***********************************************)
-
-lemma structure_reverse (p):
- (⊗p)ᴿ = ⊗(pᴿ).
-#p elim p -p //
-* [ #n ] #p #IH <reverse_lcons //
-[ <structure_d_sn <structure_d_dx //
-| <structure_m_sn <structure_m_dx //
-]
-qed.
(* Basic inversions *********************************************************)
-lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (r):
- p●r ϵ ▵t → t ϵ 𝐓 → 𝐞 = ⊗r → 𝐞 = r.
-#t #p #r #Hpr #Ht #Hr
-lapply (Ht p ?? Hpr ?)
+lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (q):
+ p●q ϵ ▵t → t ϵ 𝐓 → 𝐞 = ⊗q → 𝐞 = q.
+#t #p #q #Hpq #Ht #Hq
+lapply (Ht p ?? Hpq ?)
[ <structure_append //
| /2 width=2 by prototerm_in_root_append_des_sn/
-| /2 width=3 by eq_inv_list_append_dx_sn_refl/
+| /2 width=3 by eq_inv_list_append_dx_dx_refl/
]
qed-.
interpretation
"outer variable reference by depth (prototerm)"
- 'Hash n = (prototerm_node_0 (label_d n)).
+ 'Hash k = (prototerm_node_0 (label_d k)).
interpretation
"inner variable reference by depth (prototerm)"
- 'Tau n t = (prototerm_node_1_2 (label_d n) label_m t).
+ 'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
interpretation
"name-free functional abstraction (prototerm)"
(* Basic constructions *******************************************************)
-lemma in_comp_iref (t) (q) (n):
- q ϵ t → 𝗱n◗𝗺◗q ϵ 𝛕n.t.
+lemma in_comp_iref (t) (q) (k):
+ q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
/2 width=3 by ex2_intro/ qed.
(* Basic inversions *********************************************************)
-lemma in_comp_inv_iref (t) (p) (n):
- p ϵ 𝛕n.t →
- ∃∃q. 𝗱n◗𝗺◗q = p & q ϵ t.
-#t #p #n * #q #Hq #Hp
+lemma in_comp_inv_iref (t) (p) (k):
+ p ϵ 𝛕k.t →
+ ∃∃q. 𝗱k◗𝗺◗q = p & q ϵ t.
+#t #p #k * #q #Hq #Hp
/2 width=3 by ex2_intro/
qed-.
+
(* COMMENT
lemma prototerm_in_root_inv_lcons_oref:
∀p,l,n. l◗p ϵ ▵#n →
(* Constructions with equivalence for prototerm *****************************)
-lemma iref_eq_repl (t1) (t2) (n):
- t1 ⇔ t2 → 𝛕n.t1 ⇔ 𝛕n.t2.
+lemma iref_eq_repl (t1) (t2) (k):
+ t1 ⇔ t2 → 𝛕k.t1 ⇔ 𝛕k.t2.
/2 width=1 by subset_equivalence_ext_f1_bi/
qed.
(* Constructions with prototerm constructors ********************************)
-lemma ppc_iref (t) (n):
- (𝛕n.t) ϵ 𝐏.
-#t #n #p * #q #Hq #H0 destruct //
+lemma ppc_iref (t) (k):
+ (𝛕k.t) ϵ 𝐏.
+#t #k #p * #q #Hq #H0 destruct //
qed.
@pull_2 #l2 elim l2 -l2 //
#a2 #l2 #IH0 #l1 #IH /3 width=1 by/
qed-.
+
+(* Advanced inversions with list_append *************************************)
+
+lemma eq_inv_list_append_dx_dx_refl (A) (l1) (l2):
+ l1 = l2⨁{A}l1 → ⓔ = l2.
+#A #l1 @(list_ind_rcons … l1) -l1 [ // ]
+#l1 #a1 #IH #l2 <list_append_rcons_dx #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
+/2 width=1 by/
+qed-.
projects / helm.git / commitdiff