Unexpected behaviours regarding `exists` and `use`

Stream: general

[Asei Inoue]

import Mathlib.Tactic.Common

example (a : Nat) : ∃ n, a < n := by
  exists ?x
  -- the result is as if `exists a` had been executed
  -- why...?
  show a < a
  sorry

example (a : Nat) : ∃ n, a < n := by
  use ?x
  case x => exact a + 1
  -- the infoview displays `No goals`
  -- which is a wrong message
  show a < a + 1
  simp_arith

[Floris van Doorn]

The implementation of exists is in this case refine ⟨?_, ?_⟩; trivial. The refine generates two goals, the first of which is a natural number and trivial tries assumption, filling that natural number with a.
I'd say this is a bug. trivial should probably not use assumption for (non-propositional) goals whose metavariable occur in other goals...

[Mario Carneiro]

why is trivial even being called on the first "goal"?

[Kevin Buzzard]

I think it's worth adding here that non-Prop goals are in practice not really supported in tactic mode (experts might do this but I strongly discourage beginners from doing so), so exists ?x is in some sense an unsupported move and if you get into trouble then this might be your own fault. However is it possible to get assumption to solve a goal with metavariables and thus assign a metavariable to a "random" thing without ever having a non-Prop goal? That would be bad I guess (in the sense that a move which the user considers 100% safe may not be safe)

[Ruben Van de Velde]

Floris van Doorn said:

The implementation of exists is in this case refine ⟨?_, ?_⟩; trivial. The refine generates two goals, the first of which is a natural number and trivial tries assumption, filling that natural number with a.
I'd say this is a bug. trivial should probably not use assumption for (non-propositional) goals whose metavariable occur in other goals...

Could it be something like refine \<..., ?_X>; case _X => try trivial or whatever?