# 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) with 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 := 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 (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: Aug 03 2023 at 10:10 UTC