Lean not considering a proposition as decidable

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

variable (F : Type) [Field F] [DecidableEq F] [Repr F]

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

structure ReducedRow (n : Nat) where
  z : Option (Fin n)
  k : Nat
  tail : Vector F k
  h : (hz : z = some p) → n = p + k + 1

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

def ReducedRow.toVector (row : ReducedRow F n): Vector F n :=
  match hz:row.z with
  | none => zeroVec F n
  | some p => row.h hz ▸ (zeroVec F p).append (Vector.cons 1 row.tail)

def Vector.concat (a : α) : Vector α n → Vector α (n+1) := fun v => Vector.append v ⟨[a],rfl⟩

abbrev Vector.allZero (v : Vector F n) : Prop := v.toList.all (.=0)

inductive RowReducedEchelonForm : (R : Vector (ReducedRow F n) m) → Prop where
| nil : RowReducedEchelonForm Vector.nil
| cons : (row : ReducedRow F n) → RowReducedEchelonForm R →
         ((row.toVector F).allZero) → RowReducedEchelonForm (R.concat row)

instance : Decidable (RowReducedEchelonForm F R) :=
  R.inductionOn
  (.isTrue (RowReducedEchelonForm.nil))
  (fun _ {row} {l} ih => match ih with
    | isTrue hl =>
      if hr:(∀ r ∈ l, (hz : r.z.isSome) → (row.toVector F).get (r.z.get hz) = 0) then sorry
      else sorry
    | isFalse hl => sorry)

I've got this condition imposed on a row : ReducedRow being added to a vector of ReducedRows (essentially a matrix) which states that wherever all the other ReducedRows of the matrix have a leading one, the new ReducedRow must have a 0. Lean doesn't consider this condition as decidable. Why is that so? How can I make this decidable?

[Vivek Rajesh Joshi]

Oops, sorry, didn't notice that I was typing in this thread. I'll make my own one.

[Notification Bot]

2 messages were moved here from #new members > Defining ℤ in Lean by Vivek Rajesh Joshi.

[Vivek Rajesh Joshi]

Nevermind, figured it out

[Michal Wallace (tangentstorm)]

what was the issue?

[Michal Wallace (tangentstorm)]

(I was trying to diagnose it too, and don't have a good grasp of what Decidable is yet)

[Vivek Rajesh Joshi]

I don't know why Lean couldn't decide on this, but I manually synthesised a decidable instance for lean regarding the proposition:

instance (l : Vector (ReducedRow F n) m) (row : ReducedRow F n) : Decidable ((∀ r ∈ l, (hz : r.z.isSome) → (row.toVector F).get (r.z.get hz) = 0)) :=
  inferInstanceAs <| Decidable (∀ r ∈ l.toList, (hz : r.z.isSome) → (row.toVector F).get (r.z.get hz) = 0)

[Vivek Rajesh Joshi]

I think it's just that Lean is more familiar with List membership than Vector membership, since I've defined vector membership on the fly here. Although I have shown that vector membership is decidable too, so I'm not sure about the exact problem here but this is my best guess

[Anand Rao Tadipatri]

This needs a lemma that shows Lean how to decide whether a property is uniformly true for all elements of a vector, given that it is decidable for any given element. Here is some code to make this work:

import Mathlib.Data.Matrix.Notation

variable (F : Type) [Field F] [DecidableEq F] [Repr F]

abbrev Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

@[simp] def Vector.mem_nil (a : α) : ¬ (a ∈ Vector.nil) := List.not_mem_nil a

@[simp] def Vector.mem_head : a ∈ a ::ᵥ as := by
  show a ∈ Vector.toList _
  simp

@[simp] def Vector.mem_cons : x ∈ a ::ᵥ as ↔ x = a ∨ x ∈ as := List.mem_cons

structure ReducedRow (n : Nat) where
  z : Option (Fin n)
  k : Nat
  tail : Vector F k
  h : (hz : z = some p) → n = p + k + 1

def zeroVec (k: Nat) : Vector F k := Vector.replicate k 0

def ReducedRow.toVector (row : ReducedRow F n): Vector F n :=
  match hz:row.z with
  | none => zeroVec F n
  | some p => row.h hz ▸ (zeroVec F p).append (Vector.cons 1 row.tail)

def Vector.concat (a : α) : Vector α n → Vector α (n+1) := fun v => Vector.append v ⟨[a],rfl⟩

abbrev Vector.allZero (v : Vector F n) : Prop := v.toList.all (.=0)

inductive RowReducedEchelonForm : (R : Vector (ReducedRow F n) m) → Prop where
| nil : RowReducedEchelonForm Vector.nil
| cons : (row : ReducedRow F n) → RowReducedEchelonForm R →
         ((row.toVector F).allZero) → RowReducedEchelonForm (R.concat row)

instance {P : α → Prop} [DecidablePred P] {v : Vector α n} : Decidable (∀ a ∈ v, P a) := by
  induction v
  case nil =>
    apply Decidable.isTrue
    simp
  case cons a as ih =>
    simp
    infer_instance

instance : Decidable (RowReducedEchelonForm F R) :=
  R.inductionOn
  (.isTrue (RowReducedEchelonForm.nil))
  (fun _ {row} {l} ih => match ih with
    | isTrue hl =>
      if hr:(∀ r ∈ l, (hz : r.z.isSome) → (row.toVector F).get (r.z.get hz) = 0) then sorry
      else sorry
    | isFalse hl => sorry)

[Anand Rao Tadipatri]

Note that this also needs some "API lemmas" surrounding the membership relation for vectors.

[Kyle Miller]

Note: you should be very careful defining decidable instances using tactics. A Decidable instance is supposed to be a program that evaluates the truth of a proposition, and it's very easy to make Decidable instances this way that cannot be evaluated by the kernel. This doesn't affect compiled programs, but it can keep the decide tactic from functioning.

[Vivek Rajesh Joshi]

Pretty sure I'm just using proof terms here, not tactics. Unless match ... with is being considered as a tactic. What can I replace it with?

[Kyle Miller]

I'm responding to Anand

[Vivek Rajesh Joshi]

Right, sorry.