Inductive Certificates

We formalize the simple version of Inductive Certificates for unsolvability of automated planning as introduced in [ERH17] and [Eri19]. This file includes :

• the definition of inductive sets and inductive certificates,
• soundness of inductive certificates, and
• completeness of inductive certificates.
• the construction of the set of reachable states (which is not needed anymore)

Inductive Sets and Inductive Certificates

@[reducible, inline]

abbrev Validator.InductiveSet {n : ℕ} (pt : STRIPS n) (S : States n) : Prop

A set S is inductive if S[pt.actions] ⊆ S.

Equations

• Validator.InductiveSet pt S = (pt.progression S pt.actions ⊆ S)

@[reducible, inline]

abbrev Validator.InductiveCertificateState {n : ℕ} (pt : STRIPS n) (s : State n) (S : States n) : Prop

An inductive certificate for a state s is an inductive set containing s which does not contain any goal state.

Equations

• Validator.InductiveCertificateState pt s S = (s ∈ S ∧ (∀ s ∈ S, ¬pt.GoalState s) ∧ Validator.InductiveSet pt S)

@[reducible, inline]

abbrev Validator.InductiveCertificate {n : ℕ} (pt : STRIPS n) (S : States n) : Prop

An inductive certificate for the a planning task is an inductive certificate for the initial state.

Equations

• Validator.InductiveCertificate pt S = Validator.InductiveCertificateState pt pt.init S

Soundness of Inductive Certificates

theorem Validator.InductiveCertificate.soundness' {n : ℕ} {pt : STRIPS n} {s : State n} {S : States n} : InductiveCertificateState pt s S → UnsolvableState pt s

theorem Validator.InductiveCertificate.soundness {n : ℕ} {pt : STRIPS n} {S : States n} : InductiveCertificate pt S → Unsolvable pt

Inductive certificates are sound, i.e. if an inductive certificate exists, then the planning problem is unsolvable.

Completeness of Inductive Certificates

theorem Validator.InductiveCertificate.completeness' {n : ℕ} {pt : STRIPS n} {s : State n} : UnsolvableState pt s → ∃ (S : States n), InductiveCertificateState pt s S

theorem Validator.InductiveCertificate.completeness {n : ℕ} {pt : STRIPS n} : Unsolvable pt → ∃ (S : States n), InductiveCertificate pt S

Inductive certificates are complete, i.e. if a planning problem is unsolvable, then an inductive certificate for the planning problem exists.

Construction of Reachable States (Unused)

Previously the definition of States used Finset instead of Set. To construct the set of reachable states in completeness', we had to either show that the the predicate Reachable is decidable, or give a construction for the set of all reachable states. As the former is usually done by checking whether a state is in the set of all reachable states, we gave a direct construction.

The following definitions make this construction, but note that all underlying definitions now use Set instead of Finset. The construction is not needed anymore, but maybe it is usefull for someone someday.

def Validator.InductiveCertificate.expand {n : ℕ} (pt : STRIPS n) (S : States n) (k : ℕ) : States n

The k-th expansion of a set of states S contains all states which are reachable from a state in S by a path with length at most k.

Equations

• Validator.InductiveCertificate.expand pt S 0 = S
• Validator.InductiveCertificate.expand pt S k.succ = S ∪ pt.progression (Validator.InductiveCertificate.expand pt S k) pt.actions

theorem Validator.InductiveCertificate.expand_progression {n : ℕ} (pt : STRIPS n) (S : States n) (k : ℕ) : expand pt (pt.progression S pt.actions) k = pt.progression (expand pt S k) pt.actions

theorem Validator.InductiveCertificate.expand_monotone {n : ℕ} (pt : STRIPS n) (S : States n) : Monotone (expand pt S)

theorem Validator.InductiveCertificate.expand_monotone_states {n : ℕ} (pt : STRIPS n) (k : ℕ) : Monotone fun (x : States n) => expand pt x k

noncomputable instance Validator.InductiveCertificate.instFintypeElem {α : Type u_1} [Fintype α] {S : Set α} : Fintype ↑S

A set over a finite type is finite.

Equations

• Validator.InductiveCertificate.instFintypeElem = Fintype.ofFinite ↑S

noncomputable instance Validator.InductiveCertificate.instCompleteLatticeFinsetOfFintypeOfDecidableEq {α : Type u_1} [Fintype α] [DecidableEq α] : CompleteLattice (Finset α)

Finset over a finite type α forms a complete lattice. This uses that Finset α is a finite type, and therefore every set over Finset α is finite, so one can use Finset.inf and Finset.sup.

Equations

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

noncomputable def Validator.InductiveCertificate.reachable_states {n : ℕ} (pt : STRIPS n) (s : State n) : States n

The set of all reachable_states reachable from s can be constructed as the union of expand pt {s} k for all natural numbers k.

Equations

• Validator.InductiveCertificate.reachable_states pt s = ⨆ (k : ℕ), Validator.InductiveCertificate.expand pt {s} k

theorem Validator.InductiveCertificate.exists_eq_iSup_monotone {β : Type} [CompleteLattice β] [WellFoundedGT β] (f : ℕ → β) (hf : Monotone f) : ∃ (n : ℕ), f n = ⨆ (k : ℕ), f k

If f is a monotone function from ℕ to a complete lattice where the relation > is well-founded, then there exists n ∈ ℕ such that the suppremum ⨆ k : ℕ, f k is equal to f n.

This implies that there exists n such that reachable_states pt s is equal to the n-th expansion expand pt {s} n.

theorem Validator.InductiveCertificate.mem_reachable_helper {n : ℕ} {pt : STRIPS n} {s s' : State n} {k : ℕ} (hs' : s' ∈ expand pt {s} k) : Reachable pt s s'

States in the k-th expansion of s are reachable from s.

theorem Validator.InductiveCertificate.mem_reachable {n : ℕ} (pt : STRIPS n) {s s' : State n} : s' ∈ reachable_states pt s ↔ Reachable pt s s'

The members of reachable_states are exactly the states in the state space which are reachable.