Sequents

Optional loaded formulas (Olfs)

@[reducible, inline]

abbrev PDL.Olf : Type

In nodes we optionally have a negated loaded formula on the left or right.

Equations

• PDL.Olf = Option (PDL.NegLoadFormula ⊕ PDL.NegLoadFormula)

def PDL.Olf.voc : Olf → Vocab

The vocabulary of the optional loaded formula, ignoring its side.

Equations

• PDL.Olf.voc none = ∅
• PDL.Olf.voc (some (Sum.inl nlf)) = nlf.voc
• PDL.Olf.voc (some (Sum.inr nlf)) = nlf.voc

@[instance_reducible]

instance PDL.Option.instHasSubsetOption {α : Type u_1} : HasSubset (Option α)

Equations

• PDL.Option.instHasSubsetOption = { Subset := fun (o1 o2 : Option α) => match o1, o2 with | none, x => True | some val, none => False | some f, some g => f = g }

@[simp]

theorem PDL.Option.some_subseteq {α : Type u_1} {x : α} {O : Option α} : some x ⊆ O ↔ some x = O

@[simp]

theorem PDL.Option.none_subseteq {α : Type u_1} {O : Option α} : none ⊆ O

@[instance_reducible]

instance PDL.Option.instDecidableSubset {α : Type u_1} [DecidableEq α] (o1 o2 : Option α) : Decidable (o1 ⊆ o2)

The subset relation on Option α from Option.instHasSubsetOption is decidable.

Equations

• PDL.Option.instDecidableSubset o1 o2 = Option.casesOn o1 (isTrue trivial) fun (a : α) => Option.casesOn o2 (isFalse ⋯) fun (b : α) => decidable_of_iff (a = b) ⋯

@[instance_reducible]

instance PDL.Option.insHasSdiff {α : Type u_1} [DecidableEq α] : SDiff (Option α)

