goal is not well formed after simp??

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

@Mario Carneiro Can you use this to prove false?

[Mario Carneiro]

#mwe?

[Kenny Lau]

wow what is happening

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/bad-goal/src/data/polynomial_cayley_hamilton.lean#L63

[Johan Commelin]

I pushed to bad-goal

[Mario Carneiro]

you can't M it any more than that?

[Johan Commelin]

@[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]

This is on the Cayley--Hamilton branch

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

it might be that simp made a bad subgoal

[Johan Commelin]

@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]

Lunch time now...

[Mario Carneiro]

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

[Kenny Lau]

what does the kernel say?

[Mario Carneiro]

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]

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]

conclusion: don't use simp

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

minimized:

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

[Johan Commelin]

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

[Gabriel Ebner]

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