Zulip Chat Archive

Stream: general

Topic: How does `congr` know to apply `subsingleton.elim`


view this post on Zulip Eric Wieser (Jan 05 2021 at 12:11):

Is this hard coded? docs#subsingleton.elim doesn't have any any attributes attached, so I'm not sure how to investigate further into what tactic#congr is doing
.

view this post on Zulip Eric Wieser (Jan 05 2021 at 12:21):

The example in question is

import linear_algebra.tensor_product
open_locale tensor_product

example {R M N : Type*}
  [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
  (add_comm_monoid.nat_semimodule.to_distrib_mul_action.to_mul_action.to_has_scalar
    : has_scalar  (M [R] N)) =
  tensor_product.has_scalar' :=
begin
  change _ = tensor_product.semimodule'.to_distrib_mul_action.to_mul_action.to_has_scalar,
  congr,
  apply_instance,
  apply_instance,
end

view this post on Zulip Eric Wieser (Jan 05 2021 at 12:22):

And I was hoping that I could train congr to solve it more easily. I can't see how to tag this with attr#congr either.

view this post on Zulip Gabriel Ebner (Jan 05 2021 at 13:01):

subsingleton is hard-coded into the code that creates the congruence lemmas.


Last updated: May 14 2021 at 03:27 UTC