From eeb791d8490dacb8003f96b7b0e0c6ef754e5bd0 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Mon, 30 Oct 2023 00:16:29 +0000 Subject: [PATCH] feat: more delaborators (#7964) Co-authored-by: Kyle Miller --- Mathlib.lean | 2 +- Mathlib/Data/Set/Basic.lean | 1 + .../{PiNotation.lean => Delaborators.lean} | 39 +++++++- test/delaborators.lean | 96 ++++++++++++++++++- test/propose.lean | 2 +- 5 files changed, 135 insertions(+), 5 deletions(-) rename Mathlib/Util/{PiNotation.lean => Delaborators.lean} (72%) diff --git a/Mathlib.lean b/Mathlib.lean index de5b3b18bc9db..74134884c9ac6 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3585,13 +3585,13 @@ import Mathlib.Util.AssertNoSorry import Mathlib.Util.AtomM import Mathlib.Util.CompileInductive import Mathlib.Util.CountHeartbeats +import Mathlib.Util.Delaborators import Mathlib.Util.DischargerAsTactic import Mathlib.Util.Export import Mathlib.Util.Imports import Mathlib.Util.IncludeStr import Mathlib.Util.LongNames import Mathlib.Util.MemoFix -import Mathlib.Util.PiNotation import Mathlib.Util.Qq import Mathlib.Util.SleepHeartbeats import Mathlib.Util.Superscript diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index f71299285dccf..18fece66ff253 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -7,6 +7,7 @@ import Mathlib.Order.SymmDiff import Mathlib.Logic.Function.Iterate import Mathlib.Tactic.Tauto import Mathlib.Tactic.ByContra +import Mathlib.Util.Delaborators #align_import data.set.basic from "leanprover-community/mathlib"@"001ffdc42920050657fd45bd2b8bfbec8eaaeb29" diff --git a/Mathlib/Util/PiNotation.lean b/Mathlib/Util/Delaborators.lean similarity index 72% rename from Mathlib/Util/PiNotation.lean rename to Mathlib/Util/Delaborators.lean index 8856801e45d79..f4bd6dbbda23f 100644 --- a/Mathlib/Util/PiNotation.lean +++ b/Mathlib/Util/Delaborators.lean @@ -23,7 +23,7 @@ also be written as `(x : α) → β x`. -/ -- A direct copy of forall notation but with `Π`/`Pi` instead of `∀`/`Forall`. @[term_parser] def piNotation := leading_parser:leadPrec - unicodeSymbol "Π" "Pi" >> + unicodeSymbol "Π" "PiType" >> many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >> optType >> ", " >> termParser @@ -60,6 +60,16 @@ def delabPi : Delab := whenPPOption Lean.getPPNotation do if x == y then `(∀ $x:ident ≤ $z, $body) else pure stx | `(Π ($i:ident : $_), $j:ident ∈ $s → $body) => if i == j then `(Π $i:ident ∈ $s, $body) else pure stx + | `(∀ ($i:ident : $_), $j:ident ∉ $s → $body) => + if i == j then `(∀ $i:ident ∉ $s, $body) else pure stx + | `(∀ ($i:ident : $_), $j:ident ⊆ $s → $body) => + if i == j then `(∀ $i:ident ⊆ $s, $body) else pure stx + | `(∀ ($i:ident : $_), $j:ident ⊂ $s → $body) => + if i == j then `(∀ $i:ident ⊂ $s, $body) else pure stx + | `(∀ ($i:ident : $_), $j:ident ⊇ $s → $body) => + if i == j then `(∀ $i:ident ⊇ $s, $body) else pure stx + | `(∀ ($i:ident : $_), $j:ident ⊃ $s → $body) => + if i == j then `(∀ $i:ident ⊃ $s, $body) else pure stx | _ => pure stx /-- Override the Lean 4 pi notation delaborator with one that uses `Π` and prints @@ -122,9 +132,34 @@ def exists_delab : Delab := whenPPOption Lean.getPPNotation do | `(∃ $x:ident, $y:ident ≤ $z ∧ $body) | `(∃ ($x:ident : $_), $y:ident ≤ $z ∧ $body) => if x == y then `(∃ $x:ident ≤ $z, $body) else pure stx + | `(∃ $x:ident, $y:ident ∉ $z ∧ $body) + | `(∃ ($x:ident : $_), $y:ident ∉ $z ∧ $body) => do + if x == y then `(∃ $x:ident ∉ $z, $body) else pure stx + | `(∃ $x:ident, $y:ident ⊆ $z ∧ $body) + | `(∃ ($x:ident : $_), $y:ident ⊆ $z ∧ $body) => + if x == y then `(∃ $x:ident ⊆ $z, $body) else pure stx + | `(∃ $x:ident, $y:ident ⊂ $z ∧ $body) + | `(∃ ($x:ident : $_), $y:ident ⊂ $z ∧ $body) => + if x == y then `(∃ $x:ident ⊂ $z, $body) else pure stx + | `(∃ $x:ident, $y:ident ⊇ $z ∧ $body) + | `(∃ ($x:ident : $_), $y:ident ⊇ $z ∧ $body) => + if x == y then `(∃ $x:ident ⊇ $z, $body) else pure stx + | `(∃ $x:ident, $y:ident ⊃ $z ∧ $body) + | `(∃ ($x:ident : $_), $y:ident ⊃ $z ∧ $body) => + if x == y then `(∃ $x:ident ⊃ $z, $body) else pure stx | _ => pure stx - -- Merging match stx with | `(∃ $group:bracketedExplicitBinders, ∃ $groups*, $body) => `(∃ $group $groups*, $body) + | `(∃ $b:binderIdent, ∃ $[$bs:binderIdent]*, $body) => `(∃ $b:binderIdent $[$bs]*, $body) | _ => pure stx end existential + +open Lean Lean.PrettyPrinter.Delaborator + +/-- Delaborator for `∉`. -/ +@[delab app.Not] def delab_not_in := whenPPOption Lean.getPPNotation do + let #[f] := (← SubExpr.getExpr).getAppArgs | failure + guard <| f.isAppOfArity ``Membership.mem 5 + let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab + let stx₂ ← SubExpr.withAppArg <| SubExpr.withNaryArg 4 delab + return ← `($stx₁ ∉ $stx₂) diff --git a/test/delaborators.lean b/test/delaborators.lean index 740aea9832830..d2a38eb29d569 100644 --- a/test/delaborators.lean +++ b/test/delaborators.lean @@ -1,5 +1,5 @@ import Std.Tactic.GuardMsgs -import Mathlib.Util.PiNotation +import Mathlib.Util.Delaborators import Mathlib.Data.Set.Lattice section PiNotation @@ -45,6 +45,48 @@ variable (P : Nat → Prop) (α : Nat → Type) (s : Set ℕ) #guard_msgs in #check ∀ x, x ∈ s → P x +/-- info: ∀ x ∉ s, P x : Prop -/ +#guard_msgs in +#check ∀ x ∉ s,P x + +/-- info: ∀ x ∉ s, P x : Prop -/ +#guard_msgs in +#check ∀ x, x ∉ s → P x + +variable (Q : Set ℕ → Prop) + +/-- info: ∀ t ⊆ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t ⊆ s, Q t + +/-- info: ∀ t ⊆ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t, t ⊆ s → Q t + +/-- info: ∀ t ⊂ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t ⊂ s, Q t + +/-- info: ∀ t ⊂ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t, t ⊂ s → Q t + +/-- info: ∀ t ⊇ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t ⊇ s, Q t + +/-- info: ∀ t ⊇ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t, t ⊇ s → Q t + +/-- info: ∀ t ⊃ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t ⊃ s, Q t + +/-- info: ∀ t ⊃ s, Q t : Prop -/ +#guard_msgs in +#check ∀ t, t ⊃ s → Q t + /-- info: (x : ℕ) → α x : Type -/ #guard_msgs in #check (x : Nat) → α x @@ -103,6 +145,58 @@ section existential #guard_msgs in #check ∃ (i : Nat), i < 3 ∧ i = i +variable (s : Set ℕ) (P : ℕ → Prop) (Q : Set ℕ → Prop) + +/-- info: ∃ x ∉ s, P x : Prop -/ +#guard_msgs in +#check ∃ x ∉ s, P x + +/-- info: ∃ x ∉ s, P x : Prop -/ +#guard_msgs in +#check ∃ x, x ∉ s ∧ P x + +variable (Q : Set ℕ → Prop) + +/-- info: ∃ t ⊆ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t ⊆ s, Q t + +/-- info: ∃ t ⊆ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t, t ⊆ s ∧ Q t + +/-- info: ∃ t ⊂ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t ⊂ s, Q t + +/-- info: ∃ t ⊂ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t, t ⊂ s ∧ Q t + +/-- info: ∃ t ⊇ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t ⊇ s, Q t + +/-- info: ∃ t ⊇ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t, t ⊇ s ∧ Q t + +/-- info: ∃ t ⊃ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t ⊃ s, Q t + +/-- info: ∃ t ⊃ s, Q t : Prop -/ +#guard_msgs in +#check ∃ t, t ⊃ s ∧ Q t + +/-- info: ∃ n k, n = k : Prop -/ +#guard_msgs in +#check ∃ n k, n = k + +/-- info: ∃ n k, n = k : Prop -/ +#guard_msgs in +#check ∃ n, ∃ k, n = k + end existential section prod diff --git a/test/propose.lean b/test/propose.lean index 52ce9bb2eaa6f..30b616591d1dd 100644 --- a/test/propose.lean +++ b/test/propose.lean @@ -57,7 +57,7 @@ example (p : Nat × String) : True := by /-- info: Try this: have : List.Disjoint M L := List.disjoint_symm w --- -info: Try this: have : ¬a ∈ M := foo L M w m +info: Try this: have : a ∉ M := foo L M w m -/ #guard_msgs in example (K L M : List α) (w : L.Disjoint M) (m : a ∈ L) : True := by