Questions about "computable" definitions

Stream: new members

[Vivek Rajesh Joshi]

I have defined this function here to identify a nonzero element of a tuple (it may seem unnecessarily complicated, but that's because it is part of a larger context) :

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

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

@[simp] def Fin.allZero {F : Type} [Field F] [DecidableEq F] (v : Fin m → F) : Prop := ∀ (i : Fin m), v i = 0

section
variable (v : Fin m → F)
instance : Decidable (Fin.allZero v) :=
  inferInstanceAs <| Decidable (∀ (i : Fin m), v i = 0)
end

theorem Fin.allZero_head_tail {F : Type} [Field F] [DecidableEq F] (v : Fin (m+1) → F) : Fin.allZero v ↔ v 0 = 0 ∧ Fin.allZero (Fin.tail v) := by sorry

def Fin.allZero_not_ex_nonzero {F : Type} [Field F] [DecidableEq F] {v : Fin (m+1) → F} :
  (¬ Fin.allZero v) → {i : Fin (m+1) // v i ≠ 0} := by
  intro hv
  induction m with
  | zero =>
    rw [allZero_head_tail] at hv
    simp at hv
    exact ⟨0,hv⟩
  | succ n ih =>
    rw [allZero_head_tail] at hv
    push_neg at hv
    by_cases h1 : v 0 = 0
    · apply hv at h1
      apply ih at h1
      exact ⟨h1.1.succ,h1.2⟩
    · exact ⟨0,h1⟩

def v1 := ![0,0,6,(4:Rat)]

lemma hv1 : (¬ Fin.allZero v1) := by decide
#eval Fin.allZero_not_ex_nonzero hv1

1. I know it's bad practice to code functions in tactic mode, but I couldn't use Nat.rec ... m directly because it wasn't replacing m with 0 in the base case.

def Fin.allZero_not_ex_nonzero {F : Type} [Field F] [DecidableEq F] {v : Fin (m+1) → F} :
  (¬ Fin.allZero v) → {i : Fin (m+1) // v i ≠ 0} :=
  fun hv => (Nat.rec (⟨0,by rw [allZero_head_tail] at hv; simp at hv⟩) (sorry) m)

Can anyone tell me how to fix this, or if there's an easier way to perform induction on m without using tactic mode?

2. The function seems to work perfectly despite having used tactic mode and classical logic (the by_cases tactic). Why is that so?

[Andrés Goens]

I'll start with 2.: yep! classical logic dosen't mean uncomputable in general :wink: more concretely, the devs have made a really nice work of producing computable code from those, eliminating them. A good rule of thumb is that when calls to choice or excluded middle or similar don't matter for the actual computated vaule (just for its type correctness), they will just be eliminated

1. is a bit tricker:

Note that you need to use Nat.recAux if you want to use 0 and +1 notation. How can you find things like these out? I just did

set_option pp.proofs true in
#print Fin.allZero_not_ex_nonzero

which gives:

def Fin.allZero_not_ex_nonzero : {m : ℕ} →
  {F : Type} →
    [inst : Field F] → [inst_1 : DecidableEq F] → {v : Fin (m + 1) → F} → ¬Fin.allZero v → { i // v i ≠ 0 } :=
fun {m} {F} [Field F] [DecidableEq F] {v} hv =>
  Nat.recAux (motive := fun {m} => {v : Fin (m + 1) → F} → ¬Fin.allZero v → { i // v i ≠ 0 })
    (fun {v} hv => ⟨0, Fin.allZero_not_ex_nonzero.proof_2 hv⟩)
    (fun n ih {v} hv =>
      if h1 : v 0 = 0 then
        ⟨(↑(ih (Fin.allZero_not_ex_nonzero.proof_4 n hv h1))).succ, Fin.allZero_not_ex_nonzero.proof_5 n ih hv h1⟩
      else ⟨0, h1⟩)
    m hv

(I didn't start with the pp.proofs option, but if you hover over the elided proof the thumbnail will recommend it). That works, but it's kinda ugly. It also uses auxillary proofs, e.g.

theorem Fin.allZero_not_ex_nonzero.proof_2 : ∀ {F : Type} [inst : Field F] [inst_1 : DecidableEq F]
  {v : Fin (0 + 1) → F}, ¬Fin.allZero v → ¬v 0 = 0 :=
fun {F} [Field F] [DecidableEq F] {v} hv =>
  Eq.mp (congrArg Not (Eq.trans (congrArg (And (v 0 = 0)) Mathlib.Logic.IsEmpty._auxLemma.1) (and_true (v 0 = 0))))
    (Eq.mp (congrArg (fun _a => ¬_a) (propext (Fin.allZero_head_tail v))) hv)

Which is a lot about getting the types to check well. Now, normally you would also want to write this recursion by just using, well, recursion (calling allZero_not_ex_nonzero in the succ case). I don't know why I can't get that to work though...
I've been trying all variations of this:

def Fin.allZero_not_ex_nonzero' {F : Type} [Field F] [DecidableEq F] {v : Fin (m+1) → F} :
  (¬ Fin.allZero v) → {i : Fin (m+1) // v i ≠ 0} :=
  fun hv => match hm : m with
    | 0 =>
      let v0 := hm ▸ v
      let hv0 : v0 0 ≠ 0 := by
        rw [hm] at hv
        rw [allZero_head_tail] at hv
        push_neg at hv
        exact hv
      ⟨0,hv0⟩

But it always seems to give:

application type mismatch
  allZero v
argument
  v
has type
  Fin (m + 1) → F : Type
but is expected to have type
  Fin (0 + 1) → F : Type

It doesn't eliminate the m in the type, even though we're inside the match arm. Interestingly, if you hover over v it does eliminate the m (into 0). I'm puzzled, could this be a bug in the elaborator? I feel like @Henrik Böving could know :)?