inductive Validator.SetType : Type

• Actions : SetType
• States : SetType

inductive Validator.ConstraintType : Type

• ActionSetConstraint : ConstraintType
• StateSetConstraint : ConstraintType
• KnowledgeConstraint : ConstraintType

@[reducible, inline]

abbrev Validator.SetType.toConstraintType : SetType → ConstraintType

Equations

• Validator.SetType.Actions.toConstraintType = Validator.ConstraintType.ActionSetConstraint
• Validator.SetType.States.toConstraintType = Validator.ConstraintType.StateSetConstraint

instance Validator.instToStringConstraintType : ToString ConstraintType

Equations

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

def Validator.ConstraintType.throw_out_of_bounds {α : outParam Type} {p : α → Prop} (T : ConstraintType) (Eᵢ : ℕ) : Result α p

Equations

• T.throw_out_of_bounds Eᵢ = Validator.throwUnvalid (toString "There is no " ++ toString T ++ toString " with identifier #" ++ toString Eᵢ ++ toString ".")

def Validator.ConstraintType.throw_not_eq {α : outParam Type} {p : α → Prop} (T : ConstraintType) (Eᵢ E'ᵢ : ℕ) : Result α p

Equations

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

def Validator.ConstraintType.throw_unexpected {α : outParam Type} {β : Type u_1} {γ : Type u_2} [ToString β] [ToString γ] {p : α → Prop} (T : ConstraintType) (Eᵢ : ℕ) (expected : β) (found : γ) : Result α p

Equations

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

def Validator.verify_bounds (T : ConstraintType) (limit Eᵢ : ℕ) : Result' (Eᵢ < limit)

Equations

• Validator.verify_bounds T limit Eᵢ = if h : Eᵢ < limit then pure ⟨(), h⟩ else T.throw_out_of_bounds Eᵢ

def Validator.verify_action_bounds (limit Eᵢ : ℕ) : Result' (Eᵢ < limit)

Equations

• Validator.verify_action_bounds = Validator.verify_bounds Validator.ConstraintType.ActionSetConstraint

def Validator.verify_state_bounds (limit Eᵢ : ℕ) : Result' (Eᵢ < limit)

Equations

• Validator.verify_state_bounds = Validator.verify_bounds Validator.ConstraintType.StateSetConstraint

def Validator.verify_and {p1 p2 : Prop} (res1 : Result' p1) (res2 : Result' p2) : Result' (p1 ∧ p2)

Equations

• Validator.verify_and res1 res2 = do let __discr ← res1 match __discr with | ⟨PUnit.unit, h1⟩ => do let __discr ← res2 match __discr with | ⟨PUnit.unit, h2⟩ => pure ⟨(), ⋯⟩

def Validator.verifyActionsEnum {n : ℕ} (pt : STRIPS n) (as : List ℕ) : Result' (∀ a ∈ as, a < List.length pt.actions')

Equations

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

def Validator.Certificate.validActionSetExpr {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Aᵢ : Fin C.actions.size) : Prop

Equations

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

def Validator.Certificate.validStateSetExpr {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Sᵢ : Fin C.states.size) : Prop

Equations

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

def Validator.Certificate.verifyActionSetExpr {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Aᵢ : Fin C.actions.size) : Result' (C.validActionSetExpr Aᵢ)

Equations

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

def Validator.Certificate.verifyStateSetExpr {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Sᵢ : Fin C.states.size) : Result' (C.validStateSetExpr Sᵢ)

Equations

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

structure Validator.Certificate.validSets {n : ℕ} {pt : STRIPS n} (C : Certificate pt) : Prop

• validActions (Aᵢ : Fin C.actions.size) : C.validActionSetExpr Aᵢ
• validStates (Sᵢ : Fin C.states.size) : C.validStateSetExpr Sᵢ

@[reducible, inline]

abbrev Validator.Certificate.validSets.ActionIds {n : ℕ} (pt : STRIPS n) : Type

Equations

