Forall x not in

Stream: lean4

[Patrick Massot]

In Lean 3 we could write

variables (s : set nat) (x : nat)

#check ∀ x ∉ s, true

(without any import!). In Lean 4, even importing all of Mathlib is not enough

import Mathlib

variable (s : Set Nat) (x : Nat)

#check ∀ x ∉ s, True

Is this really missing?

[Alex J. Best]

yes looks that way, but its easy to add

import Mathlib

variable (s : Set Nat) (x : Nat)

binder_predicate x " ∉ " y:term => `($x ∉ $y)

#check ∀ x ∉ s, True

[Patrick Massot]

Thanks Alex, but I think this isn't enough. It will be missing in delaborators.

[Alex J. Best]

Looks like that is more hardcoded yeah https://github.com/leanprover-community/mathlib4/blob/8cd944d0aa56ccfd19573ab0199afe25b4431fee/Mathlib/Util/PiNotation.lean#L50

[Alex J. Best]

Oh but you wrote that 2 weeks ago?

[Patrick Massot]

I know...

[Yaël Dillies]

Surely that's covered by @Kyle Miller's binder elaboration suite?

[Patrick Massot]

std4#323 @Mario Carneiro

[Patrick Massot]

By the way Mario, are you interested in having this file in Std? I could add it to the above PR, updating it for new binders.

[Patrick Massot]

Remember you said two weeks ago that this file was good enough for Mathlib until you'll redo it better.

[Mario Carneiro]

nope, for one thing it will require a lot more review than the PR you just sent, and for another I will probably push to do it the right way if you do so it will probably take a while

[Mario Carneiro]

this is besides the part where I'm not sure we want pi notation, given it was removed from core

[Eric Wieser]

Presumably we could split that file in two, and Std could gain the bit that uses the extended binders on forall?

[Eric Wieser]

(or at least, exists_delab)

[Mario Carneiro]

yes I think a piece of that file, suitably rewritten, is appropriate for std

[Patrick Massot]

Oh no,

variable (x : Nat) (s : Set Nat)

#check x ∉ s

already fails to use the notation.

[Patrick Massot]

Is there an easy way to find which delaborator is used? Say I notice that #check 0 ≠ 1 and I want to see which delaborator was used so that I can copy-paste it.

[Alex J. Best]

Ne is its own def though, so probably just using the default app unexpander for applications (https://github.com/leanprover/lean4/blob/6c5f79c0df01e9cd74ac4ee411ec392a5ac1b5d3/src/Lean/Elab/Notation.lean#L81), so I'm not sure this would apply in the same way for not in out of the box

[Patrick Massot]

I managed to write in only half an hour:

open Lean Lean.PrettyPrinter.Delaborator
@[delab app.Not] def delab_not_in := whenPPOption Lean.getPPNotation do
  let #[f] := (← SubExpr.getExpr).getAppArgs | failure
  unless f.getAppFn matches .const `Membership.mem _ do failure
  let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab
  let stx₂ ← SubExpr.withAppArg <| SubExpr.withNaryArg 4 delab
  return ← `($stx₁ ∉ $stx₂)

I think I deserve some lunch.

[Patrick Massot]

I "quickly" created #7964 before lunch.