## Stream: general

### Topic: goal is not well formed after simp??

#### Johan Commelin (Jun 27 2020 at 09:41):

After a simp * at *, I end up with the following goal stat (pp.all is true)

R : Type u_1,
_inst_1 : ring.{u_1} R,
p q : @polynomial.{u_1} R (@ring.to_semiring.{u_1} R _inst_1),
m : nat,
r : R,
n : nat,
s : R,
h_2 : not (@eq.{1} nat n m),
h : true
⊢ @eq.{u_1+1} R
(@has_mul.mul.{u_1} R
(@mul_zero_class.to_has_mul.{u_1} R (@semiring.to_mul_zero_class.{u_1} R (@ring.to_semiring.{u_1} R _inst_1)))
r
s)
n


#### Johan Commelin (Jun 27 2020 at 09:42):

This looks like trouble, because the n at the end of the goal is a nat, but isn't coerced to R.

#### Johan Commelin (Jun 27 2020 at 09:47):

@Mario Carneiro Can you use this to prove false?

#mwe?

#### Kenny Lau (Jun 27 2020 at 09:49):

wow what is happening

#### Johan Commelin (Jun 27 2020 at 09:50):

I pushed to bad-goal

#### Mario Carneiro (Jun 27 2020 at 09:50):

you can't M it any more than that?

#### Johan Commelin (Jun 27 2020 at 09:50):

@[simp] lemma mul_coeff_zero (p q : polynomial R) : coeff (p * q) 0 = coeff p 0 * coeff q 0 :=
begin
apply polynomial.induction_on' p,
intros m r,
apply polynomial.induction_on' q,
intros n s,
rw [monomial_eq_smul_X, monomial_eq_smul_X, ← C_mul', ← C_mul', X_pow_mul_assoc, ← mul_assoc,
← C_mul, mul_assoc, ← pow_add, coeff_C_mul, coeff_C_mul, coeff_C_mul],
simp only [if_t_t, mul_boole, coeff_X_pow, zero_mul, ite_mul, mul_ite, mul_zero],
split_ifs; simp * at *,
end


#### Johan Commelin (Jun 27 2020 at 09:50):

This is on the Cayley--Hamilton branch

#### Johan Commelin (Jun 27 2020 at 09:50):

I'll see if I can M it more than that.

#### Mario Carneiro (Jun 27 2020 at 09:51):

You might want to try closing the goal with sorry and see what the kernel has to say about it

#### Mario Carneiro (Jun 27 2020 at 09:52):

it might be that simp made a bad subgoal

#### Johan Commelin (Jun 27 2020 at 10:01):

@Mario Carneiro This works on current master

import data.polynomial

example {R : Type*} [ring R] (m n : ℕ) (p q : polynomial R) (r s : R) :
ite (0 = n + m) (r * s * 1) 0 =
ite (0 = n) (ite (0 = m) (r * 1 * (s * 1)) 0) 0 :=
begin
split_ifs; simp * at *,
end


#### Johan Commelin (Jun 27 2020 at 10:01):

Lunch time now...

#### Mario Carneiro (Jun 27 2020 at 10:02):

and as I thought if you put ; sorry at the end the kernel has the same complaint as you

#### Kenny Lau (Jun 27 2020 at 10:03):

what does the kernel say?

#### Mario Carneiro (Jun 27 2020 at 10:05):

what you would expect:

example {R : Type*} [ring R] (m n : ℕ) (p q : polynomial R) (r s : R)
(h_1 : 0 = n) : r * s * 1 = 0 :=
begin
simp * at *, sorry
end

type mismatch at application
r * s = n
term
n
has type
ℕ
but is expected to have type
R


#### Mario Carneiro (Jun 27 2020 at 10:06):

simp generates a subgoal that is not well typed, so of course if you try to close that goal by any means you will get a badly typed proof

#### Kenny Lau (Jun 27 2020 at 10:07):

conclusion: don't use simp

#### Mario Carneiro (Jun 27 2020 at 10:07):

example {R : Type*} [ring R] (m n : ℕ) (p q : polynomial R) (r s : R)
(h : 0 = n) : r * s * 1 = 0 :=
begin
simp [h], sorry
end


#### Mario Carneiro (Jun 27 2020 at 10:07):

The problem is that simp isn't good at distinguishing numerals from different types

#### Mario Carneiro (Jun 27 2020 at 10:07):

so it thinks it can rewrite the 0 on the rhs of the goal using h

#### Kevin Buzzard (Jun 27 2020 at 10:14):

It's ok, simp is being removed from lean 4 anyway :laughing:

#### Kenny Lau (Jun 27 2020 at 10:16):

minimized:

example (h : 1 = 0) : (0 : ℤ) = 1 :=
begin
simp [h], sorry
end


#### Johan Commelin (Jun 27 2020 at 11:41):

@Mario Carneiro @Gabriel Ebner Is this something that can be fixed? Or should we learn to live with this/

#### Gabriel Ebner (Jun 27 2020 at 11:46):

I've pushed it onto the todo stack: lean#362

Last updated: May 18 2021 at 15:14 UTC