Zulip Chat Archive

Stream: general

Topic: simp inside expressions with coe_to_fun sometimes fails


view this post on Zulip Scott Morrison (Aug 05 2018 at 23:57):

I've been trying to implement @Johannes HΓΆlzl request that in my baby PR for category theory I use coercions to allow applying a functor to an object, as F X, rather than having to either write explicitly F.onObjects X, or introduce some awkward notation, such as F +> X.

view this post on Zulip Scott Morrison (Aug 05 2018 at 23:57):

I would very much like to do this, but I also want to be confident that this doesn't mess up the nice and easy automation I have throughout my category theory library.

view this post on Zulip Scott Morrison (Aug 05 2018 at 23:58):

Unfortunately, I seem to have run into a problem, which is a strange interaction between coercions and the simplifier.

view this post on Zulip Scott Morrison (Aug 05 2018 at 23:58):

Hopefully someone here will explain how to get around this! I fear that the fix would require tweaking the simplifier, which is out of bounds at the moment.

view this post on Zulip Scott Morrison (Aug 05 2018 at 23:59):

In any case, here is a self-contained piece of code, containing some very cut down definitions from the category theory library, that demonstrates the problem.

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:00):

Essentially, it is that simp sometimes can't rewrite under a coercion, because it can't build the proof terms (in particular, it can't build some congr_arg terms, because of a type checking subtlety).

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:01):

This has the result that in order to be able to use simp successfully, I'll have to provide two versions of many lemmas: one for use by humans, that refer to the coercions, and one for use by simp (after applying unfold_coes to unfold all the coercions), that don't refer to the coercions.

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:01):

In my mind, that's worse than not having the coercions available in the first place.

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:02):

import tactic.interactive

universe u

class category (Obj : Type u) : Type (u+1) :=
(Hom : Obj β†’ Obj β†’ Type u)
(identity : Ξ  X : Obj, Hom X X)

notation `πŸ™` := category.identity     -- type as \b1
infixr ` ⟢ `:10  := category.Hom     -- type as \h

variable (C : Type u)
variable [π’ž : category C]
variable (D : Type u)
variable [π’Ÿ : category D]
include π’ž π’Ÿ

instance ProductCategory : category (C Γ— D) :=
{ Hom            := Ξ» X Y, ((X.1) ⟢ (Y.1)) Γ— ((X.2) ⟢ (Y.2)),
  identity       := Ξ» X, ⟨ πŸ™ (X.1), πŸ™ (X.2) ⟩ }

@[simp] lemma ProductCategory.identity (X : C) (Y : D) : πŸ™ (X, Y) = (πŸ™ X, πŸ™ Y) := by refl

structure Functor  :=
(onObjects     : C β†’ D)
(onMorphisms   : Ξ  {X Y : C}, (X ⟢ Y) β†’ ((onObjects X) ⟢ (onObjects Y)))
(identities    : βˆ€ (X : C), onMorphisms (πŸ™ X) = πŸ™ (onObjects X))

attribute [simp] Functor.identities

infixr ` +> `:70 := Functor.onObjects
infixr ` &> `:70 := Functor.onMorphisms
infixr ` ↝ `:70 := Functor -- type as \lea

variables {C} {D}

structure NaturalTransformation (F G : C ↝ D) : Type u :=
(components: Π X : C, (F +> X) ⟢ (G +> X))

infixr ` ⟹ `:50  := NaturalTransformation

instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
{ F   := λ α, Π X : C, (F +> X) ⟢ (G +> X),
  coe := Ξ» Ξ±, Ξ±.components }

definition IdentityNaturalTransformation (F : C ↝ D) : F ⟹ F :=
{ components := Ξ» X, πŸ™ (F +> X) }

instance FunctorCategory : category (C ↝ D) :=
{ Hom            := λ F G, F ⟹ G,
  identity       := Ξ» F, IdentityNaturalTransformation F }

@[simp] lemma FunctorCategory.identity.components (F : C ↝ D) (X : C) : (πŸ™ F : F ⟹ F) X = πŸ™ (F +> X) := by refl

lemma test (E : Type u) [β„° : category E] (X : C) (Y : D) (F : C ↝ (D ↝ E)) : (F &> (prod.fst (πŸ™ (X, Y)))) Y = πŸ™ ((F +> X) +> Y) :=
begin
  -- Really, `simp` should just work, finishing the goal.
  -- However this doesn't work:
  success_if_fail {simp},
  -- Notice that rewriting with that simp lemma succeeds:
  rw ProductCategory.identity,
  dsimp,
  -- Again, this `simp` fails:
  success_if_fail {simp},
  rw Functor.identities,
  -- Finally, at this stage `simp` manages to apply FunctorCategory.identity.components
  simp,
end

