Certificate

Implementation of the certificates used when validating certificates

inductive Validator.ActionSetExpr : Type

• enum : List ℕ → ActionSetExpr
• union : ℕ → ℕ → ActionSetExpr
• all : ActionSetExpr

instance Validator.instReprActionSetExpr : Repr ActionSetExpr

Equations

• Validator.instReprActionSetExpr = { reprPrec := Validator.instReprActionSetExpr.repr }

def Validator.instReprActionSetExpr.repr : ActionSetExpr → ℕ → Std.Format

Equations

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

def Validator.ActionSetExpr.toSting : ActionSetExpr → String

Equations

• (Validator.ActionSetExpr.enum a).toSting = toString "the action set containing the actions with ids " ++ toString a
• (Validator.ActionSetExpr.union a a_1).toSting = toString "the union of the action sets #" ++ toString a ++ toString " and #" ++ toString a_1
• Validator.ActionSetExpr.all.toSting = "the constant set of all actions"

instance Validator.instToStringActionSetExpr : ToString ActionSetExpr

Equations

• Validator.instToStringActionSetExpr = { toString := Validator.ActionSetExpr.toSting }

inductive Validator.StateSetExpr {n : ℕ} (pt : STRIPS n) : Type

• empty {n : ℕ} {pt : STRIPS n} : StateSetExpr pt
• init {n : ℕ} {pt : STRIPS n} : StateSetExpr pt
• goal {n : ℕ} {pt : STRIPS n} : StateSetExpr pt
• bdd {n : ℕ} {pt : STRIPS n} : Formalism.UnprimedVariable pt (BDD (2 * n)) → StateSetExpr pt
• horn {n : ℕ} {pt : STRIPS n} : Formalism.UnprimedVariable pt (Horn (2 * n)) → StateSetExpr pt
• mods {n : ℕ} {pt : STRIPS n} : Formalism.UnprimedVariable pt (MODS (2 * n)) → StateSetExpr pt
• neg {n : ℕ} {pt : STRIPS n} : ℕ → StateSetExpr pt
• inter {n : ℕ} {pt : STRIPS n} : ℕ → ℕ → StateSetExpr pt
• union {n : ℕ} {pt : STRIPS n} : ℕ → ℕ → StateSetExpr pt
• progr {n : ℕ} {pt : STRIPS n} : ℕ → ℕ → StateSetExpr pt
• regr {n : ℕ} {pt : STRIPS n} : ℕ → ℕ → StateSetExpr pt

def Validator.instDecidableEqStateSetExpr.decEq {n✝ : ℕ} {pt✝ : STRIPS n✝} (x✝ x✝¹ : StateSetExpr pt✝) : Decidable (x✝ = x✝¹)

Equations

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

instance Validator.instDecidableEqStateSetExpr {n✝ : ℕ} {pt✝ : STRIPS n✝} : DecidableEq (StateSetExpr pt✝)

Equations

• Validator.instDecidableEqStateSetExpr = Validator.instDecidableEqStateSetExpr.decEq

def Validator.instReprStateSetExpr.repr {n✝ : ℕ} {pt✝ : STRIPS n✝} : StateSetExpr pt✝ → ℕ → Std.Format

Equations

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

instance Validator.instReprStateSetExpr {n✝ : ℕ} {pt✝ : STRIPS n✝} : Repr (StateSetExpr pt✝)

Equations

• Validator.instReprStateSetExpr = { reprPrec := Validator.instReprStateSetExpr.repr }

def Validator.StateSetExpr.toString {n : ℕ} {pt : STRIPS n} : StateSetExpr pt → String

Equations

• Validator.StateSetExpr.empty.toString = "the constant empty set"
• Validator.StateSetExpr.init.toString = "the constant set containing the initial state"
• Validator.StateSetExpr.goal.toString = "the constant goal set"
• (Validator.StateSetExpr.bdd a).toString = "a BDD state set"
• (Validator.StateSetExpr.horn a).toString = "a horn state set"
• (Validator.StateSetExpr.mods a).toString = "a MODS state set"
• (Validator.StateSetExpr.neg a).toString = toString "the negation of the state set #" ++ toString a
• (Validator.StateSetExpr.inter a a_1).toString = toString "the intersection of the state sets #" ++ toString a ++ toString " and #" ++ toString a_1
• (Validator.StateSetExpr.union a a_1).toString = toString "the union of the state sets #" ++ toString a ++ toString " and #" ++ toString a_1
• (Validator.StateSetExpr.progr a a_1).toString = toString "the progression of the state set #" ++ toString a ++ toString " with the action set #" ++ toString a_1
• (Validator.StateSetExpr.regr a a_1).toString = toString "the regression of the state set #" ++ toString a ++ toString " with the action set #" ++ toString a_1

instance Validator.instToStringStateSetExpr {n : ℕ} {pt : STRIPS n} : ToString (StateSetExpr pt)

Equations

• Validator.instToStringStateSetExpr = { toString := Validator.StateSetExpr.toString }

inductive Validator.DeadKnowledge : ℕ → Type

• ED (Sᵢ : ℕ) : DeadKnowledge Sᵢ

  Empty set Dead

• UD (Sᵢ a✝ : ℕ) : ℕ → DeadKnowledge Sᵢ

  Union Dead

