# Zulip Chat Archive

## 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_1 : @eq.{1} nat (@has_add.add.{0} nat nat.has_add n m) n,
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?

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

#mwe?

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

wow what is happening

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

#### 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 φ ψ hφ hψ, rw [add_mul, coeff_add, coeff_add, add_mul, hφ, hψ], },
intros m r,
apply polynomial.induction_on' q,
{ intros φ ψ hφ hψ, rw [mul_add, coeff_add, coeff_add, mul_add, hφ, hψ], },
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