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):

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

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 φ ψ  , rw [add_mul, coeff_add, coeff_add, add_mul, , ], },
  intros m r,
  apply polynomial.induction_on' q,
  { intros φ ψ  , rw [mul_add, coeff_add, coeff_add, mul_add, , ], },
  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: Dec 20 2023 at 11:08 UTC