Documentation

def Program.isAtomic :

Program → Prop

Equations

(·a).isAtomic = (true = true)
x✝.isAtomic = (false = true)

Instances For

theorem Formula.neq_neg_self (φ : Formula) :

φ ≠ ~φ

DecidablePred Program.isAtomic

@[instance_reducible]

instance instDecidablePredProgramIsAtomic :

Equations

theorem Program.isAtomic_iff {α : Program} :

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

def Program.isStar :

Program → Prop

Equations

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

Instances For

DecidablePred Program.isStar

@[instance_reducible]

instance instDecidablePredProgramIsStar :

Equations

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

theorem Program.isStar_iff {α : Program} :

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

Tools for Box Formulas #

@[simp]

theorem Formula.boxes_nil {φ : Formula} :

(⌈⌈[]⌉⌉φ) = φ

@[simp]

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

(⌈⌈β :: δ⌉⌉φ) = ⌈β⌉⌈⌈δ⌉⌉φ

@[simp]

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

((⌈⌈αs⌉⌉φ) = ⌈⌈αs⌉⌉ψ) ↔ φ = ψ

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

(⌈⌈δ ++ [α]⌉⌉φ) = ⌈⌈δ⌉⌉⌈α⌉φ

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

(⌈⌈as ++ bs⌉⌉P) = ⌈⌈as⌉⌉⌈⌈bs⌉⌉P

def boxesOf :

Formula → List Program × Formula

Equations

boxesOf (⌈prog⌉nextf) = match boxesOf nextf with | (rest, endf) => (prog :: rest, endf)
boxesOf x✝ = ([], x✝)

Instances For

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

φ = ⌈⌈γ⌉⌉ψ

def Formula.isBox :

Formula → Prop

Equations

(⌈prog⌉nextf).isBox = True
x✝.isBox = False

Instances For

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

boxesOf φ = (γ, ψ)

@[simp]

theorem boxesOf_output_not_isBox {φ : Formula} :

¬(boxesOf φ).2.isBox

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

¬ψ.isBox

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

boxesOf φ = ([], φ)

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

boxesOf (⌈⌈δs⌉⌉⌈α⌉φ) = (δs ++ [α], φ)

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

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

(⌈β⌉⌈⌈δ⌉⌉φ) ≠ φ

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

