Another unexpected rw failure

Stream: new members

[Egor Morozov]

Could someone explain why rw fails here?

import Mathlib

structure WDigraph (V R : Type*) [CommSemiring R] where
  weight : V → V → R

universe u v

variable {V : Type u}
variable {R : Type v} [CommRing R]
variable (G : WDigraph V R)

namespace WDigraph

def Adj (u v : V) : Prop := G.weight u v ≠ 0

inductive Walk : V → V → Type u
  | nil {u : V} : Walk u u
  | cons {u v w : V} (h : G.Adj u v) (p : Walk v w) : Walk u w
  deriving DecidableEq

class PathFinite : Prop where
  fin_walks : ∀ (u v : V), Finite (G.Walk u v)

/- Define Fintype instance to be able to take finite sums -/

instance {u v : V} [h : PathFinite G] : Finite (G.Walk u v) :=
  h.fin_walks u v

noncomputable instance {u v : V} [PathFinite G] :
  Fintype (G.Walk u v) := Fintype.ofFinite _

end WDigraph

open WDigraph

variable {n : ℕ}
variable [PathFinite G]

noncomputable def path_matrix (A B : Fin n → V) :=
    Matrix.of (fun i j => ∑ (p : G.Walk (A i) (B j)), p.weight)

abbrev path_system (A B : Fin n → V) :=
  (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → G.Walk (A i) (B (σ i)))

namespace path_system

variable {A B : Fin n → V} (P : path_system G A B)

instance : Finite (path_system G A B) := inferInstance

noncomputable instance : Fintype (path_system G A B) := Fintype.ofFinite _

end path_system

/- I don't need a proof of the example below, it is just a demonstration of the problem -/

example (A B : Fin n → V) : ∑ (P : path_system G A B), 0 = 0 := by
  unfold path_system
  rw [Fintype.sum_sigma
      (ι := Equiv.Perm (Fin n))
      (α := fun (σ : Equiv.Perm (Fin n)) =>
      ((i : Fin n) → G.Walk (A i) (B (σ i))))
      (M := ℕ)
      (f := fun x => 0)]

I get

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ∑ x, 0
in the target expression
  ∑ P, 0 = 0

I know that sometimes this happens because rw cannot synthesize some instances but here filled all explicit arguments by hands and I still get the same error. Also, set_option trace.Meta.synthInstance true shows that all necessary instances are synthesized. So it seems that the problem is somewhere else and I'm really out of ideas.

[Riccardo Brasca]

Just erase the line

noncomputable instance : Fintype (path_system G A B) := Fintype.ofFinite _

[Riccardo Brasca]

These Fintype instances are a little subtle, especially if you think as a mathematician. Giving a Fintype instance is not the same as saying that something is Finite, it more or less means to fix an ordering (and that the thing is finite). In particular you can have two incompatible Fintype instances, and this is what was happening here.

[Riccardo Brasca]

You may ask: which two?
Well, the point is that path_system G A B is an abbrev for (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → G.Walk (A i) (B (σ i))), and Lean sees through abbrev. In particular, when it needs a Fintype instance for path_system G A B it looks if it has one for (σ : Equiv.Perm (Fin n)) × ((i : Fin n) → G.Walk (A i) (B (σ i))): now, this is a product, so Lean knows that it is enough to find one for each factor. It keeps reasoning like that and at end it is able to produce, automatically, a Fintype instance on path_system G A B.

Now, the line noncomputable instance : Fintype (path_system G A B) := Fintype.ofFinite _ means: chose a totally random Fintype instance, one nobody can say anything about.

[Riccardo Brasca]

At the end you have fixed two ordering on your type, and so there are two ways of computing the sum (of course the result is the same, but this is not totally transparent to Lean), so the system complains.

[Egor Morozov]

@Riccardo Brasca , oh, thank you for so much! This is a really detailed and enlightening explanation.

[Riccardo Brasca]

In general don't add any instance unless Lean complains that it is not able to find one.

[Egor Morozov]

I see, that is exactly my mistake here. I was sure I need Fintypeinstance to write the sum but it turned out that Lean was able to synthesize it.

[Riccardo Brasca]

We tried to make system working as you would do on paper:you have to assume that something is finite in your work, but then all other finiteness condition are automatic, and you should to be worried about them.