Proof System for Certifying Unsolvability

We define the proof system for unsolvability described in [Eri19], which was originally introduced in [ERH17]. More specifically this file contains

• the definition of dead states and dead state sets,
• a shallow embedding of the proof system, and
• proofs for soundness and completeness of the system.

Dead States and Dead State Sets

@[reducible, inline]

abbrev Validator.ProofSystem.DeadState {n : ℕ} (pt : STRIPS.PlanningTask n) (s : STRIPS.State n) : Prop

A state s is dead iff it is not part of any plan for pt.

Equations

• Validator.ProofSystem.DeadState pt s = ∀ (plan : pt.Plan pt.init), s ∉ plan.path

theorem Validator.ProofSystem.dead_state_iff {n : ℕ} (pt : STRIPS.PlanningTask n) (s : STRIPS.State n) : DeadState pt s ↔ ¬pt.Reachable pt.init s ∨ pt.UnsolvableState s

Alternative definiton of dead states.

@[reducible, inline]

abbrev Validator.ProofSystem.Dead {n : ℕ} (pt : STRIPS.PlanningTask n) (S : STRIPS.States n) : Prop

A set of states is dead iff all its members are dead.

Equations

• Validator.ProofSystem.Dead pt S = ∀ s ∈ S, Validator.ProofSystem.DeadState pt s

Proof System

inductive Validator.ProofSystem.Derivation {n : ℕ} (pt : STRIPS.PlanningTask n) (conclusion : Prop) : Type 1

A derivation (or proof tree) in the proof system deriving the statement conclusion.

• B1 {n : ℕ} {pt : STRIPS.PlanningTask n} (R : Type) [Formalism pt R] {S S' : STRIPS.States n} : Formalism.IsLiteralInter pt R S → Formalism.IsLiteralUnion pt R S' → S ⊆ S' → Derivation pt (S ⊆ S')

  Basic statement 1

• B2 {n : ℕ} {pt : STRIPS.PlanningTask n} (R : Type) [Formalism pt R] {S S' : STRIPS.States n} : Formalism.IsProgrInter pt R S → Formalism.IsLiteralUnion pt R S' → S ⊆ S' → Derivation pt (S ⊆ S')

  Basic statement 2

• B3 {n : ℕ} {pt : STRIPS.PlanningTask n} (R : Type) [Formalism pt R] {S S' : STRIPS.States n} : Formalism.IsRegrInter pt R S → Formalism.IsLiteralUnion pt R S' → S ⊆ S' → Derivation pt (S ⊆ S')

  Basic statement 3