Instance that is used to say (O : Olf) \ (O' : Olf).

Equations

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

@[simp]

theorem PDL.Option.insHasSdiff_none {α : Type u_1} {o : Option α} [DecidableEq α] : none \ o = none

@[simp]

theorem PDL.Option.insHasSdiff_remove_none_cancel {α : Type u_1} {o : Option α} [DecidableEq α] : o \ none = o

@[simp]

theorem PDL.Option.insHasSdiff_remove_sem_eq_none {α : Type u_1} {x : α} [DecidableEq α] : some x \ some x = none

def PDL.Olf.L : Olf → Finset Formula

The unloaded left formula contributed by an optional loading.

Equations

• PDL.Olf.L none = ∅
• PDL.Olf.L (some (Sum.inl (PDL.NegLoadFormula.neg lf))) = {lf.unload.neg}
• PDL.Olf.L (some (Sum.inr val)) = ∅

@[simp]

theorem PDL.Olf.L_none : L none = ∅

@[simp]

theorem PDL.Olf.L_inr {lf : NegLoadFormula} : L (some (Sum.inr lf)) = ∅

@[simp]

theorem PDL.Olf.L_map_inr {olf : Option NegLoadFormula} : L (Option.map Sum.inr olf) = ∅

@[simp]

theorem PDL.Olf.L_inl {lf : NegLoadFormula} : L (some (Sum.inl lf)) = {lf.1.unload.neg}

theorem PDL.Olf.L_subset_of_subset {O1 O2 : Olf} (h : O1 ⊆ O2) : O1.L ⊆ O2.L

theorem PDL.Olf.L_sdiff_subset {O Ocond : Olf} : (O \ Ocond).L ⊆ O.L

def PDL.Olf.R : Olf → Finset Formula

The unloaded right formula contributed by an optional loading.

Equations

• PDL.Olf.R none = ∅
• PDL.Olf.R (some (Sum.inl val)) = ∅
• PDL.Olf.R (some (Sum.inr (PDL.NegLoadFormula.neg lf))) = {lf.unload.neg}

@[simp]

theorem PDL.Olf.R_none : R none = ∅

@[simp]

theorem PDL.Olf.R_inl {lf : NegLoadFormula} : R (some (Sum.inl lf)) = ∅

@[simp]

theorem PDL.Olf.R_map_inl {olf : Option NegLoadFormula} : R (Option.map Sum.inl olf) = ∅

@[simp]

theorem PDL.Olf.R_inr {lf : NegLoadFormula} : R (some (Sum.inr lf)) = {lf.1.unload.neg}

theorem PDL.Olf.R_subset_of_subset {O1 O2 : Olf} (h : O1 ⊆ O2) : O1.R ⊆ O2.R

theorem PDL.Olf.R_sdiff_subset {O Ocond : Olf} : (O \ Ocond).R ⊆ O.R

def Option.pdlOverwrite {α : Type u_1} : Option α → Option α → Option α

Use the new optional value when present, otherwise retain the old value.

Equations

• x✝.pdlOverwrite none = x✝
• x✝.pdlOverwrite (some x_3) = some x_3

def PDL.Olf.change (oldO Ocond newO : Olf) : Olf

Remove the rule's required loading and install its new loading when present.

Equations

• oldO.change Ocond newO = Option.pdlOverwrite (oldO \ Ocond) newO

@[simp]

theorem PDL.Olf.change_old_none_none {oldO : Olf} : oldO.change none none = oldO

@[simp]

theorem PDL.Olf.change_none_none_new {newO : Olf} : change none none newO = newO

@[simp]

theorem PDL.Olf.change_some {oldO whatever : Olf} {wnlf : NegLoadFormula ⊕ NegLoadFormula} : oldO.change whatever (some wnlf) = some wnlf

@[simp]

theorem PDL.Olf.change_some_some_eq {Onew : Olf} {nχ : NegLoadFormula ⊕ NegLoadFormula} : change (some nχ) (some nχ) Onew = Onew

def PDL.Olf.isNone : Olf → Prop

Whether the optional loading is absent.

Equations

• PDL.Olf.isNone none = True
• PDL.Olf.isNone (some (Sum.inl nlf)) = False
• PDL.Olf.isNone (some (Sum.inr nlf)) = False

def PDL.Olf.isLeft : Olf → Prop

Whether the optional loading belongs to the left component.

Equations

• PDL.Olf.isLeft none = False
• PDL.Olf.isLeft (some (Sum.inl nlf)) = True
• PDL.Olf.isLeft (some (Sum.inr nlf)) = False

def PDL.Olf.isRight : Olf → Prop

Whether the optional loading belongs to the right component.

Equations

• PDL.Olf.isRight none = False
• PDL.Olf.isRight (some (Sum.inl nlf)) = False
• PDL.Olf.isRight (some (Sum.inr nlf)) = True

@[instance_reducible]

instance PDL.instDecidableOlfisNone (o : Olf) : Decidable o.isNone

Equations

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

@[instance_reducible]

instance PDL.instDecidableOlfisLeft (o : Olf) : Decidable o.isLeft

Equations

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

@[instance_reducible]

instance PDL.instDecidableOlfisRight (o : Olf) : Decidable o.isRight

Equations

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

Sequents and their (multi)set quality

@[implicit_reducible]

def PDL.Sequent : Type

A tableau node is labelled with two finite sets of formulas and an Olf. Each formula is placed on the left or right and up to one formula may be loaded.

Equations

• PDL.Sequent = (Finset PDL.Formula × Finset PDL.Formula × PDL.Olf)

@[instance_reducible]

instance PDL.instDecidableEqSequent : DecidableEq Sequent

Equations

• PDL.instDecidableEqSequent = PDL.instDecidableEqSequent._aux_1

@[instance_reducible]

unsafe instance PDL.instReprSequent : Repr Sequent

Equations

• PDL.instReprSequent = { reprPrec := PDL.instReprSequent._aux_1 }

def PDL.Sequent.toFinset : Sequent → Finset Formula

All ordinary formulas of a sequent, including its loading after unloading.

Equations

• PDL.Sequent.toFinset (L, R, O) = L ∪ R ∪ (Option.map (Sum.elim PDL.negUnload PDL.negUnload) O).toFinset

Components and sides of sequents

def PDL.Sequent.L : Sequent → Finset Formula

The ordinary formulas in the left component.

Equations

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

def PDL.Sequent.R : Sequent → Finset Formula

The ordinary formulas in the right component.

Equations

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

def PDL.Sequent.O : Sequent → Olf

The optional loaded formula and its side.

Equations

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

@[simp]

theorem PDL.Sequent.L_eq {L R : Finset Formula} {O : Olf} : Sequent.L (L, R, O) = L

@[simp]

theorem PDL.Sequent.R_eq {L R : Finset Formula} {O : Olf} : Sequent.R (L, R, O) = R

@[simp]

theorem PDL.Sequent.O_eq {L R : Finset Formula} {O : Olf} : Sequent.O (L, R, O) = O

def PDL.Sequent.left (X : Sequent) : Finset Formula

The left component including any left loading after unloading.

Equations

• X.left = X.L ∪ X.O.L

def PDL.Sequent.right (X : Sequent) : Finset Formula

The right component including any right loading after unloading.

Equations

• X.right = X.R ∪ X.O.R

@[simp]

theorem PDL.Sequent.left_eq {L R : Finset Formula} {O : Olf} : left (L, R, O) = L ∪ O.L

@[simp]

theorem PDL.Sequent.right_eq {L R : Finset Formula} {O : Olf} : right (L, R, O) = R ∪ O.R

(Joint) vocabulary of sequents

def PDL.onlfvoc : Option NegLoadFormula → Vocab

Like Olf.voc but without the ⊕ inside.

Equations

• PDL.onlfvoc none = ∅
• PDL.onlfvoc (some nlf) = nlf.voc

def PDL.lfovoc (L : List (List Formula × Option NegLoadFormula)) : Vocab

The combined vocabulary of formula lists and optional loaded formulas.

Equations

• PDL.lfovoc L = L.toFinset.sup fun (x : List PDL.Formula × Option PDL.NegLoadFormula) => match x with | (fs, o) => fs.pdlFvoc ∪ PDL.onlfvoc o

def PDL.lfovocFin (L : Finset (Finset Formula × Option NegLoadFormula)) : Vocab

Finset version of lfovoc.

Equations

• PDL.lfovocFin L = L.sup fun (x : Finset PDL.Formula × Option PDL.NegLoadFormula) => match x with | (fs, o) => fs.pdlFvoc ∪ PDL.onlfvoc o

def PDL.jvoc (X : Sequent) : Vocab

The joint vocabulary occurring on both the left and the right side.

Equations

• PDL.jvoc X = X.left.pdlFvoc ∩ X.right.pdlFvoc

theorem PDL.jvoc_sub_of_voc_sub {Y X : Sequent} (hl : Y.left.pdlFvoc ⊆ X.left.pdlFvoc) (hr : Y.right.pdlFvoc ⊆ X.right.pdlFvoc) : jvoc Y ⊆ jvoc X

Formulas as elements of sequents

@[instance_reducible, instance 10000]

instance PDL.instMembershipFormulaSequent : Membership Formula Sequent

Equations

• PDL.instMembershipFormulaSequent = { mem := fun (X : PDL.Sequent) (φ : PDL.Formula) => φ ∈ X.L ∨ φ ∈ X.R }

@[simp]

theorem PDL.Sequent.mem_def {φ : Formula} {X : Sequent} : φ ∈ X ↔ φ ∈ X.L ∨ φ ∈ X.R

@[instance_reducible]

instance PDL.instDecidableMemFormulaSequent {φ : Formula} {X : Sequent} : Decidable (φ ∈ X)

Equations

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

@[instance_reducible]

instance PDL.instFintypeSubtypeMemSequent {X : Sequent} : Fintype { x : Formula // x ∈ X }

Equations

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

def PDL.NegLoadFormula.memSequent (X : Sequent) (nlf : NegLoadFormula) : Prop

Whether the specified loaded formula is the loading on either side of a sequent.

Equations

• PDL.NegLoadFormula.memSequent X nlf = (X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf))

@[instance_reducible]

instance PDL.instDecidableMemSequentMkFinsetFormulaProdOlf {L R : Finset Formula} {O : Olf} {nlf : NegLoadFormula} : Decidable (NegLoadFormula.memSequent (L, R, O) nlf)

Equations

• PDL.instDecidableMemSequentMkFinsetFormulaProdOlf = if h : O = some (Sum.inl nlf) then isTrue ⋯ else if h2 : O = some (Sum.inr nlf) then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PDL.instMembershipNegLoadFormulaSequent : Membership NegLoadFormula Sequent

Equations

• PDL.instMembershipNegLoadFormulaSequent = { mem := PDL.NegLoadFormula.memSequent }

def PDL.AnyNegFormula.memSequent (X : Sequent) (anf : AnyNegFormula) : Prop

Membership of a negated ordinary or loaded formula in a sequent.

Equations

• PDL.AnyNegFormula.memSequent x✝ (PDL.AnyNegFormula.neg (PDL.AnyFormula.normal φ)) = (φ.neg ∈ x✝)
• PDL.AnyNegFormula.memSequent x✝ (PDL.AnyNegFormula.neg (PDL.AnyFormula.loaded χ)) = (PDL.NegLoadFormula.neg χ ∈ x✝)

@[instance_reducible]

instance PDL.instMembershipAnyNegFormulaSequent : Membership AnyNegFormula Sequent

Equations

• PDL.instMembershipAnyNegFormulaSequent = { mem := PDL.AnyNegFormula.memSequent }

Closed, basic, loaded and free sequents

def PDL.Sequent.closed (X : Sequent) : Prop

A sequent is closed iff it contains ⊥ or contains a formula and its negation.

Equations

• X.closed = (⊥ ∈ X ∨ ∃ f ∈ X, f.neg ∈ X)

def PDL.Sequent.basic : Sequent → Prop

A sequent is basic iff it only contains basic formulas and is not closed.

Equations

• x✝.basic = ((∀ f ∈ x✝.toFinset, f.basic = true) ∧ ¬x✝.closed)

@[instance_reducible]

instance PDL.Fintype.decidableExistsConjFintype {α : Type u_1} {p q : α → Prop} [DecidablePred q] [Fintype (Subtype p)] : Decidable (∃ (a : α), p a ∧ q a)

A variant of Fintype.decidableExistsFintype, used by instDecidableClosed.

Equations

• PDL.Fintype.decidableExistsConjFintype = if h : ∃ (x : Subtype p), q ↑x then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PDL.Sequent.instDecidableClosed {X : Sequent} : Decidable X.closed

Equations

• PDL.Sequent.instDecidableClosed = id (if h : ⊥ ∈ X then isTrue ⋯ else if h_1 : ∃ f ∈ X, f.neg ∈ X then isTrue ⋯ else isFalse ⋯)

@[instance_reducible]

instance PDL.instDecidableBasic {X : Sequent} : Decidable X.basic

Equations

• PDL.instDecidableBasic = if h : X.closed then isFalse ⋯ else id (⋯.mpr (if h : ∃ f ∈ X.toFinset, f.basic ≠ true then isFalse ⋯ else isTrue ⋯))

def PDL.Sequent.isLoaded : Sequent → Prop

Whether a sequent carries a loaded formula.

Equations

• PDL.Sequent.isLoaded (fst, fst_1, none) = False
• PDL.Sequent.isLoaded (fst, fst_1, some val) = True

theorem PDL.Sequent.isRight_of_not_isLeft_isLoaded {X : Sequent} (h1 : ¬X.2.2.isLeft) (h2 : X.isLoaded) : X.2.2.isRight

A loaded sequent that is not loaded on the left is loaded on the right.

@[instance_reducible]

instance PDL.instDecidableSequentisLoaded (X : Sequent) : Decidable X.isLoaded

Equations

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

def PDL.Sequent.isFree (Γ : Sequent) : Prop

Whether a sequent has no loaded formula.

Equations

• Γ.isFree = ¬Γ.isLoaded

@[instance_reducible]

instance PDL.instDecidableSequentisFree (X : Sequent) : Decidable X.isFree

Equations

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

@[simp]

theorem PDL.Sequent.none_isFree (L R : Finset Formula) : isFree (L, R, none)

@[simp]

theorem PDL.Sequent.some_not_isFree (L R : Finset Formula) (olf : NegLoadFormula ⊕ NegLoadFormula) : ¬isFree (L, R, some olf)

Semantics of sequents

@[instance_reducible]

instance PDL.modelCanSemImplySequent {W : Type} : vDash (KripkeModel W × W) Sequent

Equations

• PDL.modelCanSemImplySequent = { SemImplies := fun (x : PDL.KripkeModel W × W) (X : PDL.Sequent) => match x with | (M, w) => ∀ f ∈ X.toFinset, PDL.evaluate M w f }

@[instance_reducible]

instance PDL.instSequentHasSat : HasSat Sequent

Equations

• PDL.instSequentHasSat = { satisfiable := fun (Δ : PDL.Sequent) => ∃ (W : Type) (M : PDL.KripkeModel W) (w : W), PDL.vDash.SemImplies (M, w) Δ }

theorem PDL.tautImp_iff_SequentUnsat {φ ψ : Formula} {X : Sequent} : X = ({φ}, {ψ.neg}, none) → (tautology (φ.and ψ.neg).neg ↔ ¬HasSat.satisfiable X)

theorem PDL.vDash_setEqTo_iff {W : Type} {X Y : Sequent} (h : X = Y) (M : KripkeModel W) (w : W) : vDash.SemImplies (M, w) X ↔ vDash.SemImplies (M, w) Y

theorem PDL.Sequent.satisfiable_top_cons_right {X : Sequent} (h_left_nil : X.left = ∅) (X_unsat : ¬HasSat.satisfiable X) : ¬HasSat.satisfiable ({⊤} ∪ X.right)

Removing loaded formulas from sequents

def PDL.Sequent.without (LRO : Sequent) (naf : AnyNegFormula) : Sequent

Remove a negated formula from the ordinary components or from the optional loading.

Equations

• PDL.Sequent.without (L, R, O) (PDL.AnyNegFormula.neg (PDL.AnyFormula.normal f)) = (L \ {f.neg}, R \ {f.neg}, O)
• PDL.Sequent.without (L, R, O) (PDL.AnyNegFormula.neg (PDL.AnyFormula.loaded lf)) = if PDL.NegLoadFormula.memSequent (L, R, O) (PDL.NegLoadFormula.neg lf) then (L, R, none) else (L, R, O)

@[simp]

theorem PDL.Sequent.without_normal_isFree_iff_isFree {φ : Formula} (LRO : Sequent) : (LRO.without (AnyNegFormula.neg (AnyFormula.normal φ))).isFree ↔ LRO.isFree

@[simp]

theorem PDL.Sequent.isFree_then_without_isFree (LRO : Sequent) : LRO.isFree → ∀ (anf : AnyNegFormula), (LRO.without anf).isFree

theorem PDL.Sequent.without_loadBoxes_isFree_of_eq_inl {d : Program} {αs : List Program} {L R : Finset Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.boxes (d :: δs) χ)))) (AnyNegFormula.neg (AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree

theorem PDL.Sequent.without_loadBoxes_isFree_of_eq_inr {d : Program} {αs : List Program} {L R : Finset Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.boxes (d :: δs) χ)))) (AnyNegFormula.neg (AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree

theorem PDL.Sequent.without_loadMulti_isFree_of_splitLast_cons_inl {d : Program} {δ_β : List Program × Program} {L R : Finset Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inl (NegLoadFormula.neg (loadMulti δ_β.1 δ_β.2 φ)))) (AnyNegFormula.neg (AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree

theorem PDL.Sequent.without_loadMulti_isFree_of_splitLast_cons_inr {d : Program} {δ_β : List Program × Program} {L R : Finset Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inr (NegLoadFormula.neg (loadMulti δ_β.1 δ_β.2 φ)))) (AnyNegFormula.neg (AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree

inductive PDL.Side : Type

The left and right components of a sequent.

• LL : Side
• RR : Side

def PDL.sideOf {α : Type u_1} : α ⊕ α → Side

The component indicated by a sum constructor.

Equations

• PDL.sideOf (Sum.inl val) = PDL.Side.LL
• PDL.sideOf (Sum.inr val) = PDL.Side.RR

def PDL.AnyNegFormula.inSide (anf : AnyNegFormula) : Side → (X : Sequent) → Prop

Membership of a negated formula in the specified sequent component.

Equations

• (PDL.AnyNegFormula.neg (PDL.AnyFormula.normal φ)).inSide PDL.Side.LL (L, fst, snd) = (φ.neg ∈ L)
• (PDL.AnyNegFormula.neg (PDL.AnyFormula.normal φ)).inSide PDL.Side.RR (fst, R, snd) = (φ.neg ∈ R)
• (PDL.AnyNegFormula.neg (PDL.AnyFormula.loaded χ)).inSide PDL.Side.LL (fst, fst_1, O) = (O = some (Sum.inl (PDL.NegLoadFormula.neg χ)))
• (PDL.AnyNegFormula.neg (PDL.AnyFormula.loaded χ)).inSide PDL.Side.RR (fst, fst_1, O) = (O = some (Sum.inr (PDL.NegLoadFormula.neg χ)))

theorem PDL.LoadFormula.in_side_of_lf_inl {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inl (NegLoadFormula.neg lf))) : (AnyNegFormula.neg (AnyFormula.loaded lf)).inSide Side.LL X

theorem PDL.LoadFormula.in_side_of_lf_inr {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inr (NegLoadFormula.neg lf))) : (AnyNegFormula.neg (AnyFormula.loaded lf)).inSide Side.RR X

theorem PDL.Sequent.isLoaded_of_negAnyFormula_loaded {α : Program} {ξ : AnyFormula} {side : Side} {X : Sequent} (negLoad_in : (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α ξ))).inSide side X) : X.isLoaded

