Flipping a tableau (for section 7)

Like the paper, we only prove interpolation for clusters with a loaded formulas on the right side. For the case where the loaded formula is on the left, we flip the tableau left-to-right.

The lemmas here then allow us to prove clusterInterpolation from clusterInterpolation_right.

def Olf.flip : Olf → Olf

Equations

• Olf.flip = Option.map Sum.swap

@[simp]

theorem Olf.flip_inj {O1 O2 : Olf} : O1.flip = O2.flip ↔ O1 = O2

@[simp]

theorem Olf.flip_flip {O : Olf} : O.flip.flip = O

@[simp]

theorem Olf.flip_none : flip none = none

def Sequent.flip : Sequent → Sequent

Equations

• Sequent.flip (L, R, O) = (R, L, O.flip)

@[simp]

theorem Sequent.flip_right {X : Sequent} : X.flip.right = X.left

@[simp]

theorem Sequent.flip_left {X : Sequent} : X.flip.left = X.right

@[simp]

theorem Sequent.flip_flip {X : Sequent} : X.flip.flip = X

@[simp]

theorem Sequent.flip_isLoaded {X : Sequent} : X.flip.isLoaded ↔ X.isLoaded

@[simp]

theorem Sequent.flip_isFree {X : Sequent} : X.flip.isFree ↔ X.isFree

theorem Sequent.flip_eq_off {X Y : Sequent} : (X.flip = Y) = (X = Y.flip)

@[simp]

theorem Sequent.map_flip_map_flip {Hist : List Sequent} : List.map flip (List.map flip Hist) = Hist

@[simp]

theorem Sequent.image_flip_image_flip {S : Finset Sequent} : Finset.image flip (Finset.image flip S) = S

Flipping all sequents in a Finset twice gives back the same set.

@[simp]

theorem basic_flip {X : Sequent} : X.flip.basic ↔ X.basic

def LocalRule.flip {Lcond Rcond : Finset Formula} {Ocond : Olf} {ress : Finset Sequent} (lr : LocalRule (Lcond, Rcond, Ocond) ress) : LocalRule (Rcond, Lcond, Ocond.flip) (Finset.image Sequent.flip ress)

Equations

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

theorem LocalRule.flip_flip {Lcond Rcond : Finset Formula} {Ocond : Olf} {ress : Finset Sequent} (lr : LocalRule (Lcond, Rcond, Ocond) ress) : lr.flip.flip = ⋯ ▸ ⋯ ▸ lr

def LocalRuleApp.flip : LocalRuleApp → LocalRuleApp

Note: is it possible and useful to rewrite this in more term and less tactic mode?

Equations

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

@[simp]

theorem Sequent.flip_comp_flip : flip ∘ flip = id

theorem LocalRuleApp.flip_flip {lra : LocalRuleApp} : lra.flip.flip = lra

theorem Sequent.flip_mem_of_mem_image_flip {B : Finset Sequent} {Y : Sequent} : Y ∈ Finset.image flip B → Y.flip ∈ B

def LocalTableau.flip {X : Sequent} : LocalTableau X → LocalTableau X.flip

Equations

• (LocalTableau.byLocalRule lra X_def next).flip = LocalTableau.byLocalRule lra.flip ⋯ fun (Y : Sequent) (Y_in : Y ∈ lra.flip.C) => ⋯ ▸ (next Y.flip ⋯).flip
• (LocalTableau.sim Xbas).flip = LocalTableau.sim ⋯

theorem LocalTableau.flip_flip {X : Sequent} {lt : LocalTableau X} : lt.flip.flip = ⋯ ▸ lt

theorem LocalTableau.flip_inj {X : Sequent} {lt : LocalTableau X} : lt.flip.flip = ⋯ ▸ lt

theorem endNodesOf_flip {X : Sequent} {lt : LocalTableau X} {Y : Sequent} : Y ∈ endNodesOf lt.flip → Y.flip ∈ endNodesOf lt

def PdlRule.flip {X Y : Sequent} (r : PdlRule X Y) : PdlRule X.flip Y.flip

Equations

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

theorem PdlRule.flip_flip {X Y : Sequent} (r : PdlRule X Y) : r.flip.flip = ⋯ ▸ ⋯ ▸ r

@[simp]

theorem Sequent.flip_eq_flip_iff {X Y : Sequent} : X.flip = Y.flip ↔ X = Y

Flipping sequents is injective.

def LoadedPathRepeat.flip {Hist : History} {X : Sequent} : LoadedPathRepeat Hist X → LoadedPathRepeat (List.map Sequent.flip Hist) X.flip

Equations

• LoadedPathRepeat.flip ⟨k, hk⟩ = ⟨⟨↑k, ⋯⟩, ⋯⟩

theorem LoadedPathRepeat.flip_flip {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) : lpr.flip.flip = ⋯ ▸ ⋯ ▸ lpr

@[simp]

theorem flprep_flip {Hist : List Sequent} {X : Sequent} : flprep (List.map Sequent.flip Hist) X.flip ↔ flprep Hist X

def Tableau.flip {Hist : History} {X : Sequent} : Tableau Hist X → Tableau (List.map Sequent.flip Hist) X.flip