αs <+: (boxesOf (⌈⌈α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 AnyFormula :

normal : Formula → AnyFormula
loaded : LoadFormula → AnyFormula

Instances For

partial def instReprLoadFormula.repr_2 :

LoadFormula → ℕ → Std.Format

@[instance_reducible]

instance instReprAnyFormula :

Repr AnyFormula

Equations

instReprAnyFormula = { reprPrec := instReprAnyFormula.repr_1 }

partial def instReprAnyFormula.repr_2 :

LoadFormula → ℕ → Std.Format

partial def instReprAnyFormula.repr_1 :

AnyFormula → ℕ → Std.Format

@[instance_reducible]

instance instReprLoadFormula :

Repr LoadFormula

Equations

instReprLoadFormula = { reprPrec := instReprLoadFormula.repr_2 }

partial def instReprLoadFormula.repr_1 :

AnyFormula → ℕ → Std.Format

@[instance_reducible]

instance instDecidableEqAnyFormula :

DecidableEq AnyFormula

Equations

instDecidableEqAnyFormula = instDecidableEqAnyFormula.decEq_1

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

Decidable (x✝ = x✝¹)

Equations

instDecidableEqAnyFormula.decEq_1 (AnyFormula.normal a) (AnyFormula.normal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
instDecidableEqAnyFormula.decEq_1 (AnyFormula.normal a) (AnyFormula.loaded a_1) = isFalse ⋯
instDecidableEqAnyFormula.decEq_1 (AnyFormula.loaded a) (AnyFormula.normal a_1) = isFalse ⋯
instDecidableEqAnyFormula.decEq_1 (AnyFormula.loaded a) (AnyFormula.loaded b) = if h : a = b then h ▸ have inst := instDecidableEqAnyFormula.decEq_2 a a; isTrue ⋯ else isFalse ⋯

Instances For

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

Decidable (x✝ = x✝¹)

Equations

instDecidableEqLoadFormula.decEq_1 (AnyFormula.normal a) (AnyFormula.normal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
instDecidableEqLoadFormula.decEq_1 (AnyFormula.normal a) (AnyFormula.loaded a_1) = isFalse ⋯
instDecidableEqLoadFormula.decEq_1 (AnyFormula.loaded a) (AnyFormula.normal a_1) = isFalse ⋯
instDecidableEqLoadFormula.decEq_1 (AnyFormula.loaded a) (AnyFormula.loaded b) = if h : a = b then h ▸ have inst := instDecidableEqLoadFormula.decEq_2 a a; isTrue ⋯ else isFalse ⋯

Instances For

def 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 instDecidableEqLoadFormula :

DecidableEq LoadFormula

Equations

instDecidableEqLoadFormula = instDecidableEqLoadFormula.decEq_2

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

inductive LoadFormula :

box : Program → AnyFormula → LoadFormula

Instances For

@[instance_reducible]

instance instCoeFormulaAnyFormula :

Coe Formula AnyFormula

Equations

instCoeFormulaAnyFormula = { coe := AnyFormula.normal }

Coe LoadFormula AnyFormula

@[instance_reducible]

instance instCoeLoadFormulaAnyFormula :

Equations

instCoeLoadFormulaAnyFormula = { coe := AnyFormula.loaded }

inductive AnyNegFormula :

neg : AnyFormula → AnyNegFormula

Instances For

def loadMulti :

List Program → Program → Formula → LoadFormula

Equations

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

Instances For

@[simp]

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

loadMulti [] α φ = ⌊α⌋AnyFormula.normal φ

@[simp]

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

loadMulti (β :: δ) α φ = ⌊β⌋AnyFormula.loaded (loadMulti δ α φ)

def LoadFormula.boxes :

List Program → LoadFormula → LoadFormula

Equations

(⌊⌊x✝¹⌋⌋x✝) = List.foldr (fun (β : Program) (lf : LoadFormula) => ⌊β⌋AnyFormula.loaded lf) x✝ x✝¹

Instances For

@[simp]

theorem LoadFormula.boxes_nil {χ : LoadFormula} :

(⌊⌊[]⌋⌋χ) = χ

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

(⌊⌊b :: bs⌋⌋φ) = ⌊b⌋AnyFormula.loaded (⌊⌊bs⌋⌋φ)

def LoadFormula.unload :

LoadFormula → Formula

Equations

(⌊α⌋AnyFormula.normal φ).unload = ⌈α⌉φ
(⌊α⌋AnyFormula.loaded χ).unload = ⌈α⌉χ.unload

Instances For

@[simp]

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

(loadMulti δ α φ).unload = ⌈⌈δ⌉⌉⌈α⌉φ

inductive NegLoadFormula :

neg : LoadFormula → NegLoadFormula

Instances For

@[instance_reducible]

instance instReprNegLoadFormula :

Repr NegLoadFormula

Equations

instReprNegLoadFormula = { reprPrec := instReprNegLoadFormula.repr }

def instReprNegLoadFormula.repr :

NegLoadFormula → ℕ → Std.Format

Equations

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

Instances For

DecidableEq NegLoadFormula

@[instance_reducible]

instance instDecidableEqNegLoadFormula :

Equations

instDecidableEqNegLoadFormula = instDecidableEqNegLoadFormula.decEq

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

Decidable (x✝ = x✝¹)

Equations

instDecidableEqNegLoadFormula.decEq (~'a) (~'b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

def «term⌊_⌋_» :

Equations

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

Instances For

def «term⌊⌊_⌋⌋_» :

Equations

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

Instances For

def «term~'_» :

Equations

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

Instances For

def «term~''_» :

Equations

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

Instances For

def negUnload :

NegLoadFormula → Formula

Equations

negUnload (~'a) = ~a.unload

Instances For

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

(⌊⌊as ++ bs⌋⌋P) = ⌊⌊as⌋⌋⌊⌊bs⌋⌋P

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

(~'⌊a⌋AnyFormula.loaded (⌊⌊as ++ [c]⌋⌋P)) = ~'⌊a⌋AnyFormula.loaded (⌊⌊as⌋⌋⌊c⌋AnyFormula.loaded P)

@[simp]

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

(⌊⌊δ⌋⌋φ).unload = ⌈⌈δ⌉⌉φ.unload

@[simp]

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

(~'⌊α⌋AnyFormula.loaded χ).1.unload = ⌈α⌉χ.unload

@[simp]

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

(~'⌊α⌋AnyFormula.normal φ).1.unload = ⌈α⌉φ

def 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

AnyFormula.loadBoxes x✝¹ x✝ = List.foldr (fun (β : Program) (lf : AnyFormula) => AnyFormula.loaded (⌊β⌋lf)) x✝ x✝¹

Instances For

@[simp]

theorem AnyFormula.boxes_nil {ξ : AnyFormula} :

loadBoxes [] ξ = ξ

@[simp]

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

loadBoxes (α :: γ) ξ = loaded (⌊α⌋loadBoxes γ ξ)

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

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

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

loadBoxes δ (loaded χ) = loaded (⌊⌊δ⌋⌋χ)

def AnyFormula.unload :

AnyFormula → Formula

Equations

(AnyFormula.normal a).unload = a
(AnyFormula.loaded a).unload = a.unload

Instances For

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

(⌊d⌋AnyFormula.loadBoxes (δ ++ αs) (AnyFormula.normal φ)) = ⌊⌊d :: δ⌋⌋χ'

@[simp]

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

(⌊α⌋AnyFormula.loadBoxes αs (AnyFormula.normal φ)).unload = ⌈α⌉(AnyFormula.loadBoxes αs (AnyFormula.normal φ)).unload

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

(loadBoxes βs (normal φ)).unload = ⌈⌈βs⌉⌉φ

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

χ.unload = ⌈⌈αs⌉⌉φ

Spliting of loaded formulas #

def AnyFormula.split (af : AnyFormula) :

List Program × Formula

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

Equations

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

Instances For

def LoadFormula.split (lf : LoadFormula) :

List Program × Formula

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

Equations

(⌊a⌋a_1).split = (fun (x : List Program × Formula) => match x with | (δ, f) => (a :: δ, f)) a_1.split

Instances For

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

(⌊⌊βs⌋⌋⌊α⌋AnyFormula.normal φ).split = (βs ++ [α], φ)

@[simp]

theorem AnyFormula.split_normal (φ : Formula) :

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

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

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

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

ξ = ξ'

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

ξ = ξ'

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

(⌊α⌋af).split = (α :: af.split.1, af.split.2)

@[simp]

theorem LoadFormula.split_list_not_empty (lf : LoadFormula) :

lf.split.1 ≠ []

def loadMulti_nonEmpty (δ : List Program) (h : δ ≠ []) :

Formula → LoadFormula

Equations

loadMulti_nonEmpty [] h x✝ = ⋯.elim
loadMulti_nonEmpty [α] x_3 x✝ = ⌊α⌋AnyFormula.normal x✝
loadMulti_nonEmpty (α :: d :: δ) x_3 x✝ = ⌊α⌋AnyFormula.loaded (loadMulti_nonEmpty (d :: δ) ⋯ x✝)

Instances For

@[simp]

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

loadMulti_nonEmpty (α :: δ) h' φ = ⌊α⌋AnyFormula.loaded (loadMulti_nonEmpty δ h φ)

@[simp]

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

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

@[simp]

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

(loadMulti_nonEmpty δ h φ).unload = ⌈⌈δ⌉⌉φ

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

lf = loadMulti_nonEmpty δ ⋯ φ

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

lf = loadMulti_nonEmpty δ h φ

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

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

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

lf = loadMulti δ α φ

theorem LoadFormula.exists_splitLast (lf : LoadFormula) :

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

theorem LoadFormula.exists_loadMulti (lf : LoadFormula) :

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

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

loadMulti δ β φ = ⌊d⌋AnyFormula.loaded (loadMulti δ.tail β φ)

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

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

splitLast #

def splitLast {α : Type u_1} :

List α → Option (List α × α)

Helper function for YsetLoad' to get last list element.

Equations

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

Instances For

@[simp]

theorem splitLast_nil {α : Type u_1} :

splitLast [] = none

theorem nil_of_splitLast_none {α✝ : Type u_1} {δs : List α✝} :

splitLast δs = none → δs = []

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

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

@[simp]

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

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

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

xs = ys

theorem 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 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 loadMulti_of_splitLast_cons {α : Program} {αs βs : List Program} {β : Program} {φ : Formula} (h : splitLast (α :: αs) = some (βs, β)) :

loadMulti βs β φ = ⌊α⌋AnyFormula.loadBoxes αs (AnyFormula.normal φ)

Measures #

@[implicit_reducible]

def lengthOfProgram :

Program → ℕ

Equations

lengthOfProgram (·a) = 1
lengthOfProgram (a;'a_1) = 1 + lengthOfProgram a + lengthOfProgram a_1
lengthOfProgram (a⋓a_1) = 1 + lengthOfProgram a + lengthOfProgram a_1
lengthOfProgram (∗a) = 1 + lengthOfProgram a
lengthOfProgram (?'a) = 2 + lengthOfFormula a

Instances For

@[implicit_reducible]

def lengthOfFormula :

Formula → ℕ

Equations

lengthOfFormula Formula.bottom = 1
lengthOfFormula (·a) = 1
lengthOfFormula (~a) = 1 + lengthOfFormula a
lengthOfFormula (a ⋀ a_1) = 1 + lengthOfFormula a + lengthOfFormula a_1
lengthOfFormula (⌈a⌉a_1) = 1 + lengthOfProgram a + lengthOfFormula a_1

Instances For

theorem lengthOfProgram_gt_zero (α : Program) :

0 < lengthOfProgram α

class HasLength (α : Type) :

lengthOf : α → ℕ

Instances

@[instance_reducible]

instance formulaHasLength :

HasLength Formula

Equations

formulaHasLength = { lengthOf := lengthOfFormula }

@[instance_reducible]

instance setFormulaHasLength :

HasLength (Finset Formula)

Equations

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

@[instance_reducible]

instance listFormulaHasLength :

HasLength (List Formula)

Equations

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

@[instance_reducible]

instance programHasLength :

HasLength Program

Equations

programHasLength = { lengthOf := lengthOfProgram }

@[instance_reducible]

instance setProgramHasLength :

HasLength (Finset Program)

Equations

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

theorem Formula.ne_neg_neg_self (φ : Formula) :

φ ≠ ~~φ

No formula is its own double negation.

theorem pair_neg_ne_singleton (φ ψ : Formula) :

{φ, ~φ} ≠ {ψ}

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

theorem pair_neg_inj {φ ψ : Formula} (h : {φ, ~φ} = {ψ, ~ψ}) :

φ = ψ

The pairs {φ, ~φ} determine φ.

Sorting formulas #

Needed to convert a Finset Formula to List Formula.

TODO: make this a separate file