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 clusterInterpolationRight.

def PDL.Olf.flip : Olf → Olf

Exchange the side of an optional loaded formula.

Equations

• PDL.Olf.flip = Option.map Sum.swap

@[simp]

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

@[simp]

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

@[simp]

theorem PDL.Olf.flip_none : flip none = none

def PDL.Sequent.flip : Sequent → Sequent

Exchange both sequent components and the side of its loaded formula.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem PDL.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 PDL.basic_flip {X : Sequent} : X.flip.basic ↔ X.basic

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

Reflect a local rule by exchanging its left and right components.

Equations

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

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

def PDL.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 PDL.Sequent.flip_comp_flip : flip ∘ flip = id

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

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

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

Reflect every rule and branch of a local tableau.

Equations

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

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

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

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

theorem PDL.exists_flip_of_endNodesOf {X : Sequent} {ltf : LocalTableau X.flip} {Zf : Sequent} : Zf ∈ endNodesOf ltf → ∃ (Z : Sequent), Zf = Z.flip ∧ Z ∈ endNodesOf ltf.flip

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

Reflect a PDL rule by exchanging the sequent components.

Equations

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

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

@[simp]

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

Flipping sequents is injective.

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

Reflect a loaded-path repeat, preserving its history position.

Equations

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

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

@[simp]

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

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

Exchange the left and right sides throughout a tableau.

Equations

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

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

@[simp]

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

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

Map a tableau path to the corresponding path in the reflected tableau.

Equations

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

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

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

theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.PathIn.flip_unflip {X : Sequent} {tab : Tableau [] X} (p : PathIn tab.flip) : p.unflip.flip = p

theorem PDL.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)} : edge (PathIn.loc Y_in t) q → ∃ (s : PathIn (next Y Y_in)), q = PathIn.loc Y_in s ∧ edge t s

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

theorem PDL.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)} : edge t.pdl q → ∃ (s : PathIn nx), q = s.pdl ∧ edge t s

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

theorem PDL.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 PDL.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) : edge p1 q1 ↔ edge p2 q2

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

theorem PDL.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 PDL.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 PDL.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) : edge PathIn.nil (PathIn.loc Y_in u)

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

theorem PDL.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) : edge PathIn.nil u.pdl

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

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

Flipping a tableau preserves the child relation.

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

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

theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.companion_flip_of_companion {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : companion p q → companion p.flip q.flip

Flipping a tableau preserves the companion relation.

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

Flipping a tableau preserves the cEdge relation ◃.

theorem PDL.cReach_flip_of_cReach {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : Relation.ReflTransGen cEdge p q → Relation.ReflTransGen cEdge p.flip q.flip

Flipping a tableau preserves reachability via ◃.

theorem PDL.cEdgeTrans_flip_of_cEdgeTrans {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : Relation.TransGen cEdge p q → Relation.TransGen cEdge p.flip q.flip

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

theorem PDL.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) : Relation.ReflTransGen cEdge p1 q1 ↔ Relation.ReflTransGen cEdge p2 q2

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

theorem PDL.cReach_flip {X : Sequent} {tab : Tableau [] X} {p q : PathIn tab} : Relation.ReflTransGen cEdge p.flip q.flip ↔ Relation.ReflTransGen cEdge p q

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

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