• Validator.Certificate.validSets.ActionIds pt = List (Fin (List.length pt.actions'))

@[reducible, inline]

abbrev Validator.Certificate.validSets.ActionIds.toActions {n : ℕ} {pt : STRIPS n} (A : ActionIds pt) : Actions n

Equations

• A.toActions = ↑(List.map (fun (x : Fin (List.length pt.actions')) => pt.actions'[x]) A).toFinset

@[irreducible]

def Validator.Certificate.validSets.getActions' {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Aᵢ : Fin C.actions.size) : ActionIds pt

Equations

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

def Validator.Certificate.validSets.getActions {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Aᵢ : Fin C.actions.size) : Actions n

Equations

• hC.getActions Aᵢ = (hC.getActions' Aᵢ).toActions

theorem Validator.Certificate.validSets.getActionsAll {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} (Aᵢ : Fin C.actions.size) (h : C.actions[Aᵢ]? = some ActionSetExpr.all) : hC.getActions Aᵢ = pt.actions

theorem Validator.Certificate.validSets.getActionsUnion {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} (Aᵢ A'ᵢ A''ᵢ : Fin C.actions.size) (h : C.actions[Aᵢ]? = some (ActionSetExpr.union ↑A'ᵢ ↑A''ᵢ)) : hC.getActions Aᵢ = hC.getActions A'ᵢ ∪ hC.getActions A''ᵢ

@[irreducible]

def Validator.Certificate.validSets.getStates {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) : States n

Equations

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

theorem Validator.Certificate.validSets.getStatesEmpty {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some StateSetExpr.empty) : hC.getStates Sᵢ = ∅

theorem Validator.Certificate.validSets.getStatesInit {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some StateSetExpr.init) : hC.getStates Sᵢ = {pt.init}

theorem Validator.Certificate.validSets.getStatesGoal {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some StateSetExpr.goal) : hC.getStates Sᵢ = pt.goal_states

theorem Validator.Certificate.validSets.getStatesBdd {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) {φ : Formalism.UnprimedVariable pt (BDD (2 * n))} (h : C.states[Sᵢ]? = some (StateSetExpr.bdd φ)) : hC.getStates Sᵢ = (↑φ).toStates

theorem Validator.Certificate.validSets.getStatesHorn {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) {φ : Formalism.UnprimedVariable pt (Horn (2 * n))} (h : C.states[Sᵢ]? = some (StateSetExpr.horn φ)) : hC.getStates Sᵢ = (↑φ).toStates

theorem Validator.Certificate.validSets.getStatesMods {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) {φ : Formalism.UnprimedVariable pt (MODS (2 * n))} (h : C.states[Sᵢ]? = some (StateSetExpr.mods φ)) : hC.getStates Sᵢ = (↑φ).toStates

theorem Validator.Certificate.validSets.getStatesNeg {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some (StateSetExpr.neg ↑S'ᵢ)) : hC.getStates Sᵢ = (hC.getStates S'ᵢ)ᶜ

theorem Validator.Certificate.validSets.getStatesInter {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ S''ᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some (StateSetExpr.inter ↑S'ᵢ ↑S''ᵢ)) : hC.getStates Sᵢ = hC.getStates S'ᵢ ∩ hC.getStates S''ᵢ

theorem Validator.Certificate.validSets.getStatesUnion {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ S''ᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some (StateSetExpr.union ↑S'ᵢ ↑S''ᵢ)) : hC.getStates Sᵢ = hC.getStates S'ᵢ ∪ hC.getStates S''ᵢ

theorem Validator.Certificate.validSets.getStatesProg {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ : Fin C.states.size) (Aᵢ : Fin C.actions.size) (h : C.states[Sᵢ]? = some (StateSetExpr.progr ↑S'ᵢ ↑Aᵢ)) : hC.getStates Sᵢ = pt.progression (hC.getStates S'ᵢ) (hC.getActions Aᵢ)

theorem Validator.Certificate.validSets.getStatesRegr {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ : Fin C.states.size) (Aᵢ : Fin C.actions.size) (h : C.states[Sᵢ]? = some (StateSetExpr.regr ↑S'ᵢ ↑Aᵢ)) : hC.getStates Sᵢ = pt.regression (hC.getStates S'ᵢ) (hC.getActions Aᵢ)