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

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

@[simp]

theorem Sequent.flip_setEqTo_flip {X Y : Sequent} : X.flip.setEqTo Y.flip ↔ X.setEqTo Y

@[simp]

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

@[simp]

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

theorem nrep_flip {Hist : History} {X : Sequent} (nrep : ¬rep Hist X) : ¬rep (List.map Sequent.flip Hist) X.flip

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

Equations

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

theorem LocalRule.flip_flip {Lcond Rcond : List Formula} {Ocond : Olf} {ress : List 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_map_flip {B : List Sequent} {Y : Sequent} : Y ∈ List.map 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

theorem 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 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_multisetEqTo {X Y : Sequent} : X.flip.multisetEqTo Y.flip ↔ X.multisetEqTo Y

@[simp]

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

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.ext {Hist : History} {X : Sequent} (lprA lprB : LoadedPathRepeat Hist X) : ↑lprA = ↑lprB → lprA = lprB

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

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

(┛ಠ_ಠ)┛彡┻━┻

Equations

• (Tableau.loc nrep nbas lt next).flip = Tableau.loc ⋯ ⋯ lt.flip fun (Y : Sequent) (Y_in : Y ∈ endNodesOf lt.flip) => ⋯ ▸ (next Y.flip ⋯).flip
• (Tableau.pdl nrep 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 PathIn.nodeAt_flip {Hist : History} {X : Sequent} {tab : Tableau Hist X} {e : PathIn tab} : nodeAt e.flip = (nodeAt e).flip

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.