reducibly defeq `![x, y, z] n`

Stream: lean4

[Kim Morrison]

Can anyone see a way to improve this:

example : ![37, 17, 57] 2 = 57 := by rfl -- succeeds
example : ![37, 17, 57] 2 = 57 := by with_reducible_and_instances rfl -- fails

It would be lovely if we could do this at reducible defeq, e.g. for file#AlgebraicGeometry/EllipticCurve/Projective

[Jovan Gerbscheid]

This definition works:

@[reducible] def vecCons {n : ℕ} (h : α) (t : Fin n → α) : Fin n.succ → α
  | ⟨i+1, hi⟩ => t ⟨i, Nat.lt_of_succ_lt_succ hi⟩
  | ⟨0, _⟩ => h

[Eric Wieser]

I think the dependent types are the issue:

import Mathlib

example : ![37, 17, 57] 2 = 57 := by
  unfold Matrix.vecCons Fin.cons Fin.cases Fin.induction Fin.induction.go Fin.induction.go Fin.induction.go
  dsimp only
  with_reducible_and_instances rfl -- fails

[Eric Wieser]

Which is a shame, because I was considering eliminating vecCons in favor of only having Fin.cons

[Eric Wieser]

This works:

import Mathlib

-- upstream these attributes, possibly
set_option allowUnsafeReducibility true
attribute [reducible] Fin.cases Fin.cons Fin.induction Matrix.vecCons Fin.induction.go Eq.mpr

example : ![37, 17, 57] 2 = 57 := by
  with_reducible_and_instances rfl -- works

[Eric Wieser]

Perhaps also relevant that I have a PR open with a dsimproc for this type of expression

[Kim Morrison]

Interesting. Making eq.mpr reducible seems scary!

[Kim Morrison]

dsimproc would be great, but wouldn't help with the erws in Elliptic.

[Aaron Liu]

Kim Morrison said:

Interesting. Making eq.mpr reducible seems scary!

The Eq.mpr comes from the base case match arm | 0, hi => by rwa [Fin.mk_zero] in docs#Fin.induction.go, which can actually just be changed to | 0, _ => zero since Fin.mk_zero is a rfl-lemma.

[Eric Wieser]

That sounds like a good change to me

[Eric Wieser]

Kim Morrison said:

Interesting. Making eq.mpr reducible seems scary!

Potentially, but perhaps worth an experiment to see how scary!