decidable instance for list

Stream: lean4

[Jesse Slater]

I have written a function that returns prop, and I want to use it to filter a list. To do that, I trying to write an instance of Decidable for it.

def vecLE {n : ℕ} (v1 v2 : Vector ℕ n) : Prop :=
  Vector.map₂ (· ≤ ·) v1 v2
  |>.toList
  |>.foldl And True

instance decideableVecLE {n : ℕ} (v1 v2 : Vector ℕ n) : Decidable (vecLE v1 v2) :=
  sorry

def getValid {n : ℕ} (v : Vector ℕ n) (l : List (Vector ℕ n)): List (Vector ℕ n) :=
  l.filter (vecLE v · |> Decidable.decide)

I have been having trouble figuring out how to prove that it is decidable.

Is this the right way to be doing this? I know that I could rewrite vecLE to return bool and then I would not have to do this, but I was looking at this, and decided to try to do it with Prop.

If this is the best approach, how can I prove decidableVecLE? If it isn't, what other approach should I use?
This is a MWE so in reality vecLE is slightly more complicated, and getValid is part of a larger function.

Also, any code criticism would be much appreciated. I am self taught, so I always just use the first solution I find in the docs, and never know if I am missing a better solution.

[Eric Wieser]

Presumably you can prove decidability of that relation by induction

[Alex Keizer]

Some comments:

• Definitions of type Prop are generally written in UpperCamelCase, so it should be VecLE,
• Nothing in this construction depends on Nat, consider generalizing to any type with a (decidable) LE instance
• it's probably easier to define a version in terms of List first, and then define VecLE in terms of ListLE

You could use the following as a starting point, just fill in the sorrys:

import Aesop

variable {α} [LE α]

def ListLE (v1 v2 : List α) : Prop :=
  List.zipWith (· ≤ ·) v1 v2
  |>.foldl And True


namespace ListLE
  theorem listLE_nil_left {bs : List α} : ListLE ([]) bs :=
    by trivial

  theorem listLE_nil_right {as : List α} : ListLE as ([]) :=
    by cases as <;> trivial



  theorem not_listLE_succ_of_not_listLE {x1 x2 : α} {v1 v2 : List α} :
      ¬(ListLE v1 v2) → ¬ListLE (x1 :: v1) (x2 :: v2) :=
  by
    sorry

  theorem not_listLE_succ_of_not_le {x1 x2 : α} {v1 v2 : List α} :
      ¬(x1 ≤ x2) → ¬ListLE (x1 :: v1) (x2 :: v2) :=
  by
    intro h₁ h₂; apply h₁; clear h₁
    simp[ListLE] at h₂

    induction v1 generalizing v2
    case nil =>
      apply h₂
    case cons hd1 tl1 ih =>
      cases v2
      case nil => apply h₂
      case cons hd2 tl2 =>
        apply @ih tl2
        simp[List.foldl] at h₂
        suffices ∀ left right tl,
          List.foldl And (left ∧ right) tl → List.foldl And right tl
        from by
          rw[And.comm] at h₂
          apply this _ _ _ h₂

        intro left right tl;
        induction tl generalizing left right
        case nil => intro ⟨_, h⟩; apply h
        case cons hd tl ih =>
          intro h
          simp only [List.foldl] at h |-
          have : ((left ∧ right) ∧ hd) = (left ∧ (right ∧ hd))
            := by aesop
          rw[this] at h; clear this;
          apply ih _ _ h





  theorem listLE_succ {x1 x2 : α} {v1 v2 : List α} :
      x1 ≤ x2 → ListLE v1 v2 → ListLE (x1 :: v1) (x2 :: v2) :=
  by
    intro h₁ h₂
    sorry




  instance decide (as bs : List α) [rel : DecidableRel (@LE.le α _)] : Decidable (ListLE as bs) :=
    match as, bs with
    | [], _           => .isTrue listLE_nil_left
    | _, []           => .isTrue listLE_nil_right
    | a::as, b::bs    => match (rel a b), (decide as bs) with
        | _, .isFalse h           => .isFalse <| not_listLE_succ_of_not_listLE h
        | .isFalse h, _           => .isFalse <| not_listLE_succ_of_not_le h
        | .isTrue h₁, .isTrue h₂  => .isTrue  <| listLE_succ h₁ h₂


end ListLE

[Kyle Miller]

If you change the definition to something that's more mathematical and less procedural, it turns out to be really easy to define this instance:

import Mathlib.Data.Vector.Basic

def VectorLE [LE α] (v1 v2 : Vector α n) : Prop :=
  ∀ i, v1.get i ≤ v2.get i

instance [LE α] [@DecidableRel α (· ≤ ·)] (v1 v2 : Vector α n) : Decidable (VectorLE v1 v2) :=
  inferInstanceAs <| Decidable (∀ _, _)

The key is that there is already a forall decidable instance when it's over Fin n.

I also generalized this to be for an arbitrary type with a decidable LE relation, rather than just Nat.

[Jesse Slater]

Thank you, this is excellent! I guess I am too used to thinking procedurally.