Marginis

/- We formally verify the method known as recursive backtracking for a monotone predicate P and another predicate Q at the leaves. -/

A vector of length L monus k, thought of as a possible suffix for a word of length L in which the first k bits are unspecified For example, a Gap 10 10 has length 10 - 10.

[This is a rewrite to replace by induction by match with.]

structure MonoPred (b : ℕ) : Type

A predicate P preserved under suffixes, with an optional condition Q at the leaves.

• P : List (Fin b) → Prop

  The predicate to be checked recursively.

• preserved_under_suffixes (u v : List (Fin b)) : u <:+ v → self.P v → self.P u
• Q (l : List (Fin b)) : Prop

  The optional predicate at the leaves.

structure MonoPred_unverified (b : ℕ) : Type

A predicate P with an optional condition Q at the leaves.

• P : List (Fin b) → Prop

  The predicate to be checked (recursively if it is monotone).

• Q : List (Fin b) → Prop

  The optional predicate at the leaves.

def Gap (b L k : ℕ) : Type

A List.Vector k entries away from full length L.

Equations

• Gap b L k = List.Vector (Fin b) (L - k)

def Gap_cons {n L b : ℕ} (a : Fin b) (w : Gap b L.succ n.succ) (h : ¬n ≥ L.succ) : Gap b L.succ n

Note that Gap_cons requires the use of L.succ instead of just L.

Equations

• Gap_cons a w h = ⟨a :: ↑w, ⋯⟩

def Gap_nil {k b L : ℕ} (h : k ≥ L) : Gap b L k

The empty "gap", with possible length overflow.

Equations

• Gap_nil h = ⟨[], ⋯⟩

def Gap_nil' (b n : ℕ) : Gap b n n

The empty "gap".

Equations

• Gap_nil' b n = ⟨[], ⋯⟩

def num_by_backtracking {k b L : ℕ} (P Q : List (Fin b) → Prop) [DecidablePred P] [DecidablePred Q] (w : Gap b L.succ k) : ℕ

The number of strings satisfying P ∧ Q, where P is a monotone predicate and Q is a predicate at the leaves.

Equations

• One or more equations did not get rendered due to their size.
• num_by_backtracking P Q w_2 = if P ↑w_2 ∧ Q ↑w_2 then 1 else 0

theorem cons_suffix {b L n_1 : ℕ} {a : Fin b} (h : ¬n_1 ≥ L.succ) (w : List.Vector (Fin b) (L.succ - n_1.succ)) : ↑w <:+ ↑(Gap_cons a w h)

The list w is a suffix of a :: w, in the setting of the Gap types.

theorem still_holds {b L z : ℕ} {M : MonoPred b} {w : Gap b L.succ z.succ} {h : ¬z ≥ L.succ} {a : Fin b} (H : M.P ↑(Gap_cons a w h)) : M.P ↑w

Preservation under suffices for M.P, for the Gap types.

theorem if_replicate {b : ℕ} (P : Fin b → Prop) (c : Fin b → ℕ) [DecidablePred P] (h : ∀ (a : Fin b), ¬P a) : (List.ofFn fun (a : Fin b) => if P a then c a else 0) = List.replicate b 0

Simplifying a list defined by a vacuous ite.

theorem if_replicate₀ {b L : ℕ} {M : MonoPred b} [DecidablePred M.P] [DecidablePred M.Q] {w : Gap b L.succ (Nat.succ 0)} (H : ¬M.P ↑w) : (List.ofFn fun (a : Fin b) => if M.P ↑(Gap_cons a w ⋯) ∧ M.Q ↑(Gap_cons a w ⋯) then 1 else 0) = List.replicate b 0

Simplifying a gap defined by a vacuous ite.

theorem if_replicate₁ {b L : ℕ} {M : MonoPred b} [DecidablePred M.P] [DecidablePred M.Q] {n_1 : ℕ} (hnL : ¬n_1 + 1 ≥ L.succ) {w : Gap b L.succ (n_1 + 1).succ} (H : ¬M.P ↑w) : (List.ofFn fun (a : Fin b) => if M.P ↑(Gap_cons a w hnL) then if h : n_1 ≥ L.succ then num_by_backtracking M.P M.Q (Gap_nil h) else (List.ofFn fun (a_1 : Fin b) => num_by_backtracking M.P M.Q (Gap_cons a_1 (Gap_cons a w hnL) h)).sum else 0) = List.replicate b 0

