implicit arguments, and `ring`

Stream: general

[Scott Morrison]

Hi @Mario Carneiro, I noticed an unfortunate feature of ring.

[Scott Morrison]

I'd got stuck doing this:

example (x y : ℕ) (h : x ^ 2 + 3 * y ^ 2 = 4) : false :=
begin
ring at h,
simp at h,
ring at h,
simp at h,
-- ...
end

[Scott Morrison]

where it looks like the goal isn't changing.

[Scott Morrison]

It just says

x y : ℕ,
h : x ^ 2 + 3 * y ^ 2 = 4
⊢ false

[Scott Morrison]

but with pp.all true, you can see if flipping back and forth:

[Mario Carneiro]

You shouldn't use ring nonterminally

[Mario Carneiro]

at least not automatically (i.e. in tidy)

[Mario Carneiro]

if it doesn't close the goal, assume it failed

[Scott Morrison]

Yes, I know, but I want to for a moment anyway. :-)

[Scott Morrison]

Ah, okay. :-)

[Scott Morrison]

But that takes all the fun out of it.

[Mario Carneiro]

ring rewrites the goal into sum-of-products form for ease of reading when it fails

[Scott Morrison]

Because sometimes ring at *, exfalso, linarith can get stuff done.

[Mario Carneiro]

this form disagrees with simp normal form in some places

[Scott Morrison]

The problem I was having here is actually just in the implicit arguments flipping back and forth.

[Scott Morrison]

The expression "itself" is not being changed by either simp or ring.

[Mario Carneiro]

wait, maybe I don't understand then

[Mario Carneiro]

what is changing?

[Scott Morrison]

With usual pretty printing, neither simp nor ring do anything, and the goal just looks like

x y : ℕ,
h : x ^ 2 + 3 * y ^ 2 = 4
⊢ false

[Scott Morrison]

but with pp.all we get:

[Scott Morrison]

x y : nat,
h :
  @eq.{1} nat
    (@has_add.add.{0} nat nat.has_add
       (@has_pow.pow.{0 0} nat nat nat.has_pow x (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))
       (@has_mul.mul.{0} nat
          (@mul_zero_class.to_has_mul.{0} nat
             (@semiring.to_mul_zero_class.{0} nat
                (@comm_semiring.to_semiring.{0} nat
                   (@canonically_ordered_comm_semiring.to_comm_semiring.{0} nat
                      nat.canonically_ordered_comm_semiring))))
          (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one))
          (@has_pow.pow.{0 0} nat nat nat.has_pow y (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))))
    (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))
⊢ false

[Scott Morrison]

after the simp

[Mario Carneiro]

oh, it's nat.pow isn't it

[Scott Morrison]

and then

[Scott Morrison]

x y : nat,
h :
  @eq.{1} nat
    (@has_add.add.{0} nat nat.has_add
       (@has_pow.pow.{0 0} nat nat
          (@monoid.has_pow.{0} nat
             (@semiring.to_monoid.{0} nat
                (@comm_semiring.to_semiring.{0} nat
                   (@canonically_ordered_comm_semiring.to_comm_semiring.{0} nat
                      nat.canonically_ordered_comm_semiring))))
          x
          (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))
       (@has_mul.mul.{0} nat
          (@mul_zero_class.to_has_mul.{0} nat
             (@semiring.to_mul_zero_class.{0} nat
                (@comm_semiring.to_semiring.{0} nat
                   (@canonically_ordered_comm_semiring.to_comm_semiring.{0} nat
                      nat.canonically_ordered_comm_semiring))))
          (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one))
          (@has_pow.pow.{0 0} nat nat
             (@monoid.has_pow.{0} nat
                (@semiring.to_monoid.{0} nat
                   (@comm_semiring.to_semiring.{0} nat
                      (@canonically_ordered_comm_semiring.to_comm_semiring.{0} nat
                         nat.canonically_ordered_comm_semiring))))
             y
             (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))))
    (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))
⊢ false

[Scott Morrison]

after the ring

[Mario Carneiro]

right, ring prefers monoid powers but that's not simp normal form

[Scott Morrison]

Okay, I see.

[Scott Morrison]

Nothing to be done, then!

[Mario Carneiro]

ring doesn't make any attempt to be in simp normal form; if you need that you should just call ring, simp

[Mario Carneiro]

but even better is to just ignore the pretty failure mode

[Kenny Lau]

it's a feature!