Why doesn't this rewrite?

Stream: new members

[Daniele Pusceddu]

Hello, I can't figure out why the rw [same] in the example below does not work.
I introduced same as a sanity check to verify they are indeed equal, but even a direct rewrite does not work... I also tried conv.

import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Finset.Basic

structure test where
  f: ℕ →₀ ℕ
  h: f.support.card = 2

def test.upd
  (t: test) (n: ℕ) (m: ℕ)
  (hin: n ∈ t.f.support) (hpos: ¬m=0): test :=

  ⟨t.f.update n m, by

   simp [Finsupp.update, hpos]
   have same:
    Finset.card (insert n t.f.support) = Finset.card t.f.support
    := by exact Finset.card_insert_of_mem hin
   rw [same]
   sorry
  ⟩

[Andrés Goens]

@Daniele Pusceddu Lean pretty-prints your proof state so that it's more readable, but you can add an option to make it show everything in detail (turn off pretty printing), e.g. by adding the line set_option pp.all true in above your def test.upd.

[Andrés Goens]

in your case it gives me this:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  @Finset.card.{0} Nat
    (@Insert.insert.{0, 0} Nat (Finset.{0} Nat)
      (@Finset.instInsertFinset.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) n
      (@Finsupp.support.{0, 0} Nat Nat
        (@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t)))
t : test
n m : Nat
hin :
  @Membership.mem.{0, 0} Nat (Finset.{0} Nat) (@Finset.instMembershipFinset.{0} Nat) n
    (@Finsupp.support.{0, 0} Nat Nat
      (@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t))
hpos : Not (@Eq.{1} Nat m (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
same :
  @Eq.{1} Nat
    (@Finset.card.{0} Nat
      (@Insert.insert.{0, 0} Nat (Finset.{0} Nat)
        (@Finset.instInsertFinset.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) n
        (@Finsupp.support.{0, 0} Nat Nat
          (@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t))))
    (@Finset.card.{0} Nat
      (@Finsupp.support.{0, 0} Nat Nat
        (@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t)))
⊢ @Eq.{1} Nat
    (@Finset.card.{0} Nat
      (@Insert.insert.{0, 0} Nat (Finset.{0} Nat)
        (@Finset.instInsertFinset.{0} Nat fun (a b : Nat) => Classical.decEq.{1} Nat a b) n
        (@Finsupp.support.{0, 0} Nat Nat
          (@LinearOrderedCommMonoidWithZero.toZero.{0} Nat Nat.linearOrderedCommMonoidWithZero) (test.f t))))
    (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))

[Andrés Goens]

and if you compare same with your goal, it looks ilke it's using a different equality type for a = b, instDecidableEqNat a b vs Classical.decEq.{1} Nat a b

[Andrés Goens]

that answers why it doesn't rewrite. How to fix that I'm not sure, I don't really know what Classical.decEq does and why your h in test asks for that

[Andrés Goens]

What I do in situations like that is just write a line
#check Classical.decEq so that I can use my editor to "go to definition", and that sends me to the mathlib definition of Classical.decEq:

/-- Any type `α` has decidable equality classically. -/
noncomputable def decEq (α : Sort u) : DecidableEq α := by infer_instance
#align classical.dec_eq Classical.decEq

[Andrés Goens]

the strange thing is that it's using that instance for your cardinalities, which are Nats. I have no idea why though

[Yaël Dillies]

The answer is that docs4#Finsupp is classical and something in the API is leaking this implementation detail. I don't know where exactly the problem is, but I can tell you something is wrong and it's not your fault.

[Andrés Goens]

thanks, that's a much better way of putting it @Yaël Dillies :sweat_smile:

[Kyle Miller]

@Daniele Pusceddu There's a tactic that can be useful here, which is convert. It knows that there is at most one Fintype instance for a given type and inserts rewrites automatically for you to convert from one to the other. Since the LHS of same is supposed to match the LHS of the goal (except for the fact it's not defeq), we can do convert same to have it line things up and create new goals for things it can't figure out are equal.

import Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic.Convert

structure test where
  f: ℕ →₀ ℕ
  h: f.support.card = 2

def test.upd
  (t: test) (n: ℕ) (m: ℕ)
  (hin: n ∈ t.f.support) (hpos: ¬m=0): test :=

  ⟨t.f.update n m,
    by

      simp [Finsupp.update, hpos]
      have same: Finset.card (insert n t.f.support) = Finset.card t.f.support
        := by exact Finset.card_insert_of_mem hin
      convert same -- or do `convert ← same` to get the goal to be reversed, which looks better
      sorry
  ⟩

[Kyle Miller]

In general, think of convert to be like exact but it creates side goals wherever there are differences that it can't resolve itself.