apply? suggested something that led to an error

Stream: new members

[Kevin Cheung]

I tried the following:

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Real.Sqrt

example (n : ℕ) (a: Fin (n + 1) → Fin (Nat.zero + 1)) : ∀ i : Fin (n + 1), a i = 0 := by
  apply?

Lean said:

Try this: exact fun i ↦ eq_zero_of_zero_eq_one rfl (a i)

But the following gives an error on rfl.

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Real.Sqrt

example (n : ℕ) (a: Fin (n + 1) → Fin (Nat.zero + 1)) : ∀ i : Fin (n + 1), a i = 0 := by
  exact fun i ↦ eq_zero_of_zero_eq_one rfl (a i)

From the InfoView:

FinError.lean:5:39
application type mismatch
  eq_zero_of_zero_eq_one rfl
argument
  rfl
has type
  0 = 0 : Prop
but is expected to have type
  0 = 1 : Prop

I have two questions:

1. Should we expect apply? to suggest something that Lean might not accept?
2. Is the example provable?

[Kyle Miller]

If apply? responds with something, it is provable.

And yes, we do expect apply? to suggest things that Lean might not accept — but, it's not that there's no proof, it's that it didn't pretty print the proof it derived in a way that can be read back in and interpreted correctly. (We expect it only because of limitations in the pretty printer's ability to succeed in "round tripping".)

[Kyle Miller]

Sometimes setting set_option pp.analysis true gets it to pretty print with enough information to work. That doesn't appear to work here however.

[Kyle Miller]

set_option pp.explicit true works

[Kyle Miller]

example (n : ℕ) (a: Fin (n + 1) → Fin (Nat.zero + 1)) : ∀ i : Fin (n + 1), a i = 0 := by
  exact fun i ↦
    @eq_zero_of_zero_eq_one (Fin (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1))
      (@NonAssocSemiring.toMulZeroOneClass
        (Fin (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1))
        (@Semiring.toNonAssocSemiring
          (Fin (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1))
          (@CommSemiring.toSemiring
            (Fin (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1))
            (@CommRing.toCommSemiring
              (Fin (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1))
              (@Fin.instCommRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1)
                (@NeZero.succ Nat.zero))))))
      (@rfl (Fin (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) Nat.zero 1)) 0) (a i)

[Kyle Miller]

Once you have that, you can simplify the term by hand.

[Kyle Miller]

example (n : ℕ) (a: Fin (n + 1) → Fin (Nat.zero + 1)) : ∀ i : Fin (n + 1), a i = 0 := by
  exact fun i ↦ eq_zero_of_zero_eq_one (Eq.refl (0 : Fin 1)) (a i)

[Kevin Cheung]

Thanks for the proof. Could the limitation be overcome?

[Kyle Miller]

Well, set_option pp.all true theoretically overcomes that limitation, at the cost of having unreadable terms :-)

[Kyle Miller]

The set_option pp.analyze true option was meant to try to make round tripping work, but (1) as we see in this example, it doesn't always work and (2) apparently in practice it was too verbose as a default for all pretty printing.

[Kyle Miller]

exact? and apply? should probably pretty print with pp.analyze true (and that algorithm needs more attention)

[Kevin Cheung]

Thanks for the explanation.

[Damiano Testa]

Sometimes I think that apply? also mistakes which variables to use where.

[Damiano Testa]

See for instance this example, where, besides the incorrect Ne.symm and metavariables, the second variable should have been H instead of repeated hc.

[Michael Stoll]

Here is another problem:

import Mathlib

