Documentation

def PDL.Program.isAtomic :

Program → Prop

Whether a program is an atomic action.

Equations

(PDL.Program.atom_prog a).isAtomic = (true = true)
x✝.isAtomic = (false = true)

Instances For

theorem PDL.Formula.neq_neg_self (φ : Formula) :

φ ≠ φ.neg

theorem PDL.Program.isAtomic_iff {α : Program} :

α.isAtomic ↔ ∃ (a : ℕ), α = atom_prog a

def PDL.Program.isStar :

Program → Prop

Whether a program has an outer Kleene-star constructor.

Equations

a.star.isStar = (true = true)
x✝.isStar = (false = true)

Instances For

DecidablePred Program.isStar

@[instance_reducible]

instance PDL.instDecidablePredProgramIsStar :

Equations

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

theorem PDL.Program.isStar_iff {α : Program} :

α.isStar ↔ ∃ (β : Program), α = β.star

Tools for Box Formulas #

@[simp]

theorem PDL.Formula.boxes_nil {φ : Formula} :

boxes [] φ = φ

@[simp]

theorem PDL.Formula.boxes_cons {β : Program} {δ : List Program} {φ : Formula} :

boxes (β :: δ) φ = box β (boxes δ φ)

@[simp]

theorem PDL.Formula.boxes_injective {αs : List Program} {φ ψ : Formula} :

boxes αs φ = boxes αs ψ ↔ φ = ψ

theorem PDL.boxes_last {δ : List Program} {α : Program} {φ : Formula} :

Formula.boxes (δ ++ [α]) φ = Formula.boxes δ (Formula.box α φ)

theorem PDL.boxes_append {as bs : List Program} {P : Formula} :

Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.boxes bs P)

def PDL.boxesOf :

Formula → List Program × Formula

Separate a formula's leading boxes from its remaining formula.

Equations

PDL.boxesOf (PDL.Formula.box prog nextf) = match PDL.boxesOf nextf with | (rest, endf) => (prog :: rest, endf)
PDL.boxesOf x✝ = ([], x✝)

Instances For

theorem PDL.def_of_boxesOf_def {φ : Formula} {γ : List Program} {ψ : Formula} (h : boxesOf φ = (γ, ψ)) :

φ = Formula.boxes γ ψ

def PDL.Formula.isBox :

Formula → Prop

Whether a formula has an outer box constructor.

Equations

(PDL.Formula.box prog nextf).isBox = True
x✝.isBox = False

Instances For

theorem PDL.boxesOf_def_of_def_of_nonBox {φ : Formula} {γ : List Program} {ψ : Formula} (h : φ = Formula.boxes γ ψ) (nonBox : ¬ψ.isBox) :

boxesOf φ = (γ, ψ)

@[simp]

theorem PDL.boxesOf_output_not_isBox {φ : Formula} :

¬(boxesOf φ).2.isBox

theorem PDL.nonBox_of_boxesOf_def {φ : Formula} {L : List Program} {ψ : Formula} (bdef : boxesOf φ = (L, ψ)) :

¬ψ.isBox

theorem PDL.boxesOf_nonBox {φ : Formula} (notBox : ¬φ.isBox) :

boxesOf φ = ([], φ)

theorem PDL.defs_of_boxesOf_last_of_nonBox {φ : Formula} (notBox : ¬φ.isBox) (δs : List Program) (α : Program) :

boxesOf (Formula.boxes δs (Formula.box α φ)) = (δs ++ [α], φ)

If φ is not a box then we know the result of boxesOf (⌈⌈δs⌉⌉⌈α⌉φ). A more general version without α should also hold.

theorem PDL.Formula.boxes_cons_neq_self (φ : Formula) (β : Program) (δ : List Program) :

box β (boxes δ φ) ≠ φ

theorem PDL.Formula.boxesOf_boxes_prefix (αs : List Program) (φ : Formula) :

αs <+: (boxesOf (boxes αs φ)).1

Loaded Formulas #

Loaded formulas consist of a non-empty sequence of loading boxes, and a normal formula. For loading boxes we write ⌊α⌋ instead of ⌈α⌉.

inductive PDL.AnyFormula :

An ordinary formula or a formula with a distinguished loaded modal path.

normal : Formula → AnyFormula
loaded : LoadFormula → AnyFormula

Instances For

@[instance_reducible]

instance PDL.instReprAnyFormula :

Repr AnyFormula

Equations

