Fold-and-reorder theory for iterated single-pair gluing

Iterated single-pair gluing over a list of pairs, with a well-formedness predicate (all 2n components pairwise distinct) and a reorder theorem: the result is invariant under permutation of the pair list, up to fragment equivalence composed with the canonical relabelling.

Well-formedness of pair lists

def RS.Fragment.PairsWF {α : Type} (ps : List (α × α)) : Prop

All 2n components of a list of pairs are pairwise distinct.

Equations

• RS.Fragment.PairsWF ps = (List.flatMap (fun (p : α × α) => [p.1, p.2]) ps).Nodup

theorem RS.Fragment.PairsWF.nil {α : Type} : PairsWF []

The empty list is trivially well-formed.

theorem RS.Fragment.PairsWF.head_ne {α : Type} {p : α × α} {ps : List (α × α)} (h : PairsWF (p :: ps)) : p.1 ≠ p.2

The components of the head pair are distinct.

theorem RS.Fragment.PairsWF.tail {α : Type} {p : α × α} {ps : List (α × α)} (h : PairsWF (p :: ps)) : PairsWF ps

The tail of a well-formed pair list is well-formed.

theorem RS.Fragment.PairsWF.head_disjoint_of {α : Type} {i j : α} {ps : List (α × α)} (h : PairsWF ((i, j) :: ps)) (q : α × α) (hq : q ∈ ps) : PairDisjoint q (i, j)

The head pair of a well-formed list shares no label with any pair of the tail.

theorem RS.Fragment.PairsWF.perm {α : Type} {ps qs : List (α × α)} (h : PairsWF ps) (hperm : ps.Perm qs) : PairsWF qs

Well-formedness is preserved by permutation of the pair list.

The flat surviving subtype

def RS.Fragment.FoldSurviving (α : Type) (ps : List (α × α)) : Type

The labels surviving all glues in a pair list: those not appearing as any component of any pair.

Equations