Simplifying a gap defined by a vacuous ite involving num_by_backtracking.

theorem branch_out {b n L : ℕ} (M : MonoPred b) [DecidablePred M.P] [DecidablePred M.Q] (hnL : ¬n ≥ L.succ) (w : Gap b L.succ n.succ) : num_by_backtracking M.P M.Q w = (List.ofFn fun (a : Fin b) => num_by_backtracking M.P M.Q (Gap_cons a w hnL)).sum

Writing num_by_backtracking as a sum of values of itself.

theorem subtype_ext {α : Type} (P Q : α → Prop) (h : ∀ (x : α), P x ↔ Q x) : { x : α // P x } = { x : α // Q x }

Subtype extensionality.

theorem fincard_ext {α : Type} {P Q : α → Prop} (h : ∀ (x : α), P x ↔ Q x) [Fintype { x : α // P x }] [Fintype { x : α // Q x }] : Fintype.card { x : α // P x } = Fintype.card { x : α // Q x }

Fintype.card extensionality.

theorem Vector_eq_of_suffix_of_length_eq {L b : ℕ} {w v : List.Vector (Fin b) L} (hv : ↑w <:+ ↑v) : ↑w = ↑v

Two vectors are equal if they have the same length and one is a suffix of the other.

theorem disjoint_branch'' {L b n : ℕ} {M : MonoPred b} (w : List.Vector (Fin b) (L.succ - n.succ)) (h : ¬n ≥ L.succ) {i j : Fin b} (hp : i ≠ j) : Disjoint (fun (v : List.Vector (Fin b) L.succ) => (M.P ↑v ∧ M.Q ↑v) ∧ ↑(Gap_cons i w h) <:+ ↑v) fun (v : List.Vector (Fin b) L.succ) => (M.P ↑v ∧ M.Q ↑v) ∧ ↑(Gap_cons j w h) <:+ ↑v

If i≠j then i::w and j::w can't be suffixes of the same vector v.

theorem list_get_ne_nil {α : Type} {x y t : List α} (ht : t ++ x = y) (hl : x.length < y.length) : t ≠ []

If y = t ++ x and y is longer than x then t is nonempty.

theorem Vector_append_succ_ne_nil {L n b : ℕ} {w : List.Vector (Fin b) (L.succ - n.succ)} {v : List.Vector (Fin b) L.succ} {t : List (Fin b)} (ht : t ++ ↑w = ↑v) : t ≠ []

For vectors t,y,x, if y = t ++ x and y is longer than x then t is nonempty.

theorem List_reverse_ne_nil {α : Type} {t : List α} (hlong : t ≠ []) : t.reverse ≠ []

The reverse of a nonempty list is also nonempty.

theorem List_reverse_cons {α : Type} {s t : List α} {a : α} (hs : t.reverse = a :: s) : t = s.reverse ++ [a]

Reversing a list constructor.

theorem prefix_of_same {L b : ℕ} (w : List.Vector (Fin b) L) (x y : { v : List.Vector (Fin b) L // ↑w <:+ ↑v }) : ↑x = ↑y

If x and y have w as a prefix and are of the same length as w, then x=y.

theorem list_sum_ofFn_succ {n : ℕ} (f : Fin n.succ → ℕ) : (List.ofFn fun (i : Fin n.succ) => f i).sum = (List.ofFn fun (i : Fin n) => f ⟨↑i, ⋯⟩).sum + f (Fin.last n)

The sum of a list of values of a function.

theorem disjoint_from_last {α : Type} {n_1 : ℕ} {p : Fin n_1.succ → α → Prop} (h : ∀ (i j : Fin n_1.succ), i ≠ j → Disjoint (p i) (p j)) : Disjoint (fun (x : α) => ∃ (i : Fin n_1), p i.castSucc x) fun (x : α) => p ⟨n_1, ⋯⟩ x

If a sequence of n+1 sets are pairwise disjoint, then the union of the first n is disjoint from the last set.

theorem distinguish_from_last {α : Type} {n_1 : ℕ} {p : Fin n_1.succ → α → Prop} (x : α) : (∃ (i : Fin n_1), p i.castSucc x) ∨ p ⟨n_1, ⋯⟩ x ↔ ∃ (i : Fin n_1.succ), p i x

One of the propositions p_0,...,p_n holds iff either the or statement of the first n holds, or p_n holds.

theorem Fintype_card_subtype_of_disjoint {α : Type} [Fintype α] {n : ℕ} (p : Fin n → α → Prop) [Fintype { x : α // ∃ (i : Fin n), p i x }] [(i : Fin n) → Fintype { x : α // p i x }] (h : ∀ (i j : Fin n), i ≠ j → Disjoint (p i) (p j)) : (List.ofFn fun (i : Fin n) => Fintype.card { x : α // p i x }).sum = Fintype.card { x : α // ∃ (i : Fin n), p i x }

If some sets are disjoint, then the cardinality of their union is the sum of their cardinalities.

theorem get_union {α : Type} {x y : List α} (h : x <:+ y) (hl : x.length < y.length) : ∃ (a : α), a :: x <:+ y

If x is a proper suffix of y then some a :: x is a suffix of y.

theorem suffix_cons {b L n : ℕ} (w : Gap b L.succ n.succ) (v : Gap b L.succ 0) : ↑w <:+ ↑v ↔ ∃ (a : Fin b), a :: ↑w <:+ ↑v

If x is a proper suffix of y then some a :: x is a suffix of y, and vice versa.

theorem backtracking_verification {k b L : ℕ} (bound : k ≤ L.succ) (M : MonoPred b) [DecidablePred M.P] [DecidablePred M.Q] (w : List.Vector (Fin b) (L.succ - k)) : Fintype.card { v : List.Vector (Fin b) L.succ // (M.P ↑v ∧ M.Q ↑v) ∧ ↑w <:+ ↑v } = num_by_backtracking M.P M.Q w

Verifies recursive backtracking for b-ary trees with monotone predicates P, with a non-monotone Q at the leaves.

@[implicit_reducible]

instance instDecidableEqGapSuccOfNatNat {b L : ℕ} : DecidableEq (Gap b L.succ 0)

Gap has decidable equality.

Equations

• instDecidableEqGapSuccOfNatNat = Subtype.instDecidableEq

def satisfy_and_have_suffix {k b L : ℕ} (P : List (Fin b) → Prop) [DecidablePred P] (Q : List (Fin b) → Prop) [DecidablePred Q] (w : Gap b L.succ k) : Finset (Gap b L.succ 0)

The lists with a given suffix satisfying conditions P (recursively) and Q.

Equations

• One or more equations did not get rendered due to their size.
• satisfy_and_have_suffix P Q w_2 = if P ↑w_2 ∧ Q ↑w_2 then {w_2} else ∅

theorem branch_out_set (b : ℕ) {n L : ℕ} {M : MonoPred b} [DecidablePred M.P] [DecidablePred M.Q] (hnL : ¬n ≥ L.succ) (w : Gap b L.succ n.succ) : satisfy_and_have_suffix M.P M.Q w = Finset.univ.biUnion fun (a : Fin b) => satisfy_and_have_suffix M.P M.Q (Gap_cons a w hnL)

those_with_suffix as a union of its own values.

@[implicit_reducible]

instance instFintypeGapSuccOfNatNat {b L : ℕ} : Fintype (Gap b L.succ 0)

Gap is a fintype.

Equations

• instFintypeGapSuccOfNatNat = id List.Vector.instFintype

theorem filter_suffix_empty {b L : ℕ} {P Q : List (Fin b) → Prop} [DecidablePred P] [DecidablePred Q] {w : Gap b L.succ 0} (holds : ¬(P ↑w ∧ Q ↑w)) : {v : Gap b L.succ 0 | P ↑v ∧ Q ↑v ∧ ↑w <:+ ↑v} = ∅

If w has full length and doesn't satisfy P ∧ Q, then none of its extensions (of the same length) do either.

theorem filter_suffix_singleton {b L : ℕ} {P Q : List (Fin b) → Prop} [DecidablePred P] [DecidablePred Q] {w : Gap b L.succ 0} (holds : P ↑w ∧ Q ↑w) : {w} = {v : Gap b L.succ 0 | P ↑v ∧ Q ↑v ∧ ↑w <:+ ↑v}

If w satisfies a predicate then the set of its extensions of the same length that do the same is {w}.

theorem verify_those_with_suffix {k b L : ℕ} (bound : k ≤ L.succ) {M : MonoPred b} [DecidablePred M.P] [DecidablePred M.Q] (w : Gap b L.succ k) : satisfy_and_have_suffix M.P M.Q w = {v : Gap b L.succ 0 | M.P ↑v ∧ M.Q ↑v ∧ ↑w <:+ ↑v}

satisfy_and_have_suffix is as advertised.