• B4 {n : ℕ} {pt : STRIPS.PlanningTask n} (R R' : Type) [Formalism pt R] [Formalism pt R'] {S S' : STRIPS.States n} : Formalism.IsLiteral pt R S → Formalism.IsLiteral pt R' S' → S ⊆ S' → Derivation pt (S ⊆ S')

  Basic statement 4

• B5 {n : ℕ} {pt : STRIPS.PlanningTask n} (A A' : STRIPS.Actions n) : A ⊆ A' → Derivation pt (A ⊆ A')

  Basic statement 5

• ED {n : ℕ} {pt : STRIPS.PlanningTask n} : Derivation pt (Dead pt ∅)

  Empty set Dead

• UD {n : ℕ} {pt : STRIPS.PlanningTask n} (S S' : STRIPS.States n) : Derivation pt (Dead pt S) → Derivation pt (Dead pt S') → Derivation pt (Dead pt (S ∪ S'))

  Union Dead

• SD {n : ℕ} {pt : STRIPS.PlanningTask n} (S S' : STRIPS.States n) : Derivation pt (Dead pt S') → Derivation pt (S ⊆ S') → Derivation pt (Dead pt S)

  Subset Dead

• PG {n : ℕ} {pt : STRIPS.PlanningTask n} (S S' : STRIPS.States n) : Derivation pt (STRIPS.progression S pt.actions ⊆ S ∪ S') → Derivation pt (Dead pt S') → Derivation pt (Dead pt (S ∩ pt.goalStates)) → Derivation pt (Dead pt S)

  Progression Goal

• PI {n : ℕ} {pt : STRIPS.PlanningTask n} (S S' : STRIPS.States n) : Derivation pt (STRIPS.progression S pt.actions ⊆ S ∪ S') → Derivation pt (Dead pt S') → Derivation pt ({pt.init} ⊆ S) → Derivation pt (Dead pt Sᶜ)

  Progression Initial

• RG {n : ℕ} {pt : STRIPS.PlanningTask n} (S S' : STRIPS.States n) : Derivation pt (STRIPS.regression S pt.actions ⊆ S ∪ S') → Derivation pt (Dead pt S') → Derivation pt (Dead pt (Sᶜ ∩ pt.goalStates)) → Derivation pt (Dead pt Sᶜ)

  Regression Goal

• RI {n : ℕ} {pt : STRIPS.PlanningTask n} (S S' : STRIPS.States n) : Derivation pt (STRIPS.regression S pt.actions ⊆ S ∪ S') → Derivation pt (Dead pt S') → Derivation pt ({pt.init} ⊆ Sᶜ) → Derivation pt (Dead pt S)

  Regression Initial

• CI {n : ℕ} {pt : STRIPS.PlanningTask n} : Derivation pt (Dead pt {pt.init}) → Derivation pt pt.Unsolvable

  Conclusion Initial

• CG {n : ℕ} {pt : STRIPS.PlanningTask n} : Derivation pt (Dead pt pt.goalStates) → Derivation pt pt.Unsolvable

  Conclusion Goal

• UR {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' : Set α) : Derivation pt (E ⊆ E ∪ E')

  Union Right

• UL {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' : Set α) : Derivation pt (E ⊆ E' ∪ E)

  Union Left

• IR {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' : Set α) : Derivation pt (E ∩ E' ⊆ E)

  Intersection Right

• IL {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' : Set α) : Derivation pt (E' ∩ E ⊆ E)

  Intersection Left

• DI {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' E'' : Set α) : Derivation pt ((E ∪ E') ∩ E'' ⊆ E ∩ E'' ∪ E' ∩ E'')

  DIstributivity

• SU {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' E'' : Set α) : Derivation pt (E ⊆ E'') → Derivation pt (E' ⊆ E'') → Derivation pt (E ∪ E' ⊆ E'')

  Subset Union

• SI {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' E'' : Set α) : Derivation pt (E ⊆ E') → Derivation pt (E ⊆ E'') → Derivation pt (E ⊆ E' ∩ E'')

  Subset Intersection

• ST {n : ℕ} {pt : STRIPS.PlanningTask n} {α : Type} (E E' E'' : Set α) : Derivation pt (E ⊆ E') → Derivation pt (E' ⊆ E'') → Derivation pt (E ⊆ E'')

  Subset Transitivity

• AT {n : ℕ} {pt : STRIPS.PlanningTask n} {x✝ : ℕ} (S S' : STRIPS.States x✝) (A A' : STRIPS.Actions x✝) : Derivation pt (STRIPS.progression S A ⊆ S') → Derivation pt (A' ⊆ A) → Derivation pt (STRIPS.progression S A' ⊆ S')

  Action Transitivity

• AU {n : ℕ} {pt : STRIPS.PlanningTask n} {x✝ : ℕ} (S S' : STRIPS.States x✝) (A A' : STRIPS.Actions x✝) : Derivation pt (STRIPS.progression S A ⊆ S') → Derivation pt (STRIPS.progression S A' ⊆ S') → Derivation pt (STRIPS.progression S (A ∪ A') ⊆ S')

  Action Union

• PT {n : ℕ} {pt : STRIPS.PlanningTask n} {x✝ : ℕ} (S S' S'' : STRIPS.States x✝) (A : STRIPS.Actions x✝) : Derivation pt (STRIPS.progression S A ⊆ S'') → Derivation pt (S' ⊆ S) → Derivation pt (STRIPS.progression S' A ⊆ S'')

  Progression Transitivity

• PU {n : ℕ} {pt : STRIPS.PlanningTask n} {x✝ : ℕ} (S S' S'' : STRIPS.States x✝) (A : STRIPS.Actions x✝) : Derivation pt (STRIPS.progression S A ⊆ S'') → Derivation pt (STRIPS.progression S' A ⊆ S'') → Derivation pt (STRIPS.progression (S ∪ S') A ⊆ S'')

  Progression Union

• PR {n : ℕ} {pt : STRIPS.PlanningTask n} {x✝ : ℕ} (S S' : STRIPS.States x✝) (A : STRIPS.Actions x✝) : Derivation pt (STRIPS.progression S A ⊆ S') → Derivation pt (STRIPS.regression S'ᶜ A ⊆ Sᶜ)

  Progression to Regression

• RP {n : ℕ} {pt : STRIPS.PlanningTask n} {x✝ : ℕ} (S S' : STRIPS.States x✝) (A : STRIPS.Actions x✝) : Derivation pt (STRIPS.regression S'ᶜ A ⊆ Sᶜ) → Derivation pt (STRIPS.progression S A ⊆ S')

  Regression to Progression

Soundness of the Proof System

theorem Validator.ProofSystem.progression_goal {n : ℕ} {pt : STRIPS.PlanningTask n} {S S' : STRIPS.States n} (h1 : STRIPS.progression S pt.actions ⊆ S ∪ S') (h2 : Dead pt S') (h3 : Dead pt (S ∩ pt.goalStates)) : Dead pt S

theorem Validator.ProofSystem.progression_initial {n : ℕ} {pt : STRIPS.PlanningTask n} {S S' : STRIPS.States n} (h1 : STRIPS.progression S pt.actions ⊆ S ∪ S') (h2 : Dead pt S') (h3 : {pt.init} ⊆ S) : Dead pt Sᶜ

theorem Validator.ProofSystem.regression_goal {n : ℕ} {pt : STRIPS.PlanningTask n} {S S' : STRIPS.States n} (h1 : STRIPS.regression S pt.actions ⊆ S ∪ S') (h2 : Dead pt S') (h3 : Dead pt (Sᶜ ∩ pt.goalStates)) : Dead pt Sᶜ

theorem Validator.ProofSystem.regression_initial {n : ℕ} {pt : STRIPS.PlanningTask n} {S S' : STRIPS.States n} (h1 : STRIPS.regression S pt.actions ⊆ S ∪ S') (h2 : Dead pt S') (h3 : {pt.init} ⊆ Sᶜ) : Dead pt S

theorem Validator.ProofSystem.Derivation.soundness {n : ℕ} {pt : STRIPS.PlanningTask n} {conclusion : Prop} (d : Derivation pt conclusion) : conclusion

The proof system is sound, i.e. given a derivation in the proof system, the conclusion of this derivation holds.

Completeness of the Proof System

theorem Validator.ProofSystem.Derivation.completeness {n : ℕ} {pt : STRIPS.PlanningTask n} : pt.Unsolvable → Nonempty (Derivation pt pt.Unsolvable)

The proof system is complete, i.e. if the planning task pt is unsolvable, then there exists a derivation in the proof system showing that pt is unsolvable.