(┛ಠ_ಠ)┛彡┻━┻

Equations

• (Tableau.loc nflprep nbas lt next).flip = Tableau.loc ⋯ ⋯ lt.flip fun (Y : Sequent) (Y_in : Y ∈ endNodesOf lt.flip) => ⋯ ▸ (next Y.flip ⋯).flip
• (Tableau.pdl nflprep bas r next).flip = Tableau.pdl ⋯ ⋯ r.flip next.flip
• (Tableau.lrep lpr).flip = Tableau.lrep lpr.flip

@[simp]

theorem Hist_flip {Hist : List Sequent} : List.map Sequent.flip (List.map Sequent.flip Hist) = Hist

@[simp]

theorem Tableau.flip_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} : tab.flip.flip = ⋯ ▸ ⋯ ▸ tab

def PathIn.flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} : PathIn tab → PathIn tab.flip

Equations

• PathIn.nil.flip = PathIn.nil
• (PathIn.loc Y_in tail).flip = PathIn.loc ⋯ (have this := tail.flip; ⋯.mpr this)
• tail.pdl.flip = tail.flip.pdl

theorem PathIn_helper {HistA : History} {XA : Sequent} {HistB : History} {XB : Sequent} {tabA : Tableau HistA XA} {tabB : Tableau HistB XB} (hHist : HistA = HistB) (hX : XA = XB) : tabA = ⋯ ▸ ⋯ ▸ tabB → PathIn tabA = PathIn tabB

@[simp]

theorem PathIn_type_flip_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} : PathIn tab.flip.flip = PathIn tab

theorem flip_aux_eq_mpr_heq {a b : Sort u} (h : a = b) (x : b) : h.mpr x ≍ x

Eq.mpr is a heterogeneous identity.

theorem flip_aux_Tableau_flip_flip_heq {H : History} {X : Sequent} (t : Tableau H X) : t.flip.flip ≍ t

Flipping a tableau twice gives back (heterogeneously) the original tableau.

theorem flip_aux_LocalTableau_flip_flip_heq {X : Sequent} (lt : LocalTableau X) : lt.flip.flip ≍ lt

Flipping a local tableau twice gives back (heterogeneously) the original one.

theorem flip_aux_PdlRule_flip_flip_heq {X Y : Sequent} (r : PdlRule X Y) : r.flip.flip ≍ r

Flipping a pdl rule twice gives back (heterogeneously) the original one.

theorem endNodesOf_flip_flip {X : Sequent} (lt : LocalTableau X) : endNodesOf lt.flip.flip = endNodesOf lt

End nodes are invariant under flipping a local tableau twice.

theorem PathIn_flip_heq {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} {p1 : PathIn t1} {p2 : PathIn t2} (hH : H1 = H2) (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) : p1.flip ≍ p2.flip

PathIn.flip respects heterogeneous equality of paths.

theorem Tableau_flip_heq {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} (hH : H1 = H2) (hX : X1 = X2) (h : t1 ≍ t2) : t1.flip ≍ t2.flip

Tableau.flip respects heterogeneous equality of tableaux.

theorem PathIn.flip_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : ⋯ ▸ p.flip.flip = p

Flipping a path twice gives back (after casting along PathIn_type_flip_flip) the original path.

def PathIn.unflip {X : Sequent} {tab : Tableau [] X} (p : PathIn tab.flip) : PathIn tab

Undo PathIn.flip: flipping twice is the identity (up to the cast).

Equations

• p.unflip = ⋯ ▸ p.flip

@[simp]

theorem PathIn.flip_unflip {X : Sequent} {tab : Tableau [] X} (p : PathIn tab.flip) : p.unflip.flip = p

theorem edge_loc_shape {Hist : List Sequent} {X Y : Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} {Y_in : Y ∈ endNodesOf lt} {t : PathIn (next Y Y_in)} {q : PathIn (Tableau.loc nrep nbas lt next)} : (PathIn.loc Y_in t) ⋖_ q → ∃ (s : PathIn (next Y Y_in)), q = PathIn.loc Y_in s ∧ t ⋖_ s

A child of a loc path is again a loc path with the same first step.

theorem edge_pdl_shape {Hist : List Sequent} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {nx : Tableau (X :: Hist) Y} {t : PathIn nx} {q : PathIn (Tableau.pdl nrep bas r nx)} : t.pdl ⋖_ q → ∃ (s : PathIn nx), q = s.pdl ∧ t ⋖_ s

A child of a pdl path is again a pdl path.

theorem PathIn.eq_nil_of_length_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} {p : PathIn tab} : p.length = 0 → p = nil

A path of length zero is the empty path.

theorem edge_heq_congr {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} {p1 q1 : PathIn t1} {p2 q2 : PathIn t2} (hH : H1 = H2) (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) (hq : q1 ≍ q2) : p1 ⋖_ q1 ↔ p2 ⋖_ q2

The edge relation only depends on paths up to heterogeneous equality.

theorem PathIn.length_heq_congr {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} {p1 : PathIn t1} {p2 : PathIn t2} (hH : H1 = H2) (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) : p1.length = p2.length

