Documentation

def Program.isAtomic :

Program → Prop

Equations

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

Instances For

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 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} {αs : List Program} {ψ : Formula} (h : boxesOf φ = (αs, ψ)) :

φ = ⌈⌈αs⌉⌉ψ

def Formula.isBox :

Formula → Prop

Equations

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

Instances For

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

boxesOf φ = (αs, ψ)

@[simp]

theorem boxesOf_output_not_isBox {φ : Formula} :

¬(boxesOf φ).snd.isBox

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

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

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

αs <+: (boxesOf (⌈⌈αs⌉⌉φ)).fst

Loaded Formulas #

inductive AnyFormula :

normal : Formula → AnyFormula
loaded : LoadFormula → AnyFormula

Instances For

partial def instReprAnyFormula.repr_2 :

LoadFormula → ℕ → Std.Format

instance instReprAnyFormula :

Repr AnyFormula

Equations

instReprAnyFormula = { reprPrec := instReprAnyFormula.repr_1 }

instance instReprLoadFormula :

Repr LoadFormula

Equations

instReprLoadFormula = { reprPrec := instReprLoadFormula.repr_2 }

partial def instReprAnyFormula.repr_1 :

AnyFormula → ℕ → Std.Format

partial def instReprLoadFormula.repr_2 :

LoadFormula → ℕ → Std.Format

partial def instReprLoadFormula.repr_1 :

AnyFormula → ℕ → Std.Format

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

instance instDecidableEqAnyFormula :

DecidableEq AnyFormula

Equations

instDecidableEqAnyFormula = instDecidableEqAnyFormula.decEq_1

instance instDecidableEqLoadFormula :

DecidableEq LoadFormula

Equations

instDecidableEqLoadFormula = instDecidableEqLoadFormula.decEq_2

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

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 instCoeFormulaAnyFormula :

Coe Formula AnyFormula

Equations

instCoeFormulaAnyFormula = { coe := AnyFormula.normal }

Coe LoadFormula AnyFormula

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

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

DecidableEq NegLoadFormula

instance instDecidableEqNegLoadFormula :

Equations

instDecidableEqNegLoadFormula = instDecidableEqNegLoadFormula.decEq

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

@[simp]

theorem AnyFormula.split_normal (φ : Formula) :

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

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

(⌊α⌋af).split = (α :: af.split.fst, af.split.snd)

@[simp]

theorem LoadFormula.split_list_not_empty (lf : LoadFormula) :

lf.split.fst ≠ []

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.fst = δ ++ [α]

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 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} {αs βs : List α✝} (h : splitLast αs = splitLast βs) :

αs = βs

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

βs_b.fst ++ [βs_b.snd] = αs