Additional definitions for the STRIPS formalism

This file extends Validator.PlanningTask.Core by implementing

• new operations for working with Path,
• definition for reachability of states,
• methods to get all (goal)states of a planning problem,
• definitions of progression and regression,
• lemmas to work with progression and regression.

Path

snoc

def Validator.Path.snoc {n : ℕ} {pt : STRIPS n} (a : Action n) {s1 : State n} (s2 : State n) {s3 : State n} (ha : a ∈ pt.actions) (π : Path pt s1 s2) (succ : Successor a s2 s3) : Path pt 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

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

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

The length of a path.

Equations

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

@[simp]

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

@[irreducible]

theorem Validator.Path.cons_to_snoc {n : ℕ} {pt : STRIPS n} {a : Action n} {s1 s2 s3 : State n} (ha : a ∈ pt.actions) (succ : Successor a s1 s2) (π : Path pt s2 s3) : ∃ (s2' : State n) (a' : Action n) (ha' : a' ∈ pt.actions) (π' : Path pt 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 Validator.Path.snocCases {n : ℕ} {pt : STRIPS n} {motive : (s s' : State n) → Path pt s s' → Prop} {s s' : State n} (π : Path pt 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) (π' : Path pt 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.

append

def Validator.Path.append {n : ℕ} {pt : STRIPS n} {s1 s2 s3 : State n} : Path pt s1 s2 → Path pt s2 s3 → Path pt 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

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

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

Equations

• Validator.Path.instHAppend = { hAppend := Validator.Path.append }

Mem

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

split

@[irreducible]

theorem Validator.Path.split {n : ℕ} {pt : STRIPS n} {s1 s2 s : State n} (π : Path pt s1 s2) (h : s ∈ π) : Nonempty (Path pt s1 s × Path pt 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.

Additional definitions for STRIPS

Reachable

@[reducible, inline]

abbrev Validator.Reachable {n : ℕ} (pt : STRIPS 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

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

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

states and goal_states

def Validator.STRIPS.goal_states {n : ℕ} (pt : STRIPS n) : States n

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

Equations

• pt.goal_states = {s : Validator.State n | pt.GoalState s}

progression and regression

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

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

Equations

• x✝.progression' S a = {s : Validator.State n | ∃ s' ∈ S, Validator.Successor a s' s}

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

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

Equations

• pt.progression S A = {s : Validator.State n | ∃ a ∈ A, s ∈ pt.progression' S a}

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

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

Equations

• x✝.regression' S a = {s : Validator.State n | ∃ s' ∈ S, Validator.Successor a s s'}

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

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

Equations

• pt.regression S A = {s : Validator.State n | ∃ a ∈ A, s ∈ pt.regression' S a}

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

theorem Validator.mem_progression_of_successor {n : ℕ} {pt : STRIPS 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' ∈ pt.progression S A

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

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

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

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

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

theorem Validator.mem_regression_of_successor {n : ℕ} {pt : STRIPS 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' ∈ pt.regression S A

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