theorem PDL.Sequent.without_loaded_in_side_isFree (LRO : Sequent) (ξ : LoadFormula) (side : Side) : (AnyNegFormula.neg (AnyFormula.loaded ξ)).inSide side LRO → (LRO.without (AnyNegFormula.neg (AnyFormula.loaded ξ))).isFree

Whatever formulas

A type to describe all formulas that can occur in a sequent, without losing information about whether they are loaded or not.

inductive PDL.WhateverFormula : Type

Unfortunately our AnyFormula type does not include negated loaded formulas, so this is yet another type to describe "whatever formula" can be in a sequent, without losing information.

• any : AnyFormula → WhateverFormula
• negLoad : NegLoadFormula → WhateverFormula

def PDL.instReprWhateverFormula.repr : WhateverFormula → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PDL.instReprWhateverFormula : Repr WhateverFormula

Equations

• PDL.instReprWhateverFormula = { reprPrec := PDL.instReprWhateverFormula.repr }

@[instance_reducible]

instance PDL.instDecidableEqWhateverFormula : DecidableEq WhateverFormula

Equations

• PDL.instDecidableEqWhateverFormula = PDL.instDecidableEqWhateverFormula.decEq

def PDL.instDecidableEqWhateverFormula.decEq (x✝ x✝¹ : WhateverFormula) : Decidable (x✝ = x✝¹)