PDL.instReprAnyFormula = { reprPrec := PDL.instReprAnyFormula.repr_1 }

partial def PDL.instReprLoadFormula.repr_1 :

AnyFormula → ℕ → Std.Format

@[instance_reducible]

instance PDL.instReprLoadFormula :

Repr LoadFormula

Equations

PDL.instReprLoadFormula = { reprPrec := PDL.instReprLoadFormula.repr_2 }

partial def PDL.instReprLoadFormula.repr_2 :

LoadFormula → ℕ → Std.Format

partial def PDL.instReprAnyFormula.repr_2 :

LoadFormula → ℕ → Std.Format

partial def PDL.instReprAnyFormula.repr_1 :

AnyFormula → ℕ → Std.Format

def PDL.instDecidableEqLoadFormula.decEq_1 (x✝ x✝¹ : AnyFormula) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
PDL.instDecidableEqLoadFormula.decEq_1 (PDL.AnyFormula.normal a) (PDL.AnyFormula.normal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
PDL.instDecidableEqLoadFormula.decEq_1 (PDL.AnyFormula.normal a) (PDL.AnyFormula.loaded a_1) = isFalse ⋯
PDL.instDecidableEqLoadFormula.decEq_1 (PDL.AnyFormula.loaded a) (PDL.AnyFormula.normal a_1) = isFalse ⋯

Instances For

def PDL.instDecidableEqAnyFormula.decEq_1 (x✝ x✝¹ : AnyFormula) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
PDL.instDecidableEqAnyFormula.decEq_1 (PDL.AnyFormula.normal a) (PDL.AnyFormula.normal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
PDL.instDecidableEqAnyFormula.decEq_1 (PDL.AnyFormula.normal a) (PDL.AnyFormula.loaded a_1) = isFalse ⋯
PDL.instDecidableEqAnyFormula.decEq_1 (PDL.AnyFormula.loaded a) (PDL.AnyFormula.normal a_1) = isFalse ⋯

Instances For

@[instance_reducible]

instance PDL.instDecidableEqAnyFormula :

DecidableEq AnyFormula

Equations

PDL.instDecidableEqAnyFormula = PDL.instDecidableEqAnyFormula.decEq_1

def PDL.instDecidableEqAnyFormula.decEq_2 (x✝ x✝¹ : LoadFormula) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def PDL.instDecidableEqLoadFormula.decEq_2 (x✝ x✝¹ : LoadFormula) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance PDL.instDecidableEqLoadFormula :

DecidableEq LoadFormula

Equations

PDL.instDecidableEqLoadFormula = PDL.instDecidableEqLoadFormula.decEq_2

inductive PDL.LoadFormula :

A box whose continuation may itself carry a loaded path.

box : Program → AnyFormula → LoadFormula

Instances For

@[instance_reducible]

instance PDL.instCoeFormulaAnyFormula :

Coe Formula AnyFormula

Equations

PDL.instCoeFormulaAnyFormula = { coe := PDL.AnyFormula.normal }

Coe LoadFormula AnyFormula

@[instance_reducible]

instance PDL.instCoeLoadFormulaAnyFormula :

Equations

PDL.instCoeLoadFormulaAnyFormula = { coe := PDL.AnyFormula.loaded }

inductive PDL.AnyNegFormula :

Negation of an ordinary or loaded formula.

neg : AnyFormula → AnyNegFormula

Instances For

def PDL.loadMulti :

List Program → Program → Formula → LoadFormula

Load a nonempty modal sequence given its prefix and final program.

Equations

PDL.loadMulti x✝² x✝¹ x✝ = List.foldr (fun (β : PDL.Program) (lf : PDL.LoadFormula) => PDL.LoadFormula.box β (PDL.AnyFormula.loaded lf)) (PDL.LoadFormula.box x✝¹ (PDL.AnyFormula.normal x✝)) x✝²

Instances For

@[simp]

theorem PDL.loadMulti_nil {α : Program} {φ : Formula} :

loadMulti [] α φ = LoadFormula.box α (AnyFormula.normal φ)

@[simp]

theorem PDL.loadMulti_cons {β : Program} {δ : List Program} {α : Program} {φ : Formula} :

loadMulti (β :: δ) α φ = LoadFormula.box β (AnyFormula.loaded (loadMulti δ α φ))

def PDL.LoadFormula.boxes :

List Program → LoadFormula → LoadFormula

Prepend a list of loaded boxes to a loaded continuation.

Equations

PDL.LoadFormula.boxes x✝¹ x✝ = List.foldr (fun (β : PDL.Program) (lf : PDL.LoadFormula) => PDL.LoadFormula.box β (PDL.AnyFormula.loaded lf)) x✝ x✝¹

Instances For

@[simp]

theorem PDL.LoadFormula.boxes_nil {χ : LoadFormula} :

boxes [] χ = χ

theorem PDL.LoadFormula.boxes_cons {b : Program} {bs : List Program} {φ : LoadFormula} :

boxes (b :: bs) φ = box b (AnyFormula.loaded (boxes bs φ))

def PDL.LoadFormula.unload :

LoadFormula → Formula

Erase loading annotations to obtain an ordinary formula.

Equations

(PDL.LoadFormula.box α (PDL.AnyFormula.normal φ)).unload = PDL.Formula.box α φ
(PDL.LoadFormula.box α (PDL.AnyFormula.loaded χ)).unload = PDL.Formula.box α χ.unload

Instances For

@[simp]

theorem PDL.unload_loadMulti {δ : List Program} {α : Program} {φ : Formula} :

(loadMulti δ α φ).unload = Formula.boxes δ (Formula.box α φ)

inductive PDL.NegLoadFormula :

A negated loaded formula.

neg : LoadFormula → NegLoadFormula

Instances For

def PDL.instReprNegLoadFormula.repr :

NegLoadFormula → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance PDL.instReprNegLoadFormula :

Repr NegLoadFormula

Equations

PDL.instReprNegLoadFormula = { reprPrec := PDL.instReprNegLoadFormula.repr }

def PDL.instDecidableEqNegLoadFormula.decEq (x✝ x✝¹ : NegLoadFormula) :

Decidable (x✝ = x✝¹)

Equations

PDL.instDecidableEqNegLoadFormula.decEq (PDL.NegLoadFormula.neg a) (PDL.NegLoadFormula.neg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

DecidableEq NegLoadFormula

@[instance_reducible]

instance PDL.instDecidableEqNegLoadFormula :

Equations

PDL.instDecidableEqNegLoadFormula = PDL.instDecidableEqNegLoadFormula.decEq

def PDL.«term⌊_⌋_» :

A loaded box modality.

Equations

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

Instances For

def PDL.«term⌊⌊_⌋⌋_» :

Iterated loaded boxes for a list of programs.

Equations

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

Instances For

def PDL.«term~'_» :

Negation of a loaded formula.

Equations

PDL.«term~'_» = Lean.ParserDescr.node `PDL.«term~'_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~'") (Lean.ParserDescr.cat `term 0))

Instances For

def PDL.«term~''_» :

Negation of an ordinary or loaded formula.

Equations

PDL.«term~''_» = Lean.ParserDescr.node `PDL.«term~''_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~''") (Lean.ParserDescr.cat `term 1023))

Instances For

def PDL.negUnload :

NegLoadFormula → Formula

Erase loading annotations from a negated loaded formula.

Equations

PDL.negUnload (PDL.NegLoadFormula.neg χ) = χ.unload.neg

Instances For

theorem PDL.loadBoxes_append {as bs : List Program} {P : LoadFormula} :

LoadFormula.boxes (as ++ bs) P = LoadFormula.boxes as (LoadFormula.boxes bs P)

theorem PDL.loadBoxes_last {a : Program} {as : List Program} {c : Program} {P : LoadFormula} :

NegLoadFormula.neg (LoadFormula.box a (AnyFormula.loaded (LoadFormula.boxes (as ++ [c]) P))) = NegLoadFormula.neg (LoadFormula.box a (AnyFormula.loaded (LoadFormula.boxes as (LoadFormula.box c (AnyFormula.loaded P)))))

@[simp]

theorem PDL.unload_boxes {δ : List Program} {φ : LoadFormula} :

(LoadFormula.boxes δ φ).unload = Formula.boxes δ φ.unload

@[simp]

theorem PDL.unload_neg_loaded {α : Program} {χ : LoadFormula} :

(NegLoadFormula.neg (LoadFormula.box α (AnyFormula.loaded χ))).1.unload = Formula.box α χ.unload

@[simp]

theorem PDL.unload_neg_normal {α : Program} {φ : Formula} :

(NegLoadFormula.neg (LoadFormula.box α (AnyFormula.normal φ))).1.unload = Formula.box α φ

def PDL.AnyFormula.loadBoxes :

List Program → AnyFormula → AnyFormula

Load a possibly already loaded formula χ with a sequence δ of boxes. The result is loaded iff δ≠[] or χ was loaded.

Equations

PDL.AnyFormula.loadBoxes x✝¹ x✝ = List.foldr (fun (β : PDL.Program) (lf : PDL.AnyFormula) => PDL.AnyFormula.loaded (PDL.LoadFormula.box β lf)) x✝ x✝¹

Instances For

@[simp]

theorem PDL.AnyFormula.boxes_nil {ξ : AnyFormula} :

loadBoxes [] ξ = ξ

@[simp]

theorem PDL.AnyFormula.loadBoxes_cons {α : Program} {γ : List Program} {ξ : AnyFormula} :

loadBoxes (α :: γ) ξ = loaded (LoadFormula.box α (loadBoxes γ ξ))

theorem PDL.AnyFormula.loadBoxes_append {as bs : List Program} {φ : AnyFormula} :

loadBoxes (as ++ bs) φ = loadBoxes as (loadBoxes bs φ)

theorem PDL.AnyFormula.loadBoxes_loaded_eq_loaded_boxes {δ : List Program} {χ : LoadFormula} :

loadBoxes δ (loaded χ) = loaded (LoadFormula.boxes δ χ)

def PDL.AnyFormula.unload :

AnyFormula → Formula

Erase loading annotations, leaving ordinary formulas unchanged.

Equations

(PDL.AnyFormula.normal φ).unload = φ
(PDL.AnyFormula.loaded χ).unload = χ.unload

Instances For

theorem PDL.box_loadBoxes_append_eq_of_loaded_eq_loadBoxes {χ' : LoadFormula} {φ : Formula} {d : Program} {δ αs : List Program} (h : AnyFormula.loaded χ' = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) :

LoadFormula.box d (AnyFormula.loadBoxes (δ ++ αs) (AnyFormula.normal φ)) = LoadFormula.boxes (d :: δ) χ'

@[simp]

theorem PDL.AnyFormulaBoxBoxes_eq_FormulaBoxLoadBoxes_inside_unload {α : Program} {φ : Formula} {αs : List Program} :

(LoadFormula.box α (AnyFormula.loadBoxes αs (AnyFormula.normal φ))).unload = Formula.box α (AnyFormula.loadBoxes αs (AnyFormula.normal φ)).unload

theorem PDL.AnyFormula.loadBoxes_unload_eq_boxes {βs : List Program} {φ : Formula} :

(loadBoxes βs (normal φ)).unload = Formula.boxes βs φ

theorem PDL.loaded_eq_to_unload_eq (χ : LoadFormula) (αs : List Program) (φ : Formula) (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) :

χ.unload = Formula.boxes αs φ

Spliting of loaded formulas #

def PDL.AnyFormula.split (af : AnyFormula) :

List Program × Formula

Split any formula into the list of loaded boxes and the free formula.

Equations

(PDL.AnyFormula.loaded lf).split = lf.split
(PDL.AnyFormula.normal f).split = ([], f)

Instances For

def PDL.LoadFormula.split (lf : LoadFormula) :

List Program × Formula

Split a loaded formula into the list of loaded boxes and the free formula.

Equations

(PDL.LoadFormula.box α af).split = (fun (x : List PDL.Program × PDL.Formula) => match x with | (δ, f) => (α :: δ, f)) af.split

Instances For

theorem PDL.LoadFormula.split_boxes_cons {βs : List Program} {α : Program} {φ : Formula} :

(boxes βs (box α (AnyFormula.normal φ))).split = (βs ++ [α], φ)

@[simp]

theorem PDL.AnyFormula.split_normal (φ : Formula) :

(normal φ).split = ([], φ)

theorem PDL.AnyFormula.split_eq_nil_is_normal (ξ : AnyFormula) (φ : Formula) :

ξ.split = ([], φ) → ξ = normal φ

theorem PDL.LoadFormula.split_inj {ξ ξ' : LoadFormula} (h : ξ.split = ξ'.split) :

ξ = ξ'

theorem PDL.AnyFormula.split_inj {ξ ξ' : AnyFormula} (h : ξ.split = ξ'.split) :

ξ = ξ'

theorem PDL.AnyFormula.box_split {α : Program} (af : AnyFormula) :

(LoadFormula.box α af).split = (α :: af.split.1, af.split.2)

@[simp]

theorem PDL.LoadFormula.split_list_not_empty (lf : LoadFormula) :

lf.split.1 ≠ []

def PDL.loadMultiNonEmpty (δ : List Program) (h : δ ≠ []) :

Formula → LoadFormula

Construct a loaded modal sequence from a list known to be nonempty.

Equations

PDL.loadMultiNonEmpty [] h x✝ = ⋯.elim
PDL.loadMultiNonEmpty [α] x_3 x✝ = PDL.LoadFormula.box α (PDL.AnyFormula.normal x✝)
PDL.loadMultiNonEmpty (α :: d :: δ) x_3 x✝ = PDL.LoadFormula.box α (PDL.AnyFormula.loaded (PDL.loadMultiNonEmpty (d :: δ) ⋯ x✝))

Instances For

@[simp]

theorem PDL.loadMulti_nonEmpty_box {δ : List Program} {α : Program} {h' : α :: δ ≠ []} {φ : Formula} (h : δ ≠ []) :

loadMultiNonEmpty (α :: δ) h' φ = LoadFormula.box α (AnyFormula.loaded (loadMultiNonEmpty δ h φ))

@[simp]

theorem PDL.loadMulti_split {α : Program} {φ : Formula} {αs : List Program} :

(loadMulti αs α φ).split = (αs ++ [α], φ)

@[simp]

theorem PDL.loadMulti_nonEmpty_unload {δ : List Program} {h : δ ≠ []} {φ : Formula} :

(loadMultiNonEmpty δ h φ).unload = Formula.boxes δ φ

theorem PDL.LoadFormula.split_eq_loadMulti_nonEmpty {δ : List Program} {φ : Formula} (lf : LoadFormula) (h : lf.split = (δ, φ)) :

lf = loadMultiNonEmpty δ ⋯ φ

theorem PDL.LoadFormula.split_eq_loadMulti_nonEmpty' {δ : List Program} {φ : Formula} (lf : LoadFormula) (h : δ ≠ []) (h2 : lf.split = (δ, φ)) :

lf = loadMultiNonEmpty δ h φ

theorem PDL.loadMulti_nonEmpty_eq_loadMulti {δ : List Program} {α : Program} {h : δ ++ [α] ≠ []} {φ : Formula} :

loadMultiNonEmpty (δ ++ [α]) h φ = loadMulti δ α φ

theorem PDL.LoadFormula.split_eq_loadMulti (lf : LoadFormula) {δ : List Program} {α : Program} {φ : Formula} (h : lf.split = (δ ++ [α], φ)) :

lf = loadMulti δ α φ

theorem PDL.LoadFormula.exists_splitLast (lf : LoadFormula) :

∃ (δ : List Program) (α : Program), lf.split.1 = δ ++ [α]

theorem PDL.LoadFormula.exists_loadMulti (lf : LoadFormula) :

∃ (δ : List Program) (α : Program) (φ : Formula), lf = loadMulti δ α φ

theorem PDL.loadMulti_eq_of_some {d : Program} {δ : List Program} {β : Program} {φ : Formula} (h : δ.head? = some d) :

loadMulti δ β φ = LoadFormula.box d (AnyFormula.loaded (loadMulti δ.tail β φ))

theorem PDL.loadMulti_eq_loadBoxes {δ : List Program} {α : Program} {φ : Formula} :

AnyFormula.loaded (loadMulti δ α φ) = AnyFormula.loadBoxes (δ ++ [α]) (AnyFormula.normal φ)

splitLast #

def PDL.splitLast {α : Type u_1} :

List α → Option (List α × α)

Helper function for YsetLoad' to get last list element.

Equations

PDL.splitLast [] = none
PDL.splitLast (x_1 :: xs) = some (match PDL.splitLast xs with | none => ([], x_1) | some (ys, y) => (x_1 :: ys, y))

Instances For

@[simp]

theorem PDL.splitLast_nil {α : Type u_1} :

splitLast [] = none

theorem PDL.nil_of_splitLast_none {α : Type u_1} {δs : List α} :

splitLast δs = none → δs = []

theorem PDL.splitLast_cons_eq_some {α : Type u_1} (x : α) (xs : List α) :

splitLast (x :: xs) = some ((x :: xs).dropLast, (x :: xs).getLast ⋯)

@[simp]

theorem PDL.splitLast_append_singleton {α : Type u_1} {xs : List α} {x : α} :

splitLast (xs ++ [x]) = some (xs, x)

theorem PDL.splitLast_inj {α : Type u_1} {xs ys : List α} (h : splitLast xs = splitLast ys) :

xs = ys

theorem PDL.LoadFormula.split_splitLast_to_loadBoxes {δs : List Program} {φ : Formula} {δs_ : List Program} {δ : Program} {ξ : AnyFormula} (ξsp_def : ξ.split = (δs, φ)) (sp_def : splitLast δs = some (δs_, δ)) :

ξ = AnyFormula.loadBoxes (δs_ ++ [δ]) (AnyFormula.normal φ)

theorem PDL.splitLast_undo_of_some {α : Type u_1} {αs : List α} {βs_b : List α × α} (h : splitLast αs = some βs_b) :

βs_b.1 ++ [βs_b.2] = αs

theorem PDL.loadMulti_of_splitLast_cons {α : Program} {αs βs : List Program} {β : Program} {φ : Formula} (h : splitLast (α :: αs) = some (βs, β)) :

loadMulti βs β φ = LoadFormula.box α (AnyFormula.loadBoxes αs (AnyFormula.normal φ))

Measures #

@[implicit_reducible]

def PDL.lengthOfProgram :

Program → ℕ

The syntactic length of a program, mutually defined with formula length.

Equations

PDL.lengthOfProgram (PDL.Program.atom_prog a) = 1
PDL.lengthOfProgram (a.sequence a_1) = 1 + PDL.lengthOfProgram a + PDL.lengthOfProgram a_1
PDL.lengthOfProgram (a.union a_1) = 1 + PDL.lengthOfProgram a + PDL.lengthOfProgram a_1
PDL.lengthOfProgram a.star = 1 + PDL.lengthOfProgram a
PDL.lengthOfProgram (PDL.Program.test a) = 2 + PDL.lengthOfFormula a

Instances For

@[implicit_reducible]

def PDL.lengthOfFormula :

Formula → ℕ

The syntactic length of a formula, mutually defined with program length.

Equations

PDL.lengthOfFormula PDL.Formula.bottom = 1
PDL.lengthOfFormula (PDL.Formula.atom_prop a) = 1
PDL.lengthOfFormula φ.neg = 1 + PDL.lengthOfFormula φ
PDL.lengthOfFormula (φ.and ψ) = 1 + PDL.lengthOfFormula φ + PDL.lengthOfFormula ψ
PDL.lengthOfFormula (PDL.Formula.box α φ) = 1 + PDL.lengthOfProgram α + PDL.lengthOfFormula φ

Instances For

theorem PDL.lengthOfProgram_gt_zero (α : Program) :

0 < lengthOfProgram α

class PDL.HasLength (α : Type) :

Types equipped with a natural-valued syntactic length.

lengthOf : α → ℕ
The syntactic length of an object.

Instances

@[instance_reducible]

instance PDL.formulaHasLength :

HasLength Formula

Equations

PDL.formulaHasLength = { lengthOf := PDL.lengthOfFormula }

@[instance_reducible]

instance PDL.setFormulaHasLength :

HasLength (Finset Formula)

Equations

PDL.setFormulaHasLength = { lengthOf := fun (X : Finset PDL.Formula) => X.sum PDL.lengthOfFormula }

@[instance_reducible]

instance PDL.listFormulaHasLength :

HasLength (List Formula)

Equations

PDL.listFormulaHasLength = { lengthOf := fun (X : List PDL.Formula) => (List.map PDL.lengthOfFormula X).sum }

@[instance_reducible]

instance PDL.programHasLength :

HasLength Program

Equations

PDL.programHasLength = { lengthOf := PDL.lengthOfProgram }

@[instance_reducible]

instance PDL.setProgramHasLength :

HasLength (Finset Program)

Equations

PDL.setProgramHasLength = { lengthOf := fun (X : Finset PDL.Program) => X.sum PDL.lengthOfProgram }

theorem PDL.Formula.ne_neg_neg_self (φ : Formula) :

φ ≠ φ.neg.neg

No formula is its own double negation.

theorem PDL.pair_neg_ne_singleton (φ ψ : Formula) :

{φ, φ.neg} ≠ {ψ}

A pair {φ, ~φ} is never a singleton.

theorem PDL.pair_neg_inj {φ ψ : Formula} (h : {φ, φ.neg} = {ψ, ψ.neg}) :

φ = ψ

The pairs {φ, ~φ} determine φ.

Sorting formulas #

Needed to convert a Finset Formula to List Formula.

TODO: make this a separate file