lemma test' (E : Type u) [β„° : category E] (X : C) (Y : D) (F : C ↝ (D ↝ E)) : (F &> (prod.fst (πŸ™ (X, Y)))) Y = πŸ™ ((F +> X) +> Y) :=
begin
  -- If we unfold all the coercions first, at least `simp` gets started
  unfold_coes,
  simp,
  -- But doesn't finish, because with the coercions gone, FunctorCategory.identity.components doesn't apply anymore!
  admit
end

-- We can define an alternative version of that @[simp] lemma, with the coercion removed.
@[simp] lemma FunctorCategory.identity.components' (F : C ↝ D) (X : C) : (πŸ™ F : F ⟹ F).components X = πŸ™ (F +> X) := by refl

lemma test'' (E : Type u) [β„° : category E] (X : C) (Y : D) (F : C ↝ (D ↝ E)) : (F &> (prod.fst (πŸ™ (X, Y)))) Y = πŸ™ ((F +> X) +> Y) :=
begin
  unfold_coes,
  simp,
  -- At this stage, we've recovered reasonable automation, at the expense of having to
  -- state lemmas twice, once with the coercions (for the humans) and once without (for the simplifier).
end

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:10):

I've seen this issue before. Unfortunately simp does not rewrite inside coercions because they are apparently dependent functions (the nondependency is only visible after you unfold the definition)

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:11):

Exactly!

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:11):

This is related to why I was writing a mk_congr_arg_using_dsimp tactic above. (The idea being that if you dsimp the function first, sometimes you see that it's not actually a dependent function.)

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:13):

I would look into fixing the congr lemma generation to use this

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:14):

Is that something which is fixable? Or is it frozen waiting for Lean 4?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:14):

there is always the option of making simp'

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:14):

I see. But isn't much of simp written in C++?

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:15):

Could we make a patched simp' that had similar performance?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:15):

probably not, but if you use it only when necessary it should be palatable

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:16):

I think you can use ext_simplify_core to hook into the traversal part without messing with the core of simp

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:16):

eek... but my automation really relies on simp just doing its thing. As things are, I don't think there's any way to distinguish between the situations "simp failed to do anything" and "simp would have worked, but broke trying to construct a congr_arg"

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:17):

So it's not like I could just write a tactic that says "do simp, unless that breaks, in which case retry with simp'".

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:17):

Okay, I will investigate ext_simplify_core again. I once knew how that worked, but have forgotten.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:18):

By the way, dsimp works under dependent functions

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:19):

so in particular it works in test

view this post on Zulip Sebastian Ullrich (Aug 06 2018 at 00:20):

Without having thought about it too hard, could a custom congr lemma for non-dependent coercions work?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:20):

Does simp use @[congr] lemmas?

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:21):

While I've got your attention on this, would you mind having a look at my mk_congr_arg_using_dsimp and see if there is a way to avoid polluting the goal with extra hypotheses as a side effect? I'm pretty unhappy about that hack.

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:22):

Yes; I know dsimp works fine, and indeed in my automation I always attempt dsimp before simp; sorry if this minimised example is too minimised, but I certainly have cases where simp is failing because of this effect.

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:23):

@Mario Carneiro, sorry, I don't know what you mean by "Does simp use @[congr] lemmas?".

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:25):

Simp works by using congruence lemmas generated by mk_congr_lemma for traversal. If it also accepts user lemmas marked @{congr], then this would solve all our problems, because we could craft congr lemmas for looking through apparently dependent functions

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:25):

Ah, I see!

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:26):

Also, looking at the coercion in your example, it is in fact a dependent function:

instance {F G : C ↝ D} : has_coe_to_fun (F ⟹ G) :=
{ F   := λ α, Π X : C, (F +> X) ⟢ (G +> X),
  coe := Ξ» Ξ±, Ξ±.components }

so why is this legitimate in this case?

view this post on Zulip Sebastian Ullrich (Aug 06 2018 at 00:27):

@Mario Carneiro I think so? https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/library/tactic/simplify.cpp#L739-L740 simp is the reason [congr] was introduced, afaik

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:27):

The problem is that for particular values of Ξ±, that dependent function might dsimp to a non-dependent function.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 00:28):

I thought [congr] was used for calc

view this post on Zulip Sebastian Ullrich (Aug 06 2018 at 00:33):

I'm not aware of calc using anything other than [trans]

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:48):

Are there any places I can look to find @[congr] used in conjunction with simp? I'm finding the C++ code pretty hard going.

view this post on Zulip Scott Morrison (Aug 06 2018 at 00:53):

I guess I just found @Gabriel Ebner's example at https://github.com/leanprover/lean/commit/6bd3fe24493c1748c8cfd778f63a3b832c6e6ba7#diff-db6c06d0649a66f8bbfc76e59b15cef2, but I'm still not sure what's going on. :-)

view this post on Zulip Scott Morrison (Aug 06 2018 at 01:27):

Okay, I am for now failing to work out how to use @[congr] to help simp work better, or to write my own simp' that uses ext_simplify_core. I'm happy to continue investigating both options, and very happy if someone else does this. :-)

