Strict-implicit binder with existential

Stream: mathlib4

[Heather Macbeth]

Do I understand correctly that the syntax for existentials with strict-implicit binders has not been implemented in Lean 4 (or mathlib4) yet? This gives error "expected '(', '_' or identifier"

import Mathlib.Data.Nat.Basic

example : ∃ ⦃x : ℕ⦄, x ^ 2 = 2 := sorry -- fails

and the following push_neg leads to the awkward infoview display ⊢ Exists fun ⦃x⦄ => x ^ 2 = 2:

import Mathlib.Data.Nat.Basic

example : ¬ ∀ ⦃x : ℕ⦄, x ^ 2 ≠ 2 := by
  push_neg -- infoview `Exists fun ⦃x⦄ => x ^ 2 = 2`
  sorry

[Heather Macbeth]

By contrast, on mathlib3 this gives no errors, and the nice infoview display ⊢ ∃ ⦃x : ℕ⦄, x ^ 2 = 2:

import data.nat.basic

example : ∃ ⦃x : ℕ⦄, x ^ 2 = 2 := sorry

example : ¬ ∀ ⦃x : ℕ⦄, x ^ 2 ≠ 2 :=
begin
  push_neg,
  sorry
end

[Heather Macbeth]

This feature seems to be missing for regular-implicit arguments, too.

import Mathlib.Data.Nat.Basic

example : ∃ {x : ℕ}, x ^ 2 = 2 := sorry -- fails

example : ¬ ∀ {x : ℕ}, x ^ 2 ≠ 2 := by
  push_neg -- infoview `Exists fun {x} => x ^ 2 = 2`
  sorry

[Kyle Miller]

Maybe since it's not generally useful to know which binder type is inside an Exists, here's an unexpander that prints them all the same way:

@[app_unexpander Exists]
def extra_exists : Lean.PrettyPrinter.Unexpander
  | `($_ fun {$x:ident} ↦ $p) => `(∃ $x:ident, $p)
  | `($_ fun {$x:ident : $ty:term} ↦ $p) => `(∃ $x:ident : $ty:term, $p)
  | `($_ fun ⦃$x:ident⦄ ↦ $p) => `(∃ $x:ident, $p)
  | `($_ fun ⦃$x:ident : $ty:term⦄ ↦ $p) => `(∃ $x:ident : $ty:term, $p)
  | _ => throw ()

#check Exists fun ⦃x : ℕ⦄ => 0 < x
-- ∃ x, 0 < x : Prop

Though maybe push_neg should normalize the binder type instead?

[Kyle Miller]

(The primary reason I have it printing them all the same way since there's no syntax for exists-with-non-default-binders.)

[Heather Macbeth]

@Kyle Miller Nice! The unexpander is not dealing out of the box with multiple existentials, though:

import Mathlib.Data.Nat.Basic

@[app_unexpander Exists]
def extra_exists : Lean.PrettyPrinter.Unexpander
  | `($_ fun {$x:ident} ↦ $p) => `(∃ $x:ident, $p)
  | `($_ fun {$x:ident : $ty:term} ↦ $p) => `(∃ $x:ident : $ty:term, $p)
  | `($_ fun ⦃$x:ident⦄ ↦ $p) => `(∃ $x:ident, $p)
  | `($_ fun ⦃$x:ident : $ty:term⦄ ↦ $p) => `(∃ $x:ident : $ty:term, $p)
  | _ => throw ()

example : ¬ ∀ {x y : ℕ}, x ^ 2 ≠ y ^ 2 := by
  push_neg -- infoview `∃ x, ∃ y, x ^ 2 = y ^ 2`
  sorry

Is it possible to extend your setup to do it? If not, maybe that's an argument in favour of changing push_neg.

[Kyle Miller]

I'm not sure how to do it with an unexpander, but here's a hack using a delaborator. What it does is set all the binder infos in an Exists chain to default before running the usual delaborator.

open Lean in
/-- Set all the binder infos to `default` in a chain of `Exists`s. -/
partial def fixExists (e : Expr) : MetaM (Bool × Expr) := do
  let (`Exists, #[α, .lam x ty body bi]) := e.getAppFnArgs | return (false, e)
  let (changed, body) ← fixExists body
  let changed := changed || bi != .default
  return (changed, mkAppN e.getAppFn #[α, .lam x ty body .default])

open Lean Lean.PrettyPrinter.Delaborator in
@[delab app.Exists]
def withFixedExists : Delab := do
  let (changed, e) ← fixExists (← SubExpr.getExpr)
  unless changed do failure
  withTheReader SubExpr (fun cfg => { cfg with expr := e}) delab

#check Exists fun ⦃x : ℕ⦄ => Exists fun {y : ℕ} => Exists fun (z : ℕ) => y < x + z
-- ∃ x y z, y < x + z

#check ∃ x y, x + y > 0
-- ∃ x y, x + y > 0

[Heather Macbeth]

Interesting! It seems to me that this works beautifully, why is it a hack?

[Kyle Miller]

It's not clear to me that it's OK to change the expr like this (though at least it's an expression that's ==!)