Bugs

Stream: general

[Sebastien Gouezel]

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)
with
  mdifferentiable_at ?m_10 ((e'.to_local_equiv).to_fun) ?m_17

[Johan Commelin]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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 :=
begin
  induction n with n IH,
  simp only [nat.nat_zero_eq_zero],
  admit,
  tactic.result >>= tactic.trace,
end

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]

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.