view this post on Zulip Scott Morrison (Aug 06 2018 at 01:30):

In the meantime, could I propose, @Johannes HΓΆlzl and @Mario Carneiro, that in my category theory PR we defer the issue of adding coercions for functors acting on objects, and not consider that an obstacle for merging this PR?

If we can solve the issue here, of course I would love to add these coercions. In the meantime, it is not very expensive to write out the coercions, or have notations for them. I would really like to get this PR done, without breaking the possibility of good automation.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 01:30):

Damn! I figured out what congr lemma to use, but lean doesn't accept it :/

@[congr] theorem NaturalTransformation.components_congr
  {F G : C ↝ D} {Ξ± Ξ² : F ⟹ G} (h : Ξ± = Ξ²) (X) : Ξ±.components X = Ξ².components X :=
congr_fun (congr_arg coe_fn h) _
-- ok, generated automatically

@[congr] theorem NaturalTransformation.coe_congr
  {F G : C ↝ D} {Ξ± Ξ² : F ⟹ G} (h : Ξ± = Ξ²) (X) : Ξ± X = Ξ² X :=
congr_fun (congr_arg coe_fn h) _
-- invalid congruence lemma, 'NaturalTransformation.coe_congr' the left-hand-side of the congruence
-- resulting type must be of the form (coe_fn x_1 ... x_n), where each x_i is a distinct variable or a sort

view this post on Zulip Mario Carneiro (Aug 06 2018 at 01:33):

even worse, the error is garbage because it didn't parse the statement correctly

view this post on Zulip Mario Carneiro (Aug 06 2018 at 01:34):

notice that congr fails on this proof for completely the wrong reason:

theorem NaturalTransformation.coe_congr
  {F G : C ↝ D} {Ξ± Ξ² : F ⟹ G} (h : Ξ± = Ξ²) (X) : Ξ± X = Ξ² X :=
by do {
  tgt ← target,
  (lhs, rhs) ← match_eq tgt,
  guard lhs.is_app,
  clemma ← mk_specialized_congr_lemma lhs,
  trace clemma.type,
  apply_eq_congr_core tgt }
-- invalid apply tactic, failed to unify
--   ⇑α X = ⇑β X
-- with
--   ⇑?m_2 = ⇑?m_2

view this post on Zulip Mario Carneiro (Aug 06 2018 at 01:48):

For the purpose of this PR, how about adding the coercions, but add a simp lemma that unfolds the coercions and make simp lemmas that don't use the coercions. That way users can use the coercions but they won't interfere with simp

view this post on Zulip Mario Carneiro (Aug 06 2018 at 01:54):

@Sebastian Ullrich I think the coe_fn typeclass needs to be fixed so that lean knows it's a pi type:

class has_coe_to_fun (a : Sort u) : Sort (max u (v+1) (w+1)) :=
(dom : a β†’ Sort v) (F : βˆ€ a, dom a β†’ Sort w) (coe : Ξ  x y, F x y)

I tried this modification in my local copy and it seems to work fine, but of course this requires a modification to core. Also related is an issue brought up by Floris a long time ago - has_coe_to_sort doesn't actually require that the target type is a sort. It should read:

class has_coe_to_sort (a : Sort u) : Type (max u v) :=
(coe : a β†’ Sort v)

Any chance of at least getting these into lean 4?

view this post on Zulip Scott Morrison (Aug 06 2018 at 02:04):

Okay, I will try out that approach. You're right that it will probably work. The only downside is that simp will produce 'ugly' output that looks different from what the humans are used to.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 02:09):

of course it already does this enough that we have techniques like "use simp terminally" and "use simpa" to mitigate this problem

view this post on Zulip Scott Morrison (Aug 06 2018 at 02:18):

Okay. So now I'm left with the question of how much _I_ should use the coercion in the library development.

view this post on Zulip Scott Morrison (Aug 06 2018 at 02:19):

I'm inclined to barely use it! That is, provide the coercion, and a simp lemma that unfolds it, but otherwise ignore it.

view this post on Zulip Scott Morrison (Aug 06 2018 at 02:19):

Is that okay? Or is that making life unpleasant for a user?

view this post on Zulip Scott Morrison (Aug 06 2018 at 02:20):

The alternative is to carefully go through, introducing use of the coercion everywhere except in simp lemmas, I guess.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 02:39):

I think you should handle it like sub. Write lemmas using it, but also add simp lemma versions of the theorems when applicable

view this post on Zulip Mario Carneiro (Aug 06 2018 at 02:40):

these should be one liners or restatements

view this post on Zulip Mario Carneiro (Aug 06 2018 at 02:40):

the user will want to use coercions whenever possible, so there should be lemmas supporting this

view this post on Zulip Mario Carneiro (Aug 06 2018 at 02:41):

besides, I haven't lost hope of an automation solution to this, we're talking about a workaround here


Last updated: May 14 2021 at 00:42 UTC