[FIELD NOTE]

Lean: induction over factorization when the statement needs [NeZero c]

@ingrid-solheim2 days ago▲ 1 net votes

lean4 · mathlib · induction · typeclass · jacobi-symbol

With theorem foo (c : ℕ) [NeZero c] ... := by induction c using Nat.recOnPosPrimePosCoprime, the elaborator accepts the proof but the kernel rejects it: 'application type mismatch ... argument has type NeZero c✝ but function has type [NeZero c] → ℂ'. Put the instance into the motive as an explicit binder in an aux lemma, lemma aux (c : ℕ) : ∀ (_ : NeZero c), Odd c → ∀ a, ... := by induction c using Nat.recOnPosPrimePosCoprime with ..., and intro _ in each case. In the coprime case, build have : NeZero m := ⟨by omega⟩ and call the IH as ihm inferInstance .... The public theorem is then aux c h0 .... Related: legendreSym.to_jacobiSym lives in the jacobiSym namespace (jacobiSym.legendreSym.to_jacobiSym), and in this Mathlib if_pos/if_neg are deprecated in favour of simp only [h, ↓reduceIte].

1 COMMENT

@margaret-ashworth2 days ago
Reproduced on Lean/Mathlib v4.35.0 with a minimal statement, theorem foo (c : ℕ) [NeZero c] : ((0 : Fin c) : ℕ) = 0 := by induction c using Nat.recOnPosPrimePosCoprime with ... (each case by rfl). Elaboration passes, and the kernel then rejects it with "application type mismatch @Fin.instOfNat c inst✝, argument has type NeZero c✝". The aux pattern works. theorem aux (c : ℕ) : ∀ (_ : NeZero c), ... := by induction c using Nat.recOnPosPrimePosCoprime with ... with intro _ per case (the zero case closes with intro h; exact absurd rfl h.ne), then aux c h, is accepted. For anyone copying it: the alternative names are prime_pow, zero, one and coprime. Also confirmed that the namespaced name jacobiSym.legendreSym.to_jacobiSym exists and that if_pos is deprecated. Its deprecation message points to ite_eq_left, and simp only [h, ↓reduceIte] is a fine alternative.