Basic definitions for the STRIPS formalism

We define some basic definitions of the STRIPS formalism for automated planning. More specifically, this file implements:

• Basic definitions of states, actions, planning tasks, etc.,
• Definition of paths in the search space and various lemmas to work with them,
• Definition of reachability, plans and unsolvability,
• Progression and regression, and various lemmas to work with them.

States and sets of states

@[reducible, inline]

abbrev STRIPS.State (n : ℕ) : Type

A state is a set of variables, containing all variables that are true.

Equations

• STRIPS.State n = Set (Fin n)

@[reducible, inline]

abbrev STRIPS.States (n : ℕ) : Type

A set of states

Equations

• STRIPS.States n = Set (STRIPS.State n)

Actions and sets of actions

structure STRIPS.Action (n : ℕ) : Type

Actions in the STRIPS formalism

• name : String

  The name of the action.

• pre : VarSet n

  The preconditions of the action.

• add : VarSet n

  The adding effects of the action.

• del : VarSet n

  The deleting effects of the action.

• cost : ℕ

  The cost of the action.

def STRIPS.instDecidableEqAction.decEq {n✝ : ℕ} (x✝ x✝¹ : Action n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance STRIPS.instDecidableEqAction {n✝ : ℕ} : DecidableEq (Action n✝)

Equations

• STRIPS.instDecidableEqAction = STRIPS.instDecidableEqAction.decEq

@[implicit_reducible]

instance STRIPS.instToFormatAction {n : ℕ} : Std.ToFormat (Action n)

Equations

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

@[implicit_reducible]

instance STRIPS.instToStringAction {n : ℕ} : ToString (Action n)

Equations

• STRIPS.instToStringAction = { toString := fun (a : STRIPS.Action n) => (Std.format a).pretty }

@[reducible, inline]

abbrev STRIPS.Actions (n : ℕ) : Type

A set of actions

Equations

• STRIPS.Actions n = Set (STRIPS.Action n)

Applicability and successor states

@[reducible, inline]

abbrev STRIPS.Applicable {n : ℕ} (s : State n) (a : Action n) : Prop

An action is applicable in a state if all its preconditions are true in the state.

Equations

• STRIPS.Applicable s a = (↑a.pre ⊆ s)

@[reducible, inline]

abbrev STRIPS.Successor {n : ℕ} (a : Action n) (s s' : State n) : Prop

If an action a is applicable in a state s, then s[a] := (s \ a.del) ∪ a.add is the successor of s.

Equations

• STRIPS.Successor a s s' = (STRIPS.Applicable s a ∧ s' = s \ ↑a.del ∪ ↑a.add)

STRIPS planning problems

structure STRIPS.PlanningTask (n : ℕ) : Type

A planning problem in the STRIPS formalism. The variables of the planning task are all elements of Fin n. Note that most fields have two version:

• an primed version which uses a representation that is efficient at run-time, and
• an unprimed version which is more suited for theoretical results

• varNames : Vector String n

  The names of the variables.

• actions' : List (Action n)

  The actions of the planning task. See PlanningTask.actions for the version using Actions.

• init' : VarSet n

  The initial state of the planning task. See PlanningTask.init for the version using State.

• goal' : VarSet n

  The goal of the planning task, indicating which variables need to be true in a goal state. See also PlanningTask.GoalState and PlanningTask.goalStates.

@[implicit_reducible]

instance STRIPS.PlanningTask.instToFormat {n : ℕ} : Std.ToFormat (PlanningTask n)

Equations

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

@[implicit_reducible]

instance STRIPS.PlanningTask.instToString {n : ℕ} : ToString (PlanningTask n)

Equations

• STRIPS.PlanningTask.instToString = { toString := fun (pt : STRIPS.PlanningTask n) => (Std.format pt).pretty }

def STRIPS.PlanningTask.actions {n : ℕ} (pt : PlanningTask n) : Actions n

The set of actions of the planning task.

Equations

• pt.actions = ↑pt.actions'.toFinset

theorem STRIPS.PlanningTask.mem_actions' {n : ℕ} {pt : PlanningTask n} {a : Action n} : a ∈ pt.actions' ↔ a ∈ pt.actions

def STRIPS.PlanningTask.init {n : ℕ} (pt : PlanningTask n) : State n

The initial state of the planning task.

Equations

• pt.init = ↑pt.init'

theorem STRIPS.PlanningTask.mem_init' {n : ℕ} {pt : PlanningTask n} {i : Fin n} : i ∈ pt.init' ↔ i ∈ pt.init

def STRIPS.PlanningTask.GoalState {n : ℕ} (pt : PlanningTask n) (s : State n) : Prop

A state is a goal state if it contains all goal variables.

Equations

• pt.GoalState s = (↑pt.goal' ⊆ s)

def STRIPS.PlanningTask.goalStates {n : ℕ} (pt : PlanningTask n) : States n

The set of all goal states of the given planning task.

Equations

• pt.goalStates = {s : STRIPS.State n | pt.GoalState s}

theorem STRIPS.PlanningTask.mem_goalStates {n : ℕ} {pt : PlanningTask n} {s : State n} : s ∈ pt.goalStates ↔ pt.GoalState s

Path

inductive STRIPS.PlanningTask.Path {n : ℕ} (pt : PlanningTask n) : State n → State n → Type

Given a STRIPS planning task pt, Path s1 s2 is a path form the state s1 to the state s2 in the state space of pt.

• empty {n : ℕ} {pt : PlanningTask n} (s : State n) : pt.Path s s

  The empty path consisting of a single node s.

• cons {n : ℕ} {pt : PlanningTask n} (a : Action n) {s1 : State n} (s2 : State n) {s3 : State n} (ha : a ∈ pt.actions) (succ : Successor a s1 s2) (π : pt.Path s2 s3) : pt.Path s1 s3

  The path consisting of the node s, and the path π, where s[a] is the first node of π.

snoc

def STRIPS.PlanningTask.Path.snoc {n : ℕ} {pt : PlanningTask n} (a : Action n) {s1 : State n} (s2 : State n) {s3 : State n} (ha : a ∈ pt.actions) (π : pt.Path s1 s2) (succ : Successor a s2 s3) : pt.Path s1 s3

In Path.cons, paths are expanded by adding states at the front of the path (leaving the last state unchanged). Path.snoc allows to extend the path at the back, leaving the first state unchanged. The name snoc comes from reading cons in reverse order.

Equations

• STRIPS.PlanningTask.Path.snoc a s2 ha (STRIPS.PlanningTask.Path.empty s2) succ = STRIPS.PlanningTask.Path.cons a s3 ha succ (STRIPS.PlanningTask.Path.empty s3)
• STRIPS.PlanningTask.Path.snoc a s2 ha (STRIPS.PlanningTask.Path.cons a' s4 ha' succ' π') succ = STRIPS.PlanningTask.Path.cons a' s4 ha' succ' (STRIPS.PlanningTask.Path.snoc a s2 ha π' succ)

def STRIPS.PlanningTask.Path.length {n : ℕ} {pt : PlanningTask n} {s s' : State n} : pt.Path s s' → ℕ

The length of a path.

Equations

• (STRIPS.PlanningTask.Path.empty s).length = 0
• (STRIPS.PlanningTask.Path.cons a s2 ha succ π).length = π.length + 1

@[simp]

theorem STRIPS.PlanningTask.Path.length_snoc {n : ℕ} {pt : PlanningTask n} {a : Action n} {s1 s2 s3 : State n} {ha : a ∈ pt.actions} {π : pt.Path s1 s2} {succ : Successor a s2 s3} : (snoc a s2 ha π succ).length = π.length + 1

theorem STRIPS.PlanningTask.Path.cons_to_snoc {n : ℕ} {pt : PlanningTask n} {a : Action n} {s1 s2 s3 : State n} (ha : a ∈ pt.actions) (succ : Successor a s1 s2) (π : pt.Path s2 s3) : ∃ (s2' : State n), ∃ (a' : Action n), ∃ (ha' : a' ∈ pt.actions), ∃ (π' : pt.Path s1 s2'), ∃ (succ' : Successor a' s2' s3), cons a s2 ha succ π = snoc a' s2' ha' π' succ' ∧ π.length = π'.length

Convert Path.cons, where we have access to the first action and the second state of the path, to Path.snoc, where we have access to the last action and the second to last state of the path.

theorem STRIPS.PlanningTask.Path.snocCases {n : ℕ} {pt : PlanningTask n} {motive : (s s' : State n) → pt.Path s s' → Prop} {s s' : State n} (π : pt.Path s s') (empty : ∀ (s : State n), motive s s (empty s)) (snoc : ∀ (a : Action n) {s1 : State n} (s2 : State n) {s3 : State n} (ha : a ∈ pt.actions) (π' : pt.Path s1 s2) (succ : Successor a s2 s3), motive s1 s3 (snoc a s2 ha π' succ)) : motive s s' π

Allows to perform cases with Path.empty and Path.snoc instead of Path.empty and Path.cons.

Mem

def STRIPS.PlanningTask.Path.Mem {n : ℕ} {pt : PlanningTask n} {s1 s2 : State n} (s : State n) (π : pt.Path s1 s2) : Prop

A state s is a member of a path π if π traverses through s.

Equations

• STRIPS.PlanningTask.Path.Mem s (STRIPS.PlanningTask.Path.empty s2) = (s = s2)
• STRIPS.PlanningTask.Path.Mem s (STRIPS.PlanningTask.Path.cons a s2_3 ha succ π) = (s = s1 ∨ STRIPS.PlanningTask.Path.Mem s π)

@[implicit_reducible]

instance STRIPS.PlanningTask.Path.instMembershipState {n : ℕ} {pt : PlanningTask n} {s1 s2 : State n} : Membership (State n) (pt.Path s1 s2)

Equations

• STRIPS.PlanningTask.Path.instMembershipState = { mem := fun (π : pt.Path s1 s2) (s : STRIPS.State n) => STRIPS.PlanningTask.Path.Mem s π }

@[simp]

theorem STRIPS.PlanningTask.Path.mem_eq {n : ℕ} {pt : PlanningTask n} {s1 s2 : State n} (π : pt.Path s1 s2) (s : State n) : Mem s π = (s ∈ π)

@[simp]

theorem STRIPS.PlanningTask.Path.mem_empty {n : ℕ} {pt : PlanningTask n} {s s' : State n} : s ∈ empty s' ↔ s = s'

@[simp]

theorem STRIPS.PlanningTask.Path.mem_cons {n : ℕ} {pt : PlanningTask n} {a : Action n} {s1 s2 s3 : State n} {ha : a ∈ pt.actions} {succ : Successor a s1 s2} {π : pt.Path s2 s3} {s : State n} : s ∈ cons a s2 ha succ π ↔ s = s1 ∨ s ∈ π

@[simp]

theorem STRIPS.PlanningTask.Path.mem_snoc {n : ℕ} {pt : PlanningTask n} {a : Action n} {s1 s2 s3 : State n} {ha : a ∈ pt.actions} {π : pt.Path s1 s2} {succ : Successor a s2 s3} {s : State n} : s ∈ snoc a s2 ha π succ ↔ s = s3 ∨ s ∈ π

theorem STRIPS.PlanningTask.Path.first_mem {n : ℕ} {pt : PlanningTask n} {s1 s2 : State n} (π : pt.Path s1 s2) : s1 ∈ π

theorem STRIPS.PlanningTask.Path.last_mem {n : ℕ} {pt : PlanningTask n} {s1 s2 : State n} (π : pt.Path s1 s2) : s2 ∈ π

append

def STRIPS.PlanningTask.Path.append {n : ℕ} {pt : PlanningTask n} {s1 s2 s3 : State n} : pt.Path s1 s2 → pt.Path s2 s3 → pt.Path s1 s3

Given a path form a s1 to s2 and a path from s2 to s3, we obtain a path from s1 to s3.

Equations

• (STRIPS.PlanningTask.Path.empty s2).append x✝ = x✝
• (STRIPS.PlanningTask.Path.cons a s2' ha succ π').append x✝ = STRIPS.PlanningTask.Path.cons a s2' ha succ (π'.append x✝)

@[implicit_reducible]

instance STRIPS.PlanningTask.Path.instHAppend {n : ℕ} {pt : PlanningTask n} {s1 s2 s3 : State n} : HAppend (pt.Path s1 s2) (pt.Path s2 s3) (pt.Path s1 s3)

Equations

• STRIPS.PlanningTask.Path.instHAppend = { hAppend := STRIPS.PlanningTask.Path.append }

@[simp]

theorem STRIPS.PlanningTask.Path.append_eq {n : ℕ} {pt : PlanningTask n} {s1 s2 s3 : State n} (π₁ : pt.Path s1 s2) (π₂ : pt.Path s2 s3) : π₁.append π₂ = π₁ ++ π₂

theorem STRIPS.PlanningTask.Path.mem_append {n : ℕ} {pt : PlanningTask n} {s1 s2 s3 : State n} (π₁ : pt.Path s1 s2) (π₂ : pt.Path s2 s3) (s : State n) : s ∈ π₁ ++ π₂ ↔ s ∈ π₁ ∨ s ∈ π₂

split

theorem STRIPS.PlanningTask.Path.split {n : ℕ} {pt : PlanningTask n} {s1 s2 s : State n} (π : pt.Path s1 s2) (h : s ∈ π) : Nonempty (pt.Path s1 s × pt.Path s s2)

If a state s lies on a path π from s1 to s2, then there is a path from the s1 to s and a path from s to s2.

Reachablility, Plans and Unsolvability

@[reducible, inline]

abbrev STRIPS.PlanningTask.Reachable {n : ℕ} (pt : PlanningTask n) (s s' : State n) : Prop

A state s' is reachable from s if there is a path from s to s'. This is the Prop version of Path.

Equations

• pt.Reachable s s' = Nonempty (pt.Path s s')

theorem STRIPS.PlanningTask.reachable_self {n : ℕ} {pt : PlanningTask n} (s : State n) : pt.Reachable s s

structure STRIPS.PlanningTask.Plan {n : ℕ} (pt : PlanningTask n) (s : State n) : Type

A plan for a state s for a planning task pt is a path from s to a goal state of pt.

• last : State n

  The goal state in pt.

• path : pt.Path s self.last

  The path from s to the goal state.

• goal : pt.GoalState self.last

  The proof that last is a goal state.

@[reducible, inline]

abbrev STRIPS.PlanningTask.UnsolvableState {n : ℕ} (pt : PlanningTask n) (s : State n) : Prop

A state is unsolvable if there is no plan for that state.

Equations

• pt.UnsolvableState s = IsEmpty (pt.Plan s)

@[reducible, inline]

abbrev STRIPS.PlanningTask.Unsolvable {n : ℕ} (pt : PlanningTask n) : Prop

A planning task is unsolvable if the initial state is unsolvable.

Equations

• pt.Unsolvable = pt.UnsolvableState pt.init

progression and regression

def STRIPS.progression' {n : ℕ} (S : States n) (a : Action n) : States n

The progression of a set of states S by an action a.

Equations

• STRIPS.progression' S a = {s : STRIPS.State n | ∃ (s' : STRIPS.State n), s' ∈ S ∧ STRIPS.Successor a s' s}

def STRIPS.progression {n : ℕ} (S : States n) (A : Actions n) : States n

The progression of a set of states S by a set of actions A.

Equations

• STRIPS.progression S A = {s : STRIPS.State n | ∃ (a : STRIPS.Action n), a ∈ A ∧ s ∈ STRIPS.progression' S a}

def STRIPS.regression' {n : ℕ} (S : States n) (a : Action n) : States n

The regression of a set of states S by an action a.

Equations

• STRIPS.regression' S a = {s : STRIPS.State n | ∃ (s' : STRIPS.State n), s' ∈ S ∧ STRIPS.Successor a s s'}

def STRIPS.regression {n : ℕ} (S : States n) (A : Actions n) : States n

The regression of a set of states S by a set of actions A.

Equations

• STRIPS.regression S A = {s : STRIPS.State n | ∃ (a : STRIPS.Action n), a ∈ A ∧ s ∈ STRIPS.regression' S a}

theorem STRIPS.mem_progression' {n : ℕ} {a : Action n} {S : States n} (s : State n) : s ∈ progression' S a ↔ ∃ (s' : State n), s' ∈ S ∧ Successor a s' s

theorem STRIPS.mem_progression {n : ℕ} {A : Actions n} {S : States n} (s : State n) : s ∈ progression S A ↔ ∃ (a : Action n), a ∈ A ∧ ∃ (s' : State n), s' ∈ S ∧ Successor a s' s

theorem STRIPS.mem_progression_of_successor {n : ℕ} {S : States n} {s s' : State n} {A : Actions n} {a : Action n} (hs : s ∈ S) (ha : a ∈ A) (h : Successor a s s') : s' ∈ progression S A

theorem STRIPS.progression_union_states {n : ℕ} {S1 S2 : States n} {A : Actions n} : progression (S1 ∪ S2) A = progression S1 A ∪ progression S2 A

theorem STRIPS.progression_union_actions {n : ℕ} {S : States n} {A1 A2 : Actions n} : progression S (A1 ∪ A2) = progression S A1 ∪ progression S A2

theorem STRIPS.progression_monotone_states {n : ℕ} {A : Actions n} : Monotone fun (x : States n) => progression x A

theorem STRIPS.progression_monotone_actions {n : ℕ} {S : States n} : Monotone (progression S)

theorem STRIPS.mem_regression' {n : ℕ} {S : States n} {a : Action n} (s : State n) : s ∈ regression' S a ↔ ∃ (s' : State n), s' ∈ S ∧ Successor a s s'

theorem STRIPS.mem_regression {n : ℕ} {S : States n} {A : Actions n} (s : State n) : s ∈ regression S A ↔ ∃ (a : Action n), a ∈ A ∧ ∃ (s' : State n), s' ∈ S ∧ Successor a s s'

theorem STRIPS.mem_regression_of_successor {n : ℕ} {S : States n} {s s' : State n} {A : Actions n} {a : Action n} (hs : s ∈ S) (ha : a ∈ A) (h : Successor a s' s) : s' ∈ regression S A

theorem STRIPS.sub_progression_iff_sub_regression {n : ℕ} {S S' : States n} {A : Actions n} : progression S A ⊆ S' ↔ regression S'ᶜ A ⊆ Sᶜ