structure Constraint (α : Type) : Type

• prop : α → Prop
• verify' : Validator.Result α self.prop
• elim_exists : (∃ (a : α), self.prop a) → { a : α // self.prop a ∧ ∀ (a' : α), self.prop a' → a' = a }
• message : Option String

def Constraint.elim_exists_0 {prop : Unit → Prop} : (∃ (v : Unit), prop v) → { v : Unit // prop v ∧ ∀ (v' : Unit), prop v' → v' = v }

Equations

• Constraint.elim_exists_0 h' = ⟨(), ⋯⟩

def Constraint.tacticElim_exists_1_ : Lean.ParserDescr

Equations

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

def Constraint.tacticElim_exists_2_ : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev Constraint.valid {α : Type} (h : Constraint α) : Prop

Equations

• h.valid = ∃ (a : α), h.prop a

def Constraint.verify {α : Type} (h : Constraint α) : Validator.Result α h.prop

Equations

• h.verify = Validator.withErrorMessage h.message h.verify'

def Constraint.seq {α1 α2 : Type} (h1 : Constraint α1) (h2 : α1 → Constraint α2) : Constraint (α1 × α2)

Equations

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

@[simp]

theorem Constraint.seq.prop_eq {α1 α2 : Type} {a : α1} {a' : α2} (h : Constraint α1) (h' : α1 → Constraint α2) : (h.seq h').prop (a, a') = (h.prop a ∧ (h' a).prop a')

def Constraint.and {α1 α2 : Type} (h1 : Constraint α1) (h2 : Constraint α2) : Constraint (α1 × α2)

Equations

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

def Constraint.«term_∧ᶜ_» : Lean.TrailingParserDescr

Equations

• Constraint.«term_∧ᶜ_» = Lean.ParserDescr.trailingNode `Constraint.«term_∧ᶜ_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∧ᶜ") (Lean.ParserDescr.cat `term 70))

@[simp]

theorem Constraint.and.prop_eq {α1 α2 : Type} {a : α1} {a' : α2} (h : Constraint α1) (h' : Constraint α2) : (h∧ᶜh').prop (a, a') = (h.prop a ∧ h'.prop a')

@[simp]

theorem Constraint.and.valid_eq {α1 α2 : Type} (h : Constraint α1) (h' : Constraint α2) : (h∧ᶜh').valid = (h.valid ∧ h'.valid)

def Constraint.eq (h : Constraint ℕ) (T : Validator.SetType) (Eᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Constraint.eq.prop_eq {T : Validator.SetType} {Eᵢ : ℕ} {a : Unit} (h : Constraint ℕ) : (h.eq T Eᵢ).prop a = h.prop Eᵢ

@[reducible, inline]

abbrev Constraint.eqState (h : Constraint ℕ) (Eᵢ : ℕ) : Constraint Unit

Equations

• h.eqState Eᵢ = h.eq Validator.SetType.States Eᵢ

@[reducible, inline]

abbrev Constraint.eqAction (h : Constraint ℕ) (Eᵢ : ℕ) : Constraint Unit

Equations

• h.eqAction Eᵢ = h.eq Validator.SetType.Actions Eᵢ

def Constraint.leftEq (h : Constraint (ℕ × ℕ)) (T : Validator.SetType) (E1ᵢ : ℕ) : Constraint ℕ

Equations

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

@[simp]

theorem Constraint.leftEq.prop_eq {T : Validator.SetType} {E1ᵢ E2ᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.leftEq T E1ᵢ).prop E2ᵢ = h.prop (E1ᵢ, E2ᵢ)

@[reducible, inline]

abbrev Constraint.leftEqState (h : Constraint (ℕ × ℕ)) (Eᵢ : ℕ) : Constraint ℕ

Equations

• h.leftEqState Eᵢ = h.leftEq Validator.SetType.States Eᵢ

@[reducible, inline]

abbrev Constraint.leftEqAction (h : Constraint (ℕ × ℕ)) (Eᵢ : ℕ) : Constraint ℕ

Equations

• h.leftEqAction Eᵢ = h.leftEq Validator.SetType.Actions Eᵢ

def Constraint.rightEq (h : Constraint (ℕ × ℕ)) (T : Validator.SetType) (E2ᵢ : ℕ) : Constraint ℕ

Equations

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

@[simp]

theorem Constraint.rightEq.prop_eq {T : Validator.SetType} {E1ᵢ E2ᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.rightEq T E2ᵢ).prop E1ᵢ = h.prop (E1ᵢ, E2ᵢ)

@[reducible, inline]

abbrev Constraint.rightEqState (h : Constraint (ℕ × ℕ)) (Eᵢ : ℕ) : Constraint ℕ

Equations

• h.rightEqState Eᵢ = h.rightEq Validator.SetType.States Eᵢ

@[reducible, inline]

abbrev Constraint.rightEqAction (h : Constraint (ℕ × ℕ)) (Eᵢ : ℕ) : Constraint ℕ

Equations

• h.rightEqAction Eᵢ = h.rightEq Validator.SetType.Actions Eᵢ

def Constraint.bothEq (h : Constraint (ℕ × ℕ)) (T1 T2 : Validator.SetType) (E1ᵢ E2ᵢ : ℕ) : Constraint Unit

Equations

• h.bothEq T1 T2 E1ᵢ E2ᵢ = (h.leftEq T1 E1ᵢ).eq T2 E2ᵢ

@[simp]

theorem Constraint.bothEq.prop_eq {T1 T2 : Validator.SetType} {Eᵢ E'ᵢ : ℕ} {a : Unit} (h : Constraint (ℕ × ℕ)) : (h.bothEq T1 T2 Eᵢ E'ᵢ).prop a = h.prop (Eᵢ, E'ᵢ)

@[reducible, inline]

abbrev Constraint.eqStates (h : Constraint (ℕ × ℕ)) (E1ᵢ E2ᵢ : ℕ) : Constraint Unit

Equations

• h.eqStates E1ᵢ E2ᵢ = h.bothEq Validator.SetType.States Validator.SetType.States E1ᵢ E2ᵢ

@[reducible, inline]

abbrev Constraint.eqStateAction (h : Constraint (ℕ × ℕ)) (E1ᵢ E2ᵢ : ℕ) : Constraint Unit

Equations

• h.eqStateAction E1ᵢ E2ᵢ = h.bothEq Validator.SetType.States Validator.SetType.Actions E1ᵢ E2ᵢ

def Constraint.trivial : Constraint Unit

Equations

• Constraint.trivial = { prop := fun (x : Unit) => True, verify' := pure ⟨(), True.intro⟩, elim_exists := Constraint.elim_exists_0 }

def Constraint.bounds (T : Validator.ConstraintType) (limit Eᵢ : ℕ) : Constraint Unit

Equations

• Constraint.bounds T limit Eᵢ = { prop := fun (x : Unit) => Eᵢ < limit, verify' := if h : Eᵢ < limit then pure ⟨(), h⟩ else T.throw_out_of_bounds Eᵢ, elim_exists := Constraint.elim_exists_0 }

@[simp]

theorem Constraint.bounds.prop_eq {T : Validator.ConstraintType} {limit Eᵢ : ℕ} {a : Unit} : (bounds T limit Eᵢ).prop a ↔ Eᵢ < limit

@[simp]

theorem Constraint.bounds.valid_eq {T : Validator.ConstraintType} {limit Eᵢ : ℕ} : (bounds T limit Eᵢ).valid ↔ Eᵢ < limit

@[reducible, inline]

abbrev Constraint.actionBounds (limit Aᵢ : ℕ) : Constraint Unit

Equations

• Constraint.actionBounds limit Aᵢ = Constraint.bounds Validator.ConstraintType.ActionSetConstraint limit Aᵢ

@[reducible, inline]

abbrev Constraint.stateBounds (limit Sᵢ : ℕ) : Constraint Unit

Equations

• Constraint.stateBounds limit Sᵢ = Constraint.bounds Validator.ConstraintType.StateSetConstraint limit Sᵢ

@[reducible, inline]

abbrev Constraint.knowledgeBounds (limit Kᵢ : ℕ) : Constraint Unit

Equations

• Constraint.knowledgeBounds limit Kᵢ = Constraint.bounds Validator.ConstraintType.KnowledgeConstraint limit Kᵢ

@[reducible, inline]

abbrev Constraint.setBounds (S : Validator.SetType) (limit Eᵢ : ℕ) : Constraint Unit

Equations

• Constraint.setBounds S limit Eᵢ = Constraint.bounds S.toConstraintType limit Eᵢ

def Constraint.actionBounds' {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Aᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Constraint.actionBounds'.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Aᵢ : ℕ} {a : Unit} : (actionBounds' C Aᵢ).prop a ↔ Aᵢ < C.actions.size

def Constraint.stateBounds' {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Constraint.stateBounds'.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (stateBounds' C Sᵢ).prop a ↔ Sᵢ < C.states.size

@[reducible, inline]

abbrev Constraint.setBounds' {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (S : Validator.SetType) : ℕ → Constraint Unit

Equations

• Constraint.setBounds' C Validator.SetType.Actions x✝ = Constraint.actionBounds' C x✝
• Constraint.setBounds' C Validator.SetType.States x✝ = Constraint.stateBounds' C x✝

def Constraint.isActionAll {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Aᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Constraint.isActionAll.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Aᵢ : ℕ} {a : Unit} : (isActionAll C Aᵢ).prop a ↔ Aᵢ < C.actions.size ∧ C.actions[Aᵢ]? = some Validator.ActionSetExpr.all

def Constraint.isActionUnion {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Aᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isActionUnion.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Aᵢ A'ᵢ A''ᵢ : ℕ} : (isActionUnion C Aᵢ).prop (A'ᵢ, A''ᵢ) ↔ Aᵢ < C.actions.size ∧ C.actions[Aᵢ]? = some (Validator.ActionSetExpr.union A'ᵢ A''ᵢ)

def Constraint.isStateConst {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (S : Validator.StateSetExpr pt) (Sᵢ : ℕ) : Constraint Unit

Equations

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

def Constraint.isStateEmpty {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• Constraint.isStateEmpty C Sᵢ = Constraint.isStateConst C Validator.StateSetExpr.empty Sᵢ

@[simp]

theorem Constraint.isStateEmpty.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (isStateEmpty C Sᵢ).prop a ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some Validator.StateSetExpr.empty

def Constraint.isStateInit {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• Constraint.isStateInit C Sᵢ = Constraint.isStateConst C Validator.StateSetExpr.init Sᵢ

@[simp]

theorem Constraint.isStateInit.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (isStateInit C Sᵢ).prop a ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some Validator.StateSetExpr.init

def Constraint.isStateGoal {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• Constraint.isStateGoal C Sᵢ = Constraint.isStateConst C Validator.StateSetExpr.goal Sᵢ

@[simp]

theorem Constraint.isStateGoal.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (isStateGoal C Sᵢ).prop a ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some Validator.StateSetExpr.goal

def Constraint.isStateNeg {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint ℕ

Equations

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

@[simp]

theorem Constraint.isStateNeg.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ : ℕ} : (isStateNeg C Sᵢ).prop S'ᵢ ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.neg S'ᵢ)

def Constraint.isStateInter {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isStateInter.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ S''ᵢ : ℕ} : (isStateInter C Sᵢ).prop (S'ᵢ, S''ᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.inter S'ᵢ S''ᵢ)

def Constraint.isStateUnion {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isStateUnion.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ S''ᵢ : ℕ} : (isStateUnion C Sᵢ).prop (S'ᵢ, S''ᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.union S'ᵢ S''ᵢ)

def Constraint.isStateProgr {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isStateProgr.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ Aᵢ : ℕ} : (isStateProgr C Sᵢ).prop (S'ᵢ, Aᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.progr S'ᵢ Aᵢ)

def Constraint.isStateRegr {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isStateRegr.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ Aᵢ : ℕ} : (isStateRegr C Sᵢ).prop (S'ᵢ, Aᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.regr S'ᵢ Aᵢ)

@[reducible, inline]

abbrev Constraint.isUnion {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) : Validator.SetType → ℕ → Constraint (ℕ × ℕ)

Equations

• Constraint.isUnion C Validator.SetType.Actions = Constraint.isActionUnion C
• Constraint.isUnion C Validator.SetType.States = Constraint.isStateUnion C

def Constraint.isDeadKnowledge {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Kᵢ : ℕ) : Constraint ℕ

Equations

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

@[simp]

theorem Constraint.isDeadKnowledge.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Kᵢ Sᵢ : ℕ} : (isDeadKnowledge C Kᵢ).prop Sᵢ = ∃ (K : Validator.DeadKnowledge Sᵢ), C.knowledge[Kᵢ]? = some (Validator.Knowledge.dead Sᵢ K)

def Constraint.isActionSubsetKnowledge {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Kᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isActionSubsetKnowledge.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Kᵢ Aᵢ A'ᵢ : ℕ} : (isActionSubsetKnowledge C Kᵢ).prop (Aᵢ, A'ᵢ) = ∃ (K : Validator.ActionSubsetKnowledge Aᵢ A'ᵢ), C.knowledge[Kᵢ]? = some (Validator.Knowledge.actionSubset Aᵢ A'ᵢ K)

def Constraint.isStateSubsetKnowledge {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) (Kᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

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

@[simp]

theorem Constraint.isStateSubsetKnowledge.prop_eq {n : ℕ} {pt : Validator.STRIPS n} {C : Validator.Certificate pt} {Kᵢ Sᵢ S'ᵢ : ℕ} : (isStateSubsetKnowledge C Kᵢ).prop (Sᵢ, S'ᵢ) = ∃ (K : Validator.StateSubsetKnowledge Sᵢ S'ᵢ), C.knowledge[Kᵢ]? = some (Validator.Knowledge.stateSubset Sᵢ S'ᵢ K)

@[reducible, inline]

abbrev Constraint.isSubsetKnowledge {n : ℕ} {pt : Validator.STRIPS n} (C : Validator.Certificate pt) : Validator.SetType → ℕ → Constraint (ℕ × ℕ)

Equations

• Constraint.isSubsetKnowledge C Validator.SetType.Actions = Constraint.isActionSubsetKnowledge C
• Constraint.isSubsetKnowledge C Validator.SetType.States = Constraint.isStateSubsetKnowledge C