Fail to show termination

Stream: new members

[Richard Copley]

Can you tell me what I'm doing wrong here? I expected fprod (k + 1) to be able to use fprod k without any fuss.

import Mathlib.Data.Finsupp.Basic

-- For all vectors `f : Fin k → (κ →₀ R)` of finitely-supported functions on $$κ$$, there
-- is a single finitely-supported function on $$κᵏ$$, `fprod k f : (Fin k → κ) →₀ R`,
-- such that `fprod k f v = List.prod <| .ofFn fun i => x i (v i)` for all `v` in $$κᵏ$$.
def fprod {κ R} [DecidableEq κ] [MonoidWithZero R] [Nontrivial R] [NoZeroDivisors R]
    (k : ℕ) (f : Fin k -> κ →₀ R) : (Fin k → κ) →₀ R :=
  match k with
  | 0 => {
      toFun := fun _ => 1
      support := {fun.}
      mem_support_toFun := fun _ => ⟨fun _ => one_ne_zero,
        fun _ => Finset.mem_singleton.mpr (Subsingleton.allEq _ _)⟩
    }
  | (m + 1) => {
      toFun := fun p => f 0 (p 0) * fprod m (Fin.tail f) (Fin.tail p)
      support := (f 0).support.biUnion fun i =>
        (fprod m (Fin.tail f)).support.map ⟨Fin.cons i, Fin.cons_right_injective _⟩
      mem_support_toFun := fun i =>
        ⟨fun h => by
          obtain ⟨h, hj, htail⟩ := Finset.mem_biUnion.mp h
          obtain ⟨a, ha, rfl⟩ := Finset.mem_map.mp htail
          dsimp only [Function.Embedding.coeFn_mk]
          rw [Fin.cons_zero, Fin.tail_cons, ne_eq, mul_eq_zero, not_or]
          exact ⟨Finsupp.mem_support_iff.mp hj, Finsupp.mem_support_iff.mp ha⟩,
        fun h =>
          have ⟨hhead, htail⟩ := mul_ne_zero_iff.mp h
          Finset.mem_biUnion.mpr ⟨i 0, Finsupp.mem_support_iff.mpr hhead,
            Finset.mem_map.mpr ⟨Fin.tail i, Finsupp.mem_support_iff.mpr htail,
              Fin.cons_self_tail i⟩⟩⟩
    }

The error is

fail to show termination for
  fprod
with errors
argument #7 was not used for structural recursion
  unexpected occurrence of recursive application
    @fprod

structural recursion cannot be used

and the remaining goal is just

⊢ k < Nat.succ m

[Matt Diamond]

here's one solution:

import Mathlib.Data.Finsupp.Basic

-- For all vectors `f : Fin k → (κ →₀ R)` of finitely-supported functions on $$κ$$, there
-- is a single finitely-supported function on $$κᵏ$$, `fprod k f : (Fin k → κ) →₀ R`,
-- such that `fprod k f v = List.prod <| .ofFn fun i => x i (v i)` for all `v` in $$κᵏ$$.
def fprod {κ R} [DecidableEq κ] [MonoidWithZero R] [Nontrivial R] [NoZeroDivisors R]
    (k : ℕ) (f : Fin k -> κ →₀ R) : (Fin k → κ) →₀ R :=
  match k with
  | 0 => {
      toFun := fun _ => 1
      support := {fun.}
      mem_support_toFun := fun _ => ⟨fun _ => one_ne_zero,
        fun _ => Finset.mem_singleton.mpr (Subsingleton.allEq _ _)⟩
    }
  | (m + 1) =>
    let f' := fprod m (Fin.tail f)
    {
      toFun := fun p => f 0 (p 0) * f' (Fin.tail p)
      support := (f 0).support.biUnion fun i =>
        (fprod m (Fin.tail f)).support.map ⟨Fin.cons i, Fin.cons_right_injective _⟩
      mem_support_toFun := fun i =>
        ⟨fun h => by
          obtain ⟨h, hj, htail⟩ := Finset.mem_biUnion.mp h
          obtain ⟨a, ha, rfl⟩ := Finset.mem_map.mp htail
          dsimp only [Function.Embedding.coeFn_mk]
          rw [Fin.cons_zero, Fin.tail_cons, ne_eq, mul_eq_zero, not_or]
          exact ⟨Finsupp.mem_support_iff.mp hj, Finsupp.mem_support_iff.mp ha⟩,
        fun h =>
          have ⟨hhead, htail⟩ := mul_ne_zero_iff.mp h
          Finset.mem_biUnion.mpr ⟨i 0, Finsupp.mem_support_iff.mpr hhead,
            Finset.mem_map.mpr ⟨Fin.tail i, Finsupp.mem_support_iff.mpr htail,
              Fin.cons_self_tail i⟩⟩⟩
    }

[Matt Diamond]

strangely it doesn't require replacing the 2nd instance of fprod m (Fin.tail f), though you can certainly do that for the sake of consistency

[Richard Copley]

How mysterious! Thank you very much.

(Here is a diff:)

--- mwe.lean    2024-02-11 19:41:39 +0000
+++ fixed.lean  2024-02-11 19:41:39 +0000
@@ -12,8 +12,10 @@
       mem_support_toFun := fun _ => ⟨fun _ => one_ne_zero,
         fun _ => Finset.mem_singleton.mpr (Subsingleton.allEq _ _)⟩
     }
-  | (m + 1) => {
-      toFun := fun p => f 0 (p 0) * fprod m (Fin.tail f) (Fin.tail p)
+  | (m + 1) =>
+    let f' := fprod m (Fin.tail f)
+    {
+      toFun := fun p => f 0 (p 0) * f' (Fin.tail p)
       support := (f 0).support.biUnion fun i =>
         (fprod m (Fin.tail f)).support.map ⟨Fin.cons i, Fin.cons_right_injective _⟩
       mem_support_toFun := fun i =>