The length of a path only depends on it up to heterogeneous equality.

theorem PathIn.flip_length {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : p.flip.length = p.length

Flipping a path does not change its length.

theorem nil_edge_loc_of_length_zero {Hist : List Sequent} {X Y : Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} {Y_in : Y ∈ endNodesOf lt} {u : PathIn (next Y Y_in)} (hu : u.length = 0) : PathIn.nil ⋖_ (PathIn.loc Y_in u)

Variant of nil_edge_loc_nil where the tail is only known to have length zero.

theorem nil_edge_pdl_of_length_zero {Hist : List Sequent} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {nx : Tableau (X :: Hist) Y} {u : PathIn nx} (hu : u.length = 0) : PathIn.nil ⋖_ u.pdl

Variant of nil_edge_pdl_nil where the tail is only known to have length zero.

theorem edge_flip_of_edge {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p q : PathIn tab) : p ⋖_ q → p.flip ⋖_ q.flip

Flipping a tableau preserves the child relation.

theorem edge_flip {H : History} {X : Sequent} {tab : Tableau H X} {p q : PathIn tab} : p.flip ⋖_ q.flip ↔ p ⋖_ q

Flipping a tableau does not change which nodes are children of which.

theorem tabAt_heq_congr {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} {p1 : PathIn t1} {p2 : PathIn t2} (hH : H1 = H2) (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) : tabAt p1 = tabAt p2

The tableau at a path only depends on it up to heterogeneous equality.

theorem toHistory_heq_congr {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} {p1 : PathIn t1} {p2 : PathIn t2} (hH : H1 = H2) (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) : p1.toHistory = p2.toHistory

The history of a path only depends on it up to heterogeneous equality.

theorem tabAt_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : tabAt p.flip = ⟨List.map Sequent.flip (tabAt p).fst, ⟨(tabAt p).snd.fst.flip, (tabAt p).snd.snd.flip⟩⟩

The tableau at a flipped path is the flip of the tableau at the original path.

theorem PathIn.nodeAt_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} {e : PathIn tab} : nodeAt e.flip = (nodeAt e).flip

The sequent at a flipped path is the flip of the sequent at the original path.

theorem toHistory_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : p.flip.toHistory = List.map Sequent.flip p.toHistory

The history of a flipped path is the flip of the history of the original path.

theorem PathIn.rewind_heq_congr {H1 : History} {X1 : Sequent} {H2 : History} {X2 : Sequent} {t1 : Tableau H1 X1} {t2 : Tableau H2 X2} {p1 : PathIn t1} {p2 : PathIn t2} {k1 : Fin (List.length p1.toHistory + 1)} {k2 : Fin (List.length p2.toHistory + 1)} (hH : H1 = H2) (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) (hk : ↑k1 = ↑k2) : p1.rewind k1 ≍ p2.rewind k2

Rewinding only depends on the path up to heterogeneous equality, and on the index only via its value.

theorem PathIn.flip_rewind {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (k : Fin (List.length p.toHistory + 1)) (k' : Fin (List.length p.flip.toHistory + 1)) : ↑k = ↑k' → (p.rewind k).flip = p.flip.rewind k'

Flipping commutes with rewinding.

theorem tabAt_flip_lrep {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (lpr : LoadedPathRepeat (tabAt p).fst (tabAt p).snd.fst) (h : (tabAt p).snd.snd = Tableau.lrep lpr) : ∃ (lpr' : LoadedPathRepeat (tabAt p.flip).fst (tabAt p.flip).snd.fst), (tabAt p.flip).snd.snd = Tableau.lrep lpr' ∧ ↑↑lpr' = ↑↑lpr

If a path ends in a loaded-path-repeat, then so does the flipped path, with a repeat at the same position in the history.

theorem companion_flip_of_companion {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : p ♥ q → p.flip ♥ q.flip

Flipping a tableau preserves the companion relation.

theorem cEdge_flip_of_cEdge {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : p ◃ q → p.flip ◃ q.flip

Flipping a tableau preserves the cEdge relation ◃.

theorem cReach_flip_of_cReach {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : p ◃* q → p.flip ◃* q.flip

Flipping a tableau preserves reachability via ◃.

theorem cEdgeTrans_flip_of_cEdgeTrans {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : p ◃⁺ q → p.flip ◃⁺ q.flip

Flipping a tableau preserves chains of ◃. (Note the ⁺ instead of *.)

theorem cReach_heq_congr {X1 X2 : Sequent} {t1 : Tableau [] X1} {t2 : Tableau [] X2} {p1 q1 : PathIn t1} {p2 q2 : PathIn t2} (hX : X1 = X2) (ht : t1 ≍ t2) (hp : p1 ≍ p2) (hq : q1 ≍ q2) : p1 ◃* q1 ↔ p2 ◃* q2

Reachability via ◃ only depends on paths up to heterogeneous equality.

theorem cReach_flip {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : p.flip ◃* q.flip ↔ p ◃* q

Flipping a tableau changes neither the child nor the companion relation, hence it also does not change reachability.

theorem cEquiv_flip {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : p.flip ≡ᶜ q.flip ↔ p ≡ᶜ q