# Zulip Chat Archive

## Stream: general

### Topic: simp inside expressions with coe_to_fun sometimes fails

#### 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`

.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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).

#### 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.

#### Scott Morrison (Aug 06 2018 at 00:01):

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

#### 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

#### 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)

#### Scott Morrison (Aug 06 2018 at 00:11):

Exactly!

#### 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.)

#### Mario Carneiro (Aug 06 2018 at 00:13):

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

#### Scott Morrison (Aug 06 2018 at 00:14):

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

#### Mario Carneiro (Aug 06 2018 at 00:14):

there is always the option of making `simp'`

#### Scott Morrison (Aug 06 2018 at 00:14):

I see. But isn't much of `simp`

written in C++?

#### Scott Morrison (Aug 06 2018 at 00:15):

Could we make a patched `simp'`

that had similar performance?

#### Mario Carneiro (Aug 06 2018 at 00:15):

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

#### 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`

#### 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`

"

#### 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'`

".

#### 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.

#### Mario Carneiro (Aug 06 2018 at 00:18):

By the way, `dsimp`

works under dependent functions

#### Mario Carneiro (Aug 06 2018 at 00:19):

so in particular it works in `test`

#### 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?

#### Mario Carneiro (Aug 06 2018 at 00:20):

Does `simp`

use `@[congr]`

lemmas?

#### 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.

#### 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.

#### Scott Morrison (Aug 06 2018 at 00:23):

@Mario Carneiro, sorry, I don't know what you mean by "Does `simp`

use `@[congr]`

lemmas?".

#### 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

#### Scott Morrison (Aug 06 2018 at 00:25):

Ah, I see!

#### 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?

#### 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

#### 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.

#### Mario Carneiro (Aug 06 2018 at 00:28):

I thought `[congr]`

was used for `calc`

#### Sebastian Ullrich (Aug 06 2018 at 00:33):

I'm not aware of `calc`

using anything other than `[trans]`

#### 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.

#### 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. :-)

#### 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. :-)

#### 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.

#### 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

#### Mario Carneiro (Aug 06 2018 at 01:33):

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

#### 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

#### 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`

#### 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?

#### 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.

#### 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

#### 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.

#### 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.

#### Scott Morrison (Aug 06 2018 at 02:19):

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

#### 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.

#### 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

#### Mario Carneiro (Aug 06 2018 at 02:40):

these should be one liners or restatements

#### Mario Carneiro (Aug 06 2018 at 02:40):

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

#### 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