• SD (Sᵢ a✝ : ℕ) : ℕ → DeadKnowledge Sᵢ

  Subset Dead

• PG (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Progression Goal

• PI (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Progression Initial

• RG (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Regression Goal

• RI (Sᵢ a✝ : ℕ) : ℕ → ℕ → DeadKnowledge Sᵢ

  Regression Initial

def Validator.instReprDeadKnowledge.repr {a✝ : ℕ} : DeadKnowledge a✝ → ℕ → Std.Format

Equations

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

instance Validator.instReprDeadKnowledge {a✝ : ℕ} : Repr (DeadKnowledge a✝)

Equations

• Validator.instReprDeadKnowledge = { reprPrec := Validator.instReprDeadKnowledge.repr }

inductive Validator.StateSubsetKnowledge : ℕ → ℕ → Type

• B1 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 1

• B2 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 2

• B3 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 3

• B4 (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Basic statement 4

• URS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Union Right State

• ULS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Union Left State

• IRS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Intersection Right State

• ILS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Intersection Left State

• DIS (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  DIstributivity State

• SUS (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Subset Union State

• SIS (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Subset Intersection State

• STS (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Subset Transitivity State

• AT (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Action Transitivity

• AU (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Action Union

• PT (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Progression Transitivity

• PU (Sᵢ S'ᵢ a✝ : ℕ) : ℕ → StateSubsetKnowledge Sᵢ S'ᵢ

  Progression Union

• PR (Sᵢ S'ᵢ a✝ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Progression to Regression

• RP (Sᵢ S'ᵢ a✝ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ

  Regression to Progression

def Validator.instReprStateSubsetKnowledge.repr {a✝ a✝¹ : ℕ} : StateSubsetKnowledge a✝ a✝¹ → ℕ → Std.Format

Equations

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

instance Validator.instReprStateSubsetKnowledge {a✝ a✝¹ : ℕ} : Repr (StateSubsetKnowledge a✝ a✝¹)

Equations

• Validator.instReprStateSubsetKnowledge = { reprPrec := Validator.instReprStateSubsetKnowledge.repr }

inductive Validator.ActionSubsetKnowledge : ℕ → ℕ → Type

• B5 (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ

  Basic statement 5

• URA (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ

  Union Right Action

• ULA (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ

  Union Left Action

• SUA (Aᵢ A'ᵢ a✝ : ℕ) : ℕ → ActionSubsetKnowledge Aᵢ A'ᵢ

  Subset Union Action

• STA (Aᵢ A'ᵢ a✝ : ℕ) : ℕ → ActionSubsetKnowledge Aᵢ A'ᵢ

  Subset Transitivity Action

def Validator.instReprActionSubsetKnowledge.repr {a✝ a✝¹ : ℕ} : ActionSubsetKnowledge a✝ a✝¹ → ℕ → Std.Format

Equations

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

instance Validator.instReprActionSubsetKnowledge {a✝ a✝¹ : ℕ} : Repr (ActionSubsetKnowledge a✝ a✝¹)

Equations

• Validator.instReprActionSubsetKnowledge = { reprPrec := Validator.instReprActionSubsetKnowledge.repr }

inductive Validator.UnsolvableKnowledge : Type

• CI : ℕ → UnsolvableKnowledge

  Conclusion Initial

• CG : ℕ → UnsolvableKnowledge

  Conclusion Goal

instance Validator.instReprUnsolvableKnowledge : Repr UnsolvableKnowledge

Equations

• Validator.instReprUnsolvableKnowledge = { reprPrec := Validator.instReprUnsolvableKnowledge.repr }

def Validator.instReprUnsolvableKnowledge.repr : UnsolvableKnowledge → ℕ → Std.Format

Equations

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

inductive Validator.Knowledge : Type

• dead (Sᵢ : ℕ) : DeadKnowledge Sᵢ → Knowledge
• actionSubset (Aᵢ A'ᵢ : ℕ) : ActionSubsetKnowledge Aᵢ A'ᵢ → Knowledge
• stateSubset (Sᵢ S'ᵢ : ℕ) : StateSubsetKnowledge Sᵢ S'ᵢ → Knowledge
• unsolvable : UnsolvableKnowledge → Knowledge

instance Validator.instReprKnowledge : Repr Knowledge

Equations

• Validator.instReprKnowledge = { reprPrec := Validator.instReprKnowledge.repr }

def Validator.instReprKnowledge.repr : Knowledge → ℕ → Std.Format

Equations

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

instance Validator.instToStringKnowledge : ToString Knowledge

Equations

• Validator.instToStringKnowledge = { toString := fun (x : Validator.Knowledge) => "TODO" }

structure Validator.Certificate {n : ℕ} (pt : STRIPS n) : Type

• actions : Array ActionSetExpr
• states : Array (StateSetExpr pt)
• knowledge : Array Knowledge

instance Validator.instReprCertificate {n✝ : ℕ} {pt✝ : STRIPS n✝} : Repr (Certificate pt✝)

Equations

• Validator.instReprCertificate = { reprPrec := Validator.instReprCertificate.repr }

def Validator.instReprCertificate.repr {n✝ : ℕ} {pt✝ : STRIPS n✝} : Certificate pt✝ → ℕ → Std.Format

Equations

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

instance Validator.instToStringCertificate {n : ℕ} {pt : STRIPS n} : ToString (Certificate pt)

Equations

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