Zulip Chat Archive

Stream: general

Topic: Bugs

Sebastien Gouezel (Jun 19 2019 at 14:58):

I have the impression to meet more and more surprising behavior of Lean lately, and also that I am not the only one on this chat. Maybe because we are pushing Lean further than the way it has really been used before, and this is bound to uncover some suprises.

Anyway, I just wanted to share with you the following funny fact (no MWE, this is deep inside a non-finished theory). I am not asking for help or whatever, as I have a workaround.

      apply mdifferentiable_at_atlas_to_fun e'_atlas,
      simp [local_homeomorph.trans_source] at hx,
      exact hx.2

works fine. But if I exchange the first two lines (which should commute because they don't touch the same objects),

      simp [local_homeomorph.trans_source] at hx,
      apply mdifferentiable_at_atlas_to_fun e'_atlas,
      exact hx.2

fails with a complain on apply saying

invalid apply tactic, failed to unify
  mdifferentiable_at k ((e'.to_local_equiv).to_fun) ((e.to_local_equiv).inv_fun x)
  mdifferentiable_at ?m_10 ((e'.to_local_equiv).to_fun) ?m_17

Johan Commelin (Jun 19 2019 at 15:01):

We might need to formalize the implementation of Lean and its tactics...

Sebastien Gouezel (Jun 19 2019 at 15:02):

If I move the offending simp two lines before, it's OK :)

Sebastien Gouezel (Jun 19 2019 at 15:10):

And I was just hit again by a simp bug by which it produces an incorrect proof, for which a MWE had been crafted by Rob Lewis as follows.

def foo_rec (n : ) (k : Type) [has_zero k]  : Prop :=
nat.rec_on n (true) (λn rec, true)

lemma stupid (k : Type) [has_zero k] (n : ) :
  foo_rec n k  foo_rec n k :=
  induction n with n IH,
  simp only [nat.nat_zero_eq_zero],
  tactic.result >>= tactic.trace,

I know I will also be able to work around it, by replacing some simp by a rw somewhere in the proof. Just have to find it, wish me luch :)

Sebastien Gouezel (Jun 19 2019 at 15:20):

This is beginning to become very amusing: the offending simp creating an incorrect proof (in a 100 line proof) is right at the place where I mentioned the first bug (where two orthogonal lines could not be swapped). So these are certainly two instances of the same problem.

Last updated: Dec 20 2023 at 11:08 UTC