Bug in by_contra (implicit arguments)

Stream: mathlib4

[Yury G. Kudryashov]

example : ∀ {n : Nat}, n = n := by
  by_contra h

creates assumptions n : Nat and n ≠ n instead of Not (∀ {n : Nat}, n = n).

[Jovan Gerbscheid]

It is a macro that turns into this:

example : ∀ {n : Nat}, n = n := by
  refine Decidable.byContradiction fun h => ?_

which has the same problem.

[Aaron Liu]

This seems like something that can be fixed with a little @

[Jovan Gerbscheid]

Wow, why does that work?

A different solution I though of was to use apply Classical.byContractction; intro h

[Eric Wieser]

I assume the fix is @fun?

[Eric Wieser]

This is just the notation to disable implicit lambdas, which are to blame here

[Jovan Gerbscheid]

I interpreted it like this, which works:

example : ∀ {n : Nat}, n = n := by
  refine @Classical.byContradiction _ fun h => ?_

[Eric Wieser]

Does my version also work?

[Jovan Gerbscheid]

No, it even introduces the variable like this:

example : ∀ {n : Nat}, n = n := by
  refine Classical.byContradiction ?_

[Jovan Gerbscheid]

But the problem is indeed caused by an implicit lambda:

import Lean
import Qq

open Qq Lean Elab Term
elab "test" e:term : tactic => do
  let t := q(∀ {n : Nat}, n = n)
  let e ← elabTerm e t
  logInfo m! "{e}"

example : ∀ {n : Nat}, n = n := by
  test Classical.byContradiction ?_ -- fun {n} => Classical.byContradiction ?m.976

[Jovan Gerbscheid]

It seems that it is a feature of @ notation that the implicit lambdas are turned off.

[Jovan Gerbscheid]

Here's another fun one:

import Batteries

example (h : ∀ {n : Nat}, n = n) : True := by
  /-
  don't know how to synthesize implicit argument 'a'
    @absurd (?m.8343 = ?m.8343) True h ?m.8344
  context:

  h : ∀ {n : Nat}, n = n
  ⊢ Prop
  -/
  absurd h

[Jovan Gerbscheid]

And exfalso also introduces implicit variables:

example : ∀ {n : Nat}, n = n := by
  exfalso

[Jovan Gerbscheid]

I think no_implicit_lambda% is also supposed to fix this, but it has some surprising behaviour:

import Lean
import Qq

open Qq Lean Elab Term
elab "test" e:term : tactic => do
  let t := q(∀ {n : Nat}, n = n)
  let e ← elabTerm e t
  logInfo m! "{e}"

set_option pp.explicit true
example : ∀ {n : Nat}, n = n := by
  test -- @Classical.byContradiction (∀ {n : Nat}, @Eq Nat n n) (fun h => ?m.979) ?m.984
    no_implicit_lambda% (Classical.byContradiction fun h => ?_)

[Yury G. Kudryashov]

See https://github.com/leanprover-community/batteries/pull/1162 by @Alex J. Best

[Eric Wieser]

Eric Wieser said:

Does my version also work?

example : ∀ {n : Nat}, n = n := by
  refine Classical.byContradiction @fun h => ?_
  sorry

Seems to work fine for me?

[Jovan Gerbscheid]

On Lean web, it gives me

n✝ : Nat
h : ¬n✝ = n✝
⊢ False

Which is what we don't want.

[Eric Wieser]

Sorry, my mistake

[Eric Wieser]

This works:

example : ∀ {n : Nat}, n = n := by
  refine @(Classical.byContradiction ?_)
  sorry

[Aaron Liu]

never seen the @(...) before

[Aaron Liu]

what does it do

[Eric Wieser]

Suppresses implicit lambdas, somewhat

[Eric Wieser]

A full fix:

example : ∀ {n : Nat}, n = n := by
  refine (Classical.byContradiction fun h => ?_ :)

[Kyle Miller]

In particular, @(t) elaborates t with the implicit lambda flag set to false. The flag doesn't get propagated to subterms, but it does propagate through macro expansions. Normally, with some exceptions, implicit and instance implicit binders in the expected type get "auto-introed" by wrapping the elaborated result in a lambda expression (hence, "implicit lambda"; I guess it's punning "implicit" in the "done implicitly" sense and the "implicit binder" sense).

[Kyle Miller]

Here's another option:

example : ∀ {n : Nat}, n = n := by
  refine_lift Classical.byContradiction ?_; intro h

[Kyle Miller]

I'm really confused why it doesn't seem possible to put fun h => ?_ into the refine_lift, without using (... :)

[Eric Wieser]

Yury G. Kudryashov said:

See https://github.com/leanprover-community/batteries/pull/1162 by Alex J. Best

This is now merged

[Aaron Liu]

(deleted)