• RS.Fragment.FoldSurviving α ps = { x : α // ∀ p ∈ ps, x ≠ p.1 ∧ x ≠ p.2 }

def RS.Fragment.foldSurvivingNilEquiv {α : Type} : FoldSurviving α [] ≃ α

The vacuous surviving equivalence for the empty list.

Equations

• RS.Fragment.foldSurvivingNilEquiv = { toFun := fun (x : RS.Fragment.FoldSurviving α []) => ↑x, invFun := fun (x : α) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def RS.Fragment.foldSurvivingPermEquiv {α : Type} {ps qs : List (α × α)} (hperm : ps.Perm qs) : FoldSurviving α ps ≃ FoldSurviving α qs

The surviving-set equivalence induced by a permutation of pairs: the membership condition is ∀-quantified over ∈, so a permutation preserving membership gives an equivalence.

Equations

• One or more equations did not get rendered due to their size.

Coercing tail pairs into the surviving-label subtype

@[reducible, inline]

abbrev RS.Fragment.PairsSep {α : Type} (i j : α) (ps : List (α × α)) : Prop

The separation hypothesis for coercing pairs.

Equations

• RS.Fragment.PairsSep i j ps = ∀ q ∈ ps, RS.PairDisjoint q (i, j)

theorem RS.Fragment.PairsWF.sep {α : Type} {i j : α} {ps : List (α × α)} (h : PairsWF ((i, j) :: ps)) : PairsSep i j ps

Extract the separation hypothesis from PairsWF.

def RS.Fragment.coercePairsList {α : Type} (i j : α) (ps : List (α × α)) : PairsSep i j ps → List (SurvivingLabel α i j × SurvivingLabel α i j)

Coerce a well-formed tail into pairs of surviving labels.

Equations

• RS.Fragment.coercePairsList i j [] x_2 = []
• RS.Fragment.coercePairsList i j (q :: ps) h = (⟨q.1, ⋯⟩, ⟨q.2, ⋯⟩) :: RS.Fragment.coercePairsList i j ps ⋯

theorem RS.Fragment.coercePairsList_length {α : Type} (i j : α) (ps : List (α × α)) (h : PairsSep i j ps) : (coercePairsList i j ps h).length = ps.length

Length of coercePairsList equals the original list length.

theorem RS.Fragment.coercePairsList_flatMap_map_val {α : Type} (i j : α) (ps : List (α × α)) (h : PairsSep i j ps) : List.map Subtype.val (List.flatMap (fun (r : SurvivingLabel α i j × SurvivingLabel α i j) => [r.1, r.2]) (coercePairsList i j ps h)) = List.flatMap (fun (q : α × α) => [q.1, q.2]) ps

The val-projection of the flattened coerced list equals the original flattened list.

theorem RS.Fragment.coercePairsList_wf {α : Type} (i j : α) (ps : List (α × α)) (hwf : PairsWF ps) (h : PairsSep i j ps) : PairsWF (coercePairsList i j ps h)

Well-formedness of the coerced pairs.

theorem RS.Fragment.coercePairsList_mem_of {α : Type} (i j : α) (ps : List (α × α)) (h : PairsSep i j ps) (r : SurvivingLabel α i j × SurvivingLabel α i j) : r ∈ coercePairsList i j ps h → ∃ q ∈ ps, ↑r.1 = q.1 ∧ ↑r.2 = q.2

Each element of coercePairsList comes from an element of ps.

theorem RS.Fragment.coercePairsList_mem {α : Type} (i j : α) (ps : List (α × α)) (h : PairsSep i j ps) (q : α × α) : q ∈ ps → ∃ r ∈ coercePairsList i j ps h, ↑r.1 = q.1 ∧ ↑r.2 = q.2

Membership in coercePairsList: if q ∈ ps then the coerced version is in coercePairsList.

The flattening equivalence

def RS.Fragment.foldFlatten {α : Type} (i j : α) (ps : List (α × α)) (h : PairsSep i j ps) : FoldSurviving (SurvivingLabel α i j) (coercePairsList i j ps h) ≃ FoldSurviving α ((i, j) :: ps)

The canonical equivalence between the nested surviving type (first remove i, j from α to get SurvivingLabel; then remove the coerced tail pairs) and the flat surviving type (remove (i, j) :: ps at once).

Equations

• One or more equations did not get rendered due to their size.

The fold: iterated single-pair gluing

noncomputable def RS.Fragment.glueListAux (n : ℕ) {α : Type} (W : Fragment α) (ps : List (α × α)) : PairsWF ps → ps.length ≤ n → Fragment (FoldSurviving α ps)

Fold a well-formed pair list using a bound on its length as structural fuel.

Equations

• RS.Fragment.glueListAux x✝² x✝ [] x_8 x_9 = x✝.relabel RS.Fragment.foldSurvivingNilEquiv.symm
• RS.Fragment.glueListAux n.succ x✝ ((i, j) :: ps) h hlen = (RS.Fragment.glueListAux n (x✝.gluePair i j ⋯) (RS.Fragment.coercePairsList i j ps ⋯) ⋯ ⋯).relabel (RS.Fragment.foldFlatten i j ps ⋯)

noncomputable def RS.Fragment.glueList {α : Type} (W : Fragment α) (ps : List (α × α)) (h : PairsWF ps) : Fragment (FoldSurviving α ps)

Iterated single-pair gluing along a list of distinct pairs. Glues each pair in order; the result is labelled by the elements of α not appearing in any pair.

Equations

• W.glueList ps h = RS.Fragment.glueListAux ps.length W ps h ⋯

theorem RS.Fragment.glueList_nil {α : Type} (W : Fragment α) (h : PairsWF []) : W.glueList [] h = W.relabel foldSurvivingNilEquiv.symm

Unfolding glueList at the empty list.

theorem RS.Fragment.glueList_cons {α : Type} (W : Fragment α) (p : α × α) (ps : List (α × α)) (hp : PairsWF (p :: ps)) : W.glueList (p :: ps) hp = ((W.gluePair p.1 p.2 ⋯).glueList (coercePairsList p.1 p.2 ps ⋯) ⋯).relabel (foldFlatten p.1 p.2 ps ⋯)

Unfolding glueList at a cons.

Congruence: glueList respects fragment equivalence

noncomputable def RS.Fragment.glueListCongrAux (n : ℕ) {α : Type} {W₁ W₂ : Fragment α} (he : W₁.Equiv W₂) (ps : List (α × α)) (h : PairsWF ps) (hn : ps.length ≤ n) : (glueListAux n W₁ ps h hn).Equiv (glueListAux n W₂ ps h hn)

Transport a bounded pair-list fold along an equivalence of input fragments.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Fragment.glueListCongr {α : Type} {W₁ W₂ : Fragment α} (he : W₁.Equiv W₂) (ps : List (α × α)) (h : PairsWF ps) : (W₁.glueList ps h).Equiv (W₂.glueList ps h)

glueList respects fragment equivalence: equivalent inputs produce equivalent outputs.

Equations

• RS.Fragment.glueListCongr he ps h = RS.Fragment.glueListCongrAux ps.length he ps h ⋯

Relabelling commutes with the fold

def RS.Fragment.mapPairs {α : Type} {β : Type u_1} (e : α ≃ β) (ps : List (α × α)) : List (β × β)

Map a pair list through an equivalence.

Equations

• RS.Fragment.mapPairs e ps = List.map (Prod.map ⇑e ⇑e) ps

theorem RS.Fragment.mapPairs_wf {α β : Type} (e : α ≃ β) (ps : List (α × α)) (hp : PairsWF ps) : PairsWF (mapPairs e ps)

Well-formedness is preserved by mapping through an equivalence.

def RS.Fragment.foldSurvivingMapEquiv {α β : Type} (e : α ≃ β) (ps : List (α × α)) : FoldSurviving α ps ≃ FoldSurviving β (mapPairs e ps)

The canonical equivalence on FoldSurviving induced by a label equivalence.

Equations

• One or more equations did not get rendered due to their size.

def RS.Fragment.survLabelMapEquiv {α β : Type} (e : α ≃ β) (i j : α) : SurvivingLabel α i j ≃ SurvivingLabel β (e i) (e j)

The surviving-label equivalence induced by a label equiv.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Fragment.glueListEqEquiv {α : Type} (W : Fragment α) {ps qs : List (α × α)} (h : ps = qs) (hp : PairsWF ps) (hq : PairsWF qs) (hperm : ps.Perm qs) : ((W.glueList ps hp).relabel (foldSurvivingPermEquiv hperm)).Equiv (W.glueList qs hq)

Casting a glueList result along a list equality: relabelling by the induced foldSurvivingPermEquiv bridges the type change.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Fragment.glueListRelabel {α β : Type} (W : Fragment α) (e : α ≃ β) (ps : List (α × α)) (hp : PairsWF ps) : ((W.relabel e).glueList (mapPairs e ps) ⋯).Equiv ((W.glueList ps hp).relabel (foldSurvivingMapEquiv e ps))

Iterated gluing commutes with relabelling: gluing the mapped pairs in the relabelled fragment is the original fold, relabelled by the induced surviving-label equivalence.

Equations

• W.glueListRelabel e ps hp = ⋯.some

Concatenation: folding in two stages

@[reducible, inline]

abbrev RS.Fragment.PairsSepAll {α : Type} (ps qs : List (α × α)) : Prop

The separation of the second block from the first.

Equations

• RS.Fragment.PairsSepAll ps qs = ∀ q ∈ qs, ∀ p ∈ ps, RS.PairDisjoint q p

def RS.Fragment.liftPairs {α : Type} (ps qs : List (α × α)) : PairsSepAll ps qs → List (FoldSurviving α ps × FoldSurviving α ps)

Pairs avoiding an earlier pair list lift into its surviving labels.

Equations

• RS.Fragment.liftPairs ps [] x_2 = []
• RS.Fragment.liftPairs ps (q :: qs) h = (⟨q.1, ⋯⟩, ⟨q.2, ⋯⟩) :: RS.Fragment.liftPairs ps qs ⋯

theorem RS.Fragment.PairsWF.append_sep {α : Type} {ps qs : List (α × α)} (h : PairsWF (ps ++ qs)) : PairsSepAll ps qs

The separation hypothesis of a well-formed concatenation.

theorem RS.Fragment.PairsWF.append_left {α : Type} {ps qs : List (α × α)} (h : PairsWF (ps ++ qs)) : PairsWF ps

The first block of a well-formed concatenation.

theorem RS.Fragment.PairsWF.append_right {α : Type} {ps qs : List (α × α)} (h : PairsWF (ps ++ qs)) : PairsWF qs

The second block of a well-formed concatenation.

theorem RS.Fragment.liftPairs_flatMap_map_val {α : Type} (ps qs : List (α × α)) (h : PairsSepAll ps qs) : List.map Subtype.val (List.flatMap (fun (r : FoldSurviving α ps × FoldSurviving α ps) => [r.1, r.2]) (liftPairs ps qs h)) = List.flatMap (fun (q : α × α) => [q.1, q.2]) qs

The val-projection of the flattened lifted list is the original flattened list.

theorem RS.Fragment.liftPairs_wf {α : Type} (ps qs : List (α × α)) (hwf : PairsWF qs) (h : PairsSepAll ps qs) : PairsWF (liftPairs ps qs h)

The lifted second block is well-formed.

theorem RS.Fragment.liftPairs_mem_of {α : Type} (ps qs : List (α × α)) (h : PairsSepAll ps qs) (r : FoldSurviving α ps × FoldSurviving α ps) : r ∈ liftPairs ps qs h → ∃ q ∈ qs, ↑r.1 = q.1 ∧ ↑r.2 = q.2

Each lifted pair comes from an original pair.

theorem RS.Fragment.liftPairs_mem {α : Type} (ps qs : List (α × α)) (h : PairsSepAll ps qs) (q : α × α) : q ∈ qs → ∃ r ∈ liftPairs ps qs h, ↑r.1 = q.1 ∧ ↑r.2 = q.2

Each original pair lifts to a member.

def RS.Fragment.appendFlatten {α : Type} (ps qs : List (α × α)) (h : PairsSepAll ps qs) : FoldSurviving (FoldSurviving α ps) (liftPairs ps qs h) ≃ FoldSurviving α (ps ++ qs)

The two-stage surviving labels flatten to the concatenation's surviving labels.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Fragment.coercePairsList_append {α : Type} (i j : α) (ps qs : List (α × α)) (h : PairsSep i j (ps ++ qs)) : coercePairsList i j (ps ++ qs) h = coercePairsList i j ps ⋯ ++ coercePairsList i j qs ⋯

Coercing a concatenation coerces blockwise.

noncomputable def RS.Fragment.glueListAppend {α : Type} (W : Fragment α) (ps qs : List (α × α)) (h : PairsWF (ps ++ qs)) : (W.glueList (ps ++ qs) h).Equiv (((W.glueList ps ⋯).glueList (liftPairs ps qs ⋯) ⋯).relabel (appendFlatten ps qs ⋯))

Two-stage folding: gluing a concatenation of pair lists is gluing the first block, then the lifted second block, up to the flattening of survivors.

Equations

• W.glueListAppend ps qs h = ⋯.some

Disjoint-union embedding: left

def RS.Fragment.inlPairs {α : Type} {β : Type u_1} (ps : List (α × α)) : List ((α ⊕ β) × (α ⊕ β))

Embed a pair list into the left summand of a disjoint union.

Equations

• RS.Fragment.inlPairs ps = List.map (Prod.map Sum.inl Sum.inl) ps

theorem RS.Fragment.inlPairs_wf {α β : Type} (ps : List (α × α)) (hp : PairsWF ps) : PairsWF (inlPairs ps)

inlPairs preserves well-formedness.

def RS.Fragment.inlFoldEquiv {α β : Type} (ps : List (α × α)) : FoldSurviving (α ⊕ β) (inlPairs ps) ≃ FoldSurviving α ps ⊕ β

The surviving-label equivalence for left-embedded pairs: inl-labels survive iff they survive the original list; all inr-labels survive.

Equations

• One or more equations did not get rendered due to their size.

Disjoint-union embedding: right

def RS.Fragment.inrPairs {α : Type} {β : Type u_1} (qs : List (β × β)) : List ((α ⊕ β) × (α ⊕ β))

Embed a pair list into the right summand of a disjoint union.

Equations

• RS.Fragment.inrPairs qs = List.map (Prod.map Sum.inr Sum.inr) qs

theorem RS.Fragment.inrPairs_wf {α β : Type} (qs : List (β × β)) (hq : PairsWF qs) : PairsWF (inrPairs qs)

inrPairs preserves well-formedness.

def RS.Fragment.inrFoldEquiv {α β : Type} (qs : List (β × β)) : FoldSurviving (α ⊕ β) (inrPairs qs) ≃ α ⊕ FoldSurviving β qs

The surviving-label equivalence for right-embedded pairs: inr-labels survive iff they survive the original list; all inl-labels survive.

Equations

• One or more equations did not get rendered due to their size.

Helpers for disjoint-union embedding proofs

Disjoint-union left: main induction

noncomputable def RS.Fragment.glueListDisjUnionLeft {α β : Type} (W₁ : Fragment α) (W₂ : Fragment β) (ps : List (α × α)) (hp : PairsWF ps) : ((W₁.disjUnion W₂).glueList (inlPairs ps) ⋯).Equiv (((W₁.glueList ps hp).disjUnion W₂).relabel (inlFoldEquiv ps).symm)

Iterated left-side gluing commutes with disjoint union: gluing the inlPairs-embedded pair list in the disjoint union is equivalent to gluing W₁ alone and then taking the disjoint union with W₂, up to the canonical label isomorphism inlFoldEquiv.

Equations

• W₁.glueListDisjUnionLeft W₂ ps hp = ⋯.some

noncomputable def RS.Fragment.glueListDisjUnionRight {α β : Type} (W₁ : Fragment α) (W₂ : Fragment β) (qs : List (β × β)) (hq : PairsWF qs) : ((W₁.disjUnion W₂).glueList (inrPairs qs) ⋯).Equiv ((W₁.disjUnion (W₂.glueList qs hq)).relabel (inrFoldEquiv qs).symm)

Iterated right-side gluing commutes with disjoint union: gluing the inrPairs-embedded pair list in the disjoint union is equivalent to gluing W₂ alone and then taking the disjoint union with W₁, up to the canonical label isomorphism inrFoldEquiv.

Equations

• One or more equations did not get rendered due to their size.

The swap-components fold lemma

theorem RS.Fragment.swapPairs_wf {α : Type} (ps : List (α × α)) (hp : PairsWF ps) : PairsWF (List.map Prod.swap ps)

Swapping every pair preserves well-formedness.

def RS.Fragment.swapFoldEquiv {α : Type} (ps : List (α × α)) : FoldSurviving α (List.map Prod.swap ps) ≃ FoldSurviving α ps

Surviving labels are invariant under swapping pair components: x ≠ p.1 ∧ x ≠ p.2 iff x ≠ p.2 ∧ x ≠ p.1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.Fragment.glueListSwap {α : Type} (W : Fragment α) (ps : List (α × α)) (hp : PairsWF ps) : (W.glueList (List.map Prod.swap ps) ⋯).Equiv ((W.glueList ps hp).relabel (swapFoldEquiv ps).symm)

Gluing a pair list is symmetric in each pair's components: swapping every (i,j) to (j,i) yields an equivalent fold, up to the canonical swapFoldEquiv.

Equations

• W.glueListSwap ps hp = ⋯.some

The reorder theorem

noncomputable def RS.Fragment.glueListPerm {α : Type} (W : Fragment α) {ps qs : List (α × α)} (hperm : ps.Perm qs) (hp : PairsWF ps) : (W.glueList ps hp).Equiv ((W.glueList qs ⋯).relabel (foldSurvivingPermEquiv hperm).symm)

The reorder theorem: gluing along a permuted pair list yields an equivalent fragment (up to the canonical relabelling of survivors).

Equations

• W.glueListPerm hperm hp = ⋯.some