esimp?

Stream: general

[Reid Barton]

Using Scott's category theory library, I sometimes encounter subexpressions like compose f (identity X), but with the caveat that one or both of the implicit "object" arguments of compose is not syntactically equal to X. This appears to stymie simp from reducing the subexpression to f. Is there a way to make simp smarter here?
I know about erw, which in my experience solves this problem when I want to use rw, but I haven't found a good solution for simp.

[Reid Barton]

It's kind of annoying, since I guess simp could just generalize the wildcards in the pattern when trying to match the identity lemma...

[Reid Barton]

that is, rather than match against

@categories.category.compose.{?u_0 ?u_1} ?x_0 ?x_1 ?x_2 ?x_3 ?x_3 ?x_4
  (@categories.category.identity.{?u_0 ?u_1} ?x_0 ?x_1 ?x_3)

look for

@categories.category.compose.{?u_0 ?u_1} ?x_0 ?x_1 ?x_2 ?x_3' ?x_3'' ?x_4   -- make these distinct
  (@categories.category.identity.{?u_0 ?u_1} ?x_0 ?x_1 ?x_3)

on the assumption that, if we found this, we can conclude that definitionally ?x_3 = ?x_3' = ?x_3'', and no need to check syntactic equality

[Mario Carneiro]

In my experience this doesn't stop simp...

def nat2 := nat
example (x : ℕ) : x + @has_zero.zero nat2 nat.has_zero = x :=
by simp

[Mario Carneiro]

I don't think it tries to match arguments that are dependencies at all

[Reid Barton]

Hmm, strange. I have several uses of dsimp, simp where I'm pretty sure the dsimp is just simplifying one of these object arguments. Let me look more closely at a simple one...

[Reid Barton]

Here is a small reproducer that depends on lean-category-theory (or -pr):

import categories.category
open categories
variables {C : Type} [small_category C]
def M : C → C := id

set_option trace.simplify.rewrite true
set_option pp.all true
variables {a b : C} {f : M a ⟶ M b}
example : (f ≫ 𝟙 b : a ⟶ b) = f := begin simp end
/-
simplify tactic failed to simplify
state:
C : Type,
_inst_1 : categories.small_category.{0} C,
a b : C,
f : @categories.category.Hom.{0 0} C _inst_1 (@M C _inst_1 a) (@M C _inst_1 b)
⊢ @eq.{1} (@categories.category.Hom.{0 0} C _inst_1 a b)
    (@categories.category.compose.{0 0} C _inst_1 a (@M C _inst_1 b) b f
       (@categories.category.identity.{0 0} C _inst_1 b))
    f
-/
example : (f ≫ 𝟙 b : a ⟶ b) = f := begin dsimp [M], simp end -- ok

[Reid Barton]

With the dsimp [M], the only change in the goal is that (@M C _inst_1 b) is replaced by b

[Mario Carneiro]

is there any change if you dsimp the type of f instead of the goal?

[Reid Barton]

How would I do that?

[Mario Carneiro]

dsimp [M] at f

[Reid Barton]

Subsequent simp is still stuck

[Mario Carneiro]

does rw work?

[Reid Barton]

rw doesn't work, but erw does

[Reid Barton]

(Which I learned about from its usage in Scott's library.)

[Mario Carneiro]

erw will work because it's basically just dsimp [M], rw

[Reid Barton]

Maybe your example works because of this canonize_instances stuff?

[Reid Barton]

Or maybe not

[Reid Barton]

A related example that I don't understand.

set_option pp.all true
variable (z : has_zero nat)
example (x : nat) : x + @has_zero.zero nat z = x := by simp
/-
type mismatch at application
  (λ (a a_1 : nat) (e_1 : @eq.{1} nat a a_1) (a_2 a_3 : nat) (e_2 : @eq.{1} nat a_2 a_3),
     @congr.{1 1} nat Prop (@eq.{1} nat a) (@eq.{1} nat a_1) a_2 a_3
       (@congr_arg.{1 1} nat (nat → Prop) a a_1 (@eq.{1} nat) e_1)
       e_2)
    (@has_add.add.{0} nat nat.has_add x (@has_zero.zero.{0} nat z))
    x
    (@add_zero.{0} nat nat.add_monoid x)
term
  @add_zero.{0} nat nat.add_monoid x
has type
  @eq.{1} nat
    (@has_add.add.{0} nat (@add_semigroup.to_has_add.{0} nat (@add_monoid.to_add_semigroup.{0} nat nat.add_monoid)) x
       (@has_zero.zero.{0} nat (@add_monoid.to_has_zero.{0} nat nat.add_monoid)))
    x
but is expected to have type
  @eq.{1} nat (@has_add.add.{0} nat nat.has_add x (@has_zero.zero.{0} nat z)) x
-/

[Reid Barton]

Note that the simp tactic actually succeeded, and used add_zero. So somehow simp didn't care that the has_zero dictionary was the wrong one. But looking at trace.type_context.is_def_eq_detail output and the type_context.cpp code, I don't see how this is possible.

[Chris Hughes]

This problem came up for me today, helping someone who had a proof that was approved by the tactics but not by the kernel, where there was a nat.pow versus monoid.pow issue somewhere.