Equations

• PDL.instDecidableEqWhateverFormula.decEq (PDL.WhateverFormula.any a) (PDL.WhateverFormula.any b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PDL.instDecidableEqWhateverFormula.decEq (PDL.WhateverFormula.any a) (PDL.WhateverFormula.negLoad a_1) = isFalse ⋯
• PDL.instDecidableEqWhateverFormula.decEq (PDL.WhateverFormula.negLoad a) (PDL.WhateverFormula.any a_1) = isFalse ⋯
• PDL.instDecidableEqWhateverFormula.decEq (PDL.WhateverFormula.negLoad a) (PDL.WhateverFormula.negLoad b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PDL.instCoeFormulaWhateverFormula : Coe Formula WhateverFormula

Equations

• PDL.instCoeFormulaWhateverFormula = { coe := PDL.WhateverFormula.any ∘ PDL.AnyFormula.normal }

@[instance_reducible]

instance PDL.instCoeLoadFormulaWhateverFormula : Coe LoadFormula WhateverFormula

Equations

• PDL.instCoeLoadFormulaWhateverFormula = { coe := PDL.WhateverFormula.any ∘ PDL.AnyFormula.loaded }

@[instance_reducible]

instance PDL.instCoeNegLoadFormulaWhateverFormula : Coe NegLoadFormula WhateverFormula

Equations

• PDL.instCoeNegLoadFormulaWhateverFormula = { coe := PDL.WhateverFormula.negLoad }

def PDL.Olf.wForms : Olf → Finset WhateverFormula

The optional loading viewed as a finset of tagged formulas.

Equations

• PDL.Olf.wForms none = ∅
• PDL.Olf.wForms (some (Sum.inl nlf)) = {PDL.WhateverFormula.negLoad nlf}
• PDL.Olf.wForms (some (Sum.inr nlf)) = {PDL.WhateverFormula.negLoad nlf}

def PDL.Sequent.wForms : Sequent → Finset WhateverFormula

All ordinary and loaded formulas of a sequent, retaining their tags.

Equations

• PDL.Sequent.wForms (L, R, O) = Finset.image Coe.coe L ∪ Finset.image Coe.coe R ∪ O.wForms

theorem PDL.Sequent.mem_toFinset_iff (φ : Formula) (X : Sequent) : φ ∈ X.toFinset ↔ WhateverFormula.any (AnyFormula.normal φ) ∈ X.wForms ∨ (∃ (χ : LoadFormula), χ.unload = φ ∧ WhateverFormula.any (AnyFormula.loaded χ) ∈ X.wForms) ∨ ∃ (ψ : NegLoadFormula), negUnload ψ = φ ∧ WhateverFormula.negLoad ψ ∈ X.wForms

theorem PDL.Sequent.mem_wForms_normal_iff {ψ : Formula} {L R : Finset Formula} {O : Olf} : (WhateverFormula.any ∘ AnyFormula.normal) ψ ∈ wForms (L, R, O) ↔ ψ ∈ L ∨ ψ ∈ R

A normal formula is in X.wForms iff it is on the left or on the right of X. (Note that the Olf part of X only contributes negated loaded formulas.)

theorem PDL.Sequent.isAtomic_of_basic_of_negBox_mem_wForms {X : Sequent} {α : Program} {φ : Formula} (bas : X.basic) (h : (WhateverFormula.any ∘ AnyFormula.normal) (Formula.box α φ).neg ∈ X.wForms) : α.isAtomic

In a basic sequent all free diamonds are atomic.

theorem PDL.Sequent.mem_wForms_negLoad_iff {nlf : NegLoadFormula} {L R : Finset Formula} {O : Olf} : WhateverFormula.negLoad nlf ∈ wForms (L, R, O) ↔ O = some (Sum.inl nlf) ∨ O = some (Sum.inr nlf)

A negated loaded formula is in X.wForms iff it is the loaded formula of X.

theorem PDL.Sequent.isAtomic_of_basic_of_negLoad_mem_wForms {X : Sequent} {α : Program} {ξ : AnyFormula} (bas : X.basic) (h : WhateverFormula.negLoad (NegLoadFormula.neg (LoadFormula.box α ξ)) ∈ X.wForms) : α.isAtomic

In a basic sequent all loaded diamonds are atomic.

Sorting Finsets of Sequents

Lexicographic orders on lists and pairs

NOTE: The following two definitions and their properties are general, i.e. not about PDL at all. These could be moved to a separate file (or even might be in newer versions of Mathlib?).

def PDL.listLex {α : Type} (le : α → α → Prop) : List α → List α → Prop

Lexicographic extension of a relation le to lists: shorter lists come first, and lists of the same shape are compared element-wise from left to right.

Equations

• PDL.listLex le [] x✝ = True
• PDL.listLex le (head :: tail) [] = False
• PDL.listLex le (a :: as) (b :: bs) = (le a b ∧ (a = b → PDL.listLex le as bs))

@[instance_reducible]

instance PDL.listLex.instDecidableRel {α : Type} [DecidableEq α] (le : α → α → Prop) [DecidableRel le] : DecidableRel (listLex le)

Equations

• PDL.listLex.instDecidableRel le [] x✝ = isTrue trivial
• PDL.listLex.instDecidableRel le (head :: tail) [] = isFalse not_false
• PDL.listLex.instDecidableRel le (a :: as) (b :: bs) = inferInstance

theorem PDL.listLex_refl {α : Type} {le : α → α → Prop} (hrefl : ∀ (a : α), le a a) (as : List α) : listLex le as as

theorem PDL.listLex_antisymm {α : Type} {le : α → α → Prop} (hanti : ∀ (a b : α), le a b → le b a → a = b) (as bs : List α) : listLex le as bs → listLex le bs as → as = bs

theorem PDL.listLex_trans {α : Type} {le : α → α → Prop} (hanti : ∀ (a b : α), le a b → le b a → a = b) (htrans : ∀ (a b c : α), le a b → le b c → le a c) (as bs cs : List α) : listLex le as bs → listLex le bs cs → listLex le as cs

theorem PDL.listLex_total {α : Type} {le : α → α → Prop} (hrefl : ∀ (a : α), le a a) (htotal : ∀ (a b : α), le a b ∨ le b a) (as bs : List α) : listLex le as bs ∨ listLex le bs as

def PDL.prodLex {α β : Type} (le1 : α → α → Prop) (le2 : β → β → Prop) : α × β → α × β → Prop

Lexicographic combination of two relations on a product type.

Equations

• PDL.prodLex le1 le2 (a, b) (a', b') = (le1 a a' ∧ (a = a' → le2 b b'))

@[instance_reducible]

instance PDL.prodLex.instDecidableRel {α β : Type} [DecidableEq α] (le1 : α → α → Prop) (le2 : β → β → Prop) [DecidableRel le1] [DecidableRel le2] : DecidableRel (prodLex le1 le2)

Equations

• PDL.prodLex.instDecidableRel le1 le2 (a, b) (a', b') = inferInstance

theorem PDL.prodLex_refl {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (h1 : ∀ (a : α), le1 a a) (h2 : ∀ (b : β), le2 b b) (x : α × β) : prodLex le1 le2 x x

theorem PDL.prodLex_antisymm {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (h1 : ∀ (a a' : α), le1 a a' → le1 a' a → a = a') (h2 : ∀ (b b' : β), le2 b b' → le2 b' b → b = b') (x y : α × β) : prodLex le1 le2 x y → prodLex le1 le2 y x → x = y

theorem PDL.prodLex_trans {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (hanti1 : ∀ (a a' : α), le1 a a' → le1 a' a → a = a') (htrans1 : ∀ (a a' a'' : α), le1 a a' → le1 a' a'' → le1 a a'') (htrans2 : ∀ (b b' b'' : β), le2 b b' → le2 b' b'' → le2 b b'') (x y z : α × β) : prodLex le1 le2 x y → prodLex le1 le2 y z → prodLex le1 le2 x z

theorem PDL.prodLex_total {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (hrefl1 : ∀ (a : α), le1 a a) (htotal1 : ∀ (a a' : α), le1 a a' ∨ le1 a' a) (htotal2 : ∀ (b b' : β), le2 b b' ∨ le2 b' b) (x y : α × β) : prodLex le1 le2 x y ∨ prodLex le1 le2 y x

An order on loaded formulas, via a key

def PDL.LoadFormula.key : LoadFormula → List Program × Formula

Every loaded formula is a non-empty sequence of loading boxes followed by a normal formula. The key of a loaded formula records exactly this data, and hence determines it uniquely. NOTE: This could be moved to Pdl/Syntax.lean.

Equations

• (PDL.LoadFormula.box α (PDL.AnyFormula.normal φ)).key = ([α], φ)
• (PDL.LoadFormula.box α (PDL.AnyFormula.loaded χ)).key = (α :: χ.key.1, χ.key.2)

def PDL.loadFormulaOfKey : List Program → Formula → LoadFormula

Inverse of LoadFormula.key, see LoadFormula.ofKey_key. (The value for the empty list of programs is arbitrary.) NOTE: This could be moved to Pdl/Syntax.lean.

Equations

• PDL.loadFormulaOfKey [] x✝ = PDL.LoadFormula.box (PDL.Program.test x✝) (PDL.AnyFormula.normal x✝)
• PDL.loadFormulaOfKey [α] x✝ = PDL.LoadFormula.box α (PDL.AnyFormula.normal x✝)
• PDL.loadFormulaOfKey (α :: β :: δ) x✝ = PDL.LoadFormula.box α (PDL.AnyFormula.loaded (PDL.loadFormulaOfKey (β :: δ) x✝))

theorem PDL.LoadFormula.ofKey_key (χ : LoadFormula) : loadFormulaOfKey χ.key.1 χ.key.2 = χ

The key of a loaded formula determines it.

theorem PDL.LoadFormula.key_injective {χ χ' : LoadFormula} (h : χ.key = χ'.key) : χ = χ'

An order on sequents, via a key

def PDL.Olf.key : Olf → ℕ × List Program × Formula

Key of an Olf: which side (if any) is loaded, together with the key of the loaded formula.

Equations

• PDL.Olf.key none = (0, [], PDL.Formula.bottom)
• PDL.Olf.key (some (Sum.inl (PDL.NegLoadFormula.neg χ))) = (1, χ.key)
• PDL.Olf.key (some (Sum.inr (PDL.NegLoadFormula.neg χ))) = (2, χ.key)

theorem PDL.Olf.key_injective {O O' : Olf} : O.key = O'.key → O = O'

def PDL.Sequent.key (X : Sequent) : List Formula × List Formula × ℕ × List Program × Formula

Key of a sequent: the sorted lists of the left and right side, and the key of the Olf.

Equations

• X.key = (X.L.pdlSort, X.R.pdlSort, X.O.key)

theorem PDL.Finset.pdlSort_injective {X Y : Finset Formula} (h : X.pdlSort = Y.pdlSort) : X = Y

Finsets of formulas with the same pdlSort are equal. NOTE: This could be moved to Pdl/Syntax.lean.

theorem PDL.Sequent.key_injective {X Y : Sequent} (h : X.key = Y.key) : X = Y

def PDL.olfKeyLe : ℕ × List Program × Formula → ℕ × List Program × Formula → Prop

Order used to compare the keys of Olfs.

Equations

• PDL.olfKeyLe = PDL.prodLex (fun (n m : ℕ) => n ≤ m) (PDL.prodLex (PDL.listLex PDL.Program.le) PDL.Formula.le)

@[instance_reducible]

instance PDL.instDecidableRelProdNatListProgramFormulaOlfKeyLe : DecidableRel olfKeyLe

Equations

• PDL.instDecidableRelProdNatListProgramFormulaOlfKeyLe = id inferInstance

theorem PDL.olfKeyLe_refl (x : ℕ × List Program × Formula) : olfKeyLe x x

theorem PDL.olfKeyLe_antisymm (x y : ℕ × List Program × Formula) (h1 : olfKeyLe x y) (h2 : olfKeyLe y x) : x = y

theorem PDL.olfKeyLe_trans (x y z : ℕ × List Program × Formula) (h1 : olfKeyLe x y) (h2 : olfKeyLe y z) : olfKeyLe x z

theorem PDL.olfKeyLe_total (x y : ℕ × List Program × Formula) : olfKeyLe x y ∨ olfKeyLe y x

def PDL.seqKeyLe : List Formula × List Formula × ℕ × List Program × Formula → List Formula × List Formula × ℕ × List Program × Formula → Prop

Order used to compare the keys of sequents.

Equations

• PDL.seqKeyLe = PDL.prodLex (PDL.listLex PDL.Formula.le) (PDL.prodLex (PDL.listLex PDL.Formula.le) PDL.olfKeyLe)

@[instance_reducible]

instance PDL.instDecidableRelProdListFormulaNatProgramSeqKeyLe : DecidableRel seqKeyLe

Equations

• PDL.instDecidableRelProdListFormulaNatProgramSeqKeyLe = id inferInstance

def PDL.Sequent.le (X Y : Sequent) : Prop

A linear order on sequents, used to define Finset.pdlSeqSort.

Equations

• X.le Y = PDL.seqKeyLe X.key Y.key

@[instance_reducible]

instance PDL.Sequent.instDecidableRelLe : DecidableRel le

Equations

• X.instDecidableRelLe Y = id inferInstance

instance PDL.Sequent.instIsTransLe : IsTrans Sequent le

instance PDL.Sequent.instAntisymmLe : Std.Antisymm le

instance PDL.Sequent.instTotalLe : Std.Total le

def Finset.pdlSeqSort : Finset PDL.Sequent → List PDL.Sequent

Sort a finite set of sequents into a list, using Sequent.le.

Equations

• A.pdlSeqSort = A.sort PDL.Sequent.le

@[simp]

theorem PDL.Finset.mem_seqSort {X : Sequent} (A : Finset Sequent) : X ∈ A.pdlSeqSort ↔ X ∈ A

theorem PDL.Finset.seqSort_nodup (A : Finset Sequent) : A.pdlSeqSort.Nodup

@[simp]

theorem PDL.Finset.length_seqSort (A : Finset Sequent) : A.pdlSeqSort.length = A.card

@[simp]

theorem PDL.Finset.seqSort_eq_nil_iff {A : Finset Sequent} : A.pdlSeqSort = [] ↔ A = ∅