Zulip Chat Archive

Stream: general

Topic: goal is not well formed after simp??


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 27 2020 at 09:47):

@Mario Carneiro Can you use this to prove false?

view this post on Zulip Mario Carneiro (Jun 27 2020 at 09:48):

#mwe?

view this post on Zulip Kenny Lau (Jun 27 2020 at 09:49):

wow what is happening

view this post on Zulip Johan Commelin (Jun 27 2020 at 09:50):

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

view this post on Zulip Johan Commelin (Jun 27 2020 at 09:50):

I pushed to bad-goal

view this post on Zulip Mario Carneiro (Jun 27 2020 at 09:50):

you can't M it any more than that?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 27 2020 at 09:50):

This is on the Cayley--Hamilton branch

view this post on Zulip Johan Commelin (Jun 27 2020 at 09:50):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 27 2020 at 09:52):

it might be that simp made a bad subgoal

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 27 2020 at 10:01):

Lunch time now...

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 27 2020 at 10:03):

what does the kernel say?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 27 2020 at 10:07):

conclusion: don't use simp

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 27 2020 at 10:07):

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

view this post on Zulip Mario Carneiro (Jun 27 2020 at 10:07):

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

view this post on Zulip Kevin Buzzard (Jun 27 2020 at 10:14):

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

view this post on Zulip Kenny Lau (Jun 27 2020 at 10:16):

minimized:

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

view this post on Zulip 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/

view this post on Zulip 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