lemma main_odd {a : ℕ} (ha' : Odd a) :
    0 ≠ 4 + a := by
  intro heq
  have ha'' : Odd (4 + a) := by
    -- `apply?` suggests
    refine Nat.odd_add'.mpr (?_ (id heq.symm))
    -- which gives an error on `(?_ (id heq.symm))`
  sorry

Why is apply? producing suggestions involving expressions like (?_ (id heq.symm)) above? It does not seem to make a lot of sense.

[Kyle Miller]

That's weird. The goals that apply? reports show that it's really just saying "you can prove this by reverting heq"

Try this: refine Nat.odd_add'.mpr (?_ (id heq.symm))
Remaining subgoals:
⊢ 4 + a = 0 → (Odd a ↔ Even 4)
⊢ Odd a ↔ Even 4

[Michael Stoll]

But the second subgoal subsumes the first, so reverting heq is completely unnecessary.

[Michael Stoll]

Here is another failure:

import Mathlib.Data.Int.Basic

example (a b c : ℤ) (ha : a ≠ 0) (h : a * b = a * c) : b = c := by
  -- exact? fails, apply? does not produce anything useful
  exact Int.eq_of_mul_eq_mul_left ha h

It works when I remove the import.

[Michael Stoll]

The first suggestion from apply? is

Try this: refine Int.neg_inj.mp (?_ (id (Ne.symm ha)))
Remaining subgoals:
⊢ 0 ≠ a → -b = -c
⊢ a * c = a * b → -b = -c
⊢ -b = -c

where again the last subgoal implies the other two (and this occurs a lot). It should just produce

Try this: refine Int.neg_inj.mp ?_
Remaining subgoals:
⊢ -b = -c

(not that this is useful in the example...).

[Michael Stoll]

@Kim Morrison :up:

[Michael Stoll]

You really don't want the first suggestion apply? produces to look like that:

Try this: refine help (?_ (id heq.symm)) (?_ (id heq.symm)) (?_ (id heq.symm))
Remaining subgoals:
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → ℕ
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → ℤ
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → ℤ
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → ℤ
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → ℤ
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → IsCoprime (?m.63791 ⋯) ↑(?m.60679 ⋯)
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 →
  ?m.70015 ⋯ ^ 2 - ?m.66903 ⋯ * ?m.73127 ⋯ ^ 2 = ?m.63791 ⋯ * ↑(?m.60679 ⋯)
⊢ 8 * ↑b * (1 + 2 * ↑b ^ 3) = X ^ 2 - 7 * (2 * ↑b) * Y ^ 2 → J(?m.66903 ⋯ | ?m.60679 ⋯) = -1
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → ℕ
⊢ ℕ
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → ℤ
⊢ ℤ
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → ℤ
⊢ ℤ
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → ℤ
⊢ ℤ
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → ℤ
⊢ ℤ
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → IsCoprime (?m.63791 ⋯) ↑(?m.60679 ⋯)
⊢ IsCoprime (?m.63791 ⋯) ↑(?m.60679 ⋯)
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → ?m.70015 ⋯ ^ 2 - ?m.66903 ⋯ * ?m.73127 ⋯ ^ 2 = ?m.63791 ⋯ * ↑(?m.60679 ⋯)
⊢ ?m.70015 ⋯ ^ 2 - ?m.66903 ⋯ * ?m.73127 ⋯ ^ 2 = ?m.63791 ⋯ * ↑(?m.60679 ⋯)
⊢ -1 = J(7 * (2 * ↑b) | 1 + 2 * b ^ 3) → J(?m.66903 ⋯ | ?m.60679 ⋯) = -1
⊢ J(?m.66903 ⋯ | ?m.60679 ⋯) = -1

Am I the only one who is seeing this?

[Michael Stoll]

This seems to be a fairly recent regression.

[Michael Stoll]

I think I have found the declaration that changes the behavior of apply? from "good" to "bad" (but I have no idea how it does it):

axiom f : Nat → Nat

theorem test (m n : Nat) (h : n = f m) : f n = f m := sorry

attribute [symm] Eq.symm -- set in `Mathlib.Init.Logic`

theorem foo (a : Nat) (h : a = 6) : f a = f 3 := by
  apply?
  /-
  Try this: refine test 3 a (?_ (id h.symm))
  Remaining subgoals:
  ⊢ 6 = a → a = f 3
  ⊢ a = f 3 -/

-- without `attribute [symm] Eq.symm`:
  /-
  Try this: refine test 3 a ?h
  Remaining subgoals:
  ⊢ a = f 3
  -/

file#Mathlib/Init/Logic in line 45 does

attribute [symm] Eq.symm

Whatever the intended effect is, it also has the unintended effect on apply? shown above.
A knock-on effect of this bad behavior seems to be that the text produced by apply? in the infoview is extremely bloated, which (at least on my fairly fast laptop) makes scrolling through it in VSCode extremely sluggish, so that apply? becomes almost unusable except in very simple situations. (This had been much better until fairly recently.)

[Michael Stoll]

The symm attribute is defined in Lean/Meta/Tactic/Symm.lean, which seems to have been created by lean4#3408 (maybe moved from Std). @Joe Hendrix
The problematic behavior of apply? seems to predate the merging of this PR, though...

[Michael Stoll]

Moving the discussion here.