Bump Mathlib and Lean

avigad · Oct 16, 2023 · 010746f · 010746f
1 parent 0dfa81c
commit 010746f
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 265 deletions.
diff --git a/MIL/Common.lean b/MIL/Common.lean
@@ -2,250 +2,3 @@ import Mathlib.Tactic
 import Mathlib.Util.PiNotation
 
 set_option warningAsError false
-
-namespace PiNotation
-open Lean.Parser Term
-open Lean.PrettyPrinter.Delaborator
-
-
-/-- Override the Lean 4 pi notation delaborator with one that uses `Π`.
-Note that this takes advantage of the fact that `(x : α) → p x` notation is
-never used for propositions, so we can match on this result and rewrite it. -/
-@[delab forallE]
-def delabPi' : Delab := whenPPOption Lean.getPPNotation do
-  let stx ← delabForall
-  -- Replacements
-  let stx : Term ←
-    match stx with
-    | `($group:bracketedBinder → $body) => `(Π $group:bracketedBinder, $body)
-    | _ => pure stx
-  -- Cute binders
-  let stx : Term ←
-    match stx with
-    | `(∀ ($i:ident : $_), $j:ident ∈ $s → $body) =>
-      if i == j then `(∀ $i:ident ∈ $s, $body) else pure stx
-    | `(∀ ($x:ident : $_), $y:ident > $z → $body) =>
-      if x == y then `(∀ $x:ident > $z, $body) else pure stx
-    | `(∀ ($x:ident : $_), $y:ident < $z → $body) =>
-      if x == y then `(∀ $x:ident < $z, $body) else pure stx
-    | `(∀ ($x:ident : $_), $y:ident ≥ $z → $body) =>
-      if x == y then `(∀ $x:ident ≥ $z, $body) else pure stx
-    | `(∀ ($x:ident : $_), $y:ident ≤ $z → $body) =>
-      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
-    | _ => pure stx
-  -- Merging
-  match stx with
-  | `(Π $group, Π $groups*, $body) => `(Π $group $groups*, $body)
-  | _ => pure stx
-
-end PiNotation
-
-section SupInfNotation
-open Lean Lean.PrettyPrinter.Delaborator
-
-/-!
-Improvements to the unexpanders in `Mathlib.Order.CompleteLattice`.
-
-These are implemented as delaborators directly.
--/
-@[delab app.iSup]
-def iSup_delab : Delab := whenPPOption Lean.getPPNotation do
-  let #[_, _, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
-  unless f.isLambda do failure
-  let prop ← Meta.isProp ι
-  let dep := f.bindingBody!.hasLooseBVar 0
-  let ppTypes ← getPPOption getPPFunBinderTypes
-  let stx ← SubExpr.withAppArg do
-    let dom ← SubExpr.withBindingDomain delab
-    withBindingBodyUnusedName $ fun x => do
-      let x : TSyntax `ident := .mk x
-      let body ← delab
-      if prop && !dep then
-        `(⨆ (_ : $dom), $body)
-      else if prop || ppTypes then
-        `(⨆ ($x:ident : $dom), $body)
-      else
-        `(⨆ $x:ident, $body)
-  -- Cute binders
-  let stx : Term ←
-    match stx with
-    | `(⨆ $x:ident, ⨆ (_ : $y:ident ∈ $s), $body)
-    | `(⨆ ($x:ident : $_), ⨆ (_ : $y:ident ∈ $s), $body) =>
-      if x == y then `(⨆ $x:ident ∈ $s, $body) else pure stx
-    | _ => pure stx
-  return stx
-
-@[delab app.iInf]
-def iInf_delab : Delab := whenPPOption Lean.getPPNotation do
-  let #[_, _, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
-  unless f.isLambda do failure
-  let prop ← Meta.isProp ι
-  let dep := f.bindingBody!.hasLooseBVar 0
-  let ppTypes ← getPPOption getPPFunBinderTypes
-  let stx ← SubExpr.withAppArg do
-    let dom ← SubExpr.withBindingDomain delab
-    withBindingBodyUnusedName $ fun x => do
-      let x : TSyntax `ident := .mk x
-      let body ← delab
-      if prop && !dep then
-        `(⨅ (_ : $dom), $body)
-      else if prop || ppTypes then
-        `(⨅ ($x:ident : $dom), $body)
-      else
-        `(⨅ $x:ident, $body)
-  -- Cute binders
-  let stx : Term ←
-    match stx with
-    | `(⨅ $x:ident, ⨅ (_ : $y:ident ∈ $s), $body)
-    | `(⨅ ($x:ident : $_), ⨅ (_ : $y:ident ∈ $s), $body) =>
-      if x == y then `(⨅ $x:ident ∈ $s, $body) else pure stx
-    | _ => pure stx
-  return stx
-
-/-- The Exists notation has similar considerations as sup/inf -/
-@[delab app.Exists]
-def exists_delab : Delab := whenPPOption Lean.getPPNotation do
-  let #[ι, f] := (← SubExpr.getExpr).getAppArgs | failure
-  unless f.isLambda do failure
-  let prop ← Meta.isProp ι
-  let dep := f.bindingBody!.hasLooseBVar 0
-  let ppTypes ← getPPOption getPPFunBinderTypes
-  let stx ← SubExpr.withAppArg do
-    let dom ← SubExpr.withBindingDomain delab
-    withBindingBodyUnusedName $ fun x => do
-      let x : TSyntax `ident := .mk x
-      let body ← delab
-      if prop && !dep then
-        `(∃ (_ : $dom), $body)
-      else if prop || ppTypes then
-        `(∃ ($x:ident : $dom), $body)
-      else
-        `(∃ $x:ident, $body)
-  -- Cute binders
-  let stx : Term ←
-    match stx with
-    | `(∃ $i:ident, $j:ident ∈ $s ∧ $body)
-    | `(∃ ($i:ident : $_), $j:ident ∈ $s ∧ $body) =>
-      if i == j then `(∃ $i:ident ∈ $s, $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)
-  | _ => pure stx
-
--- the above delaborators are still needed:
-#check ⨆ (i : Nat) (_ : i ∈ Set.univ), (i = i)
-#check ∃ (i : Nat), i ≥ 3 ∧ i = i
-
-end SupInfNotation
-
-section UnionInterNotation
-open Lean Lean.PrettyPrinter.Delaborator
-
-/-!
-Improvements to the unexpanders in `Mathlib.Data.Set.Lattice`.
-
-These are implemented as delaborators directly.
--/
-
-@[delab app.Set.iUnion]
-def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
-  let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
-  unless f.isLambda do failure
-  let prop ← Meta.isProp ι
-  let dep := f.bindingBody!.hasLooseBVar 0
-  let ppTypes ← getPPOption getPPFunBinderTypes
-  let stx ← SubExpr.withAppArg do
-    let dom ← SubExpr.withBindingDomain delab
-    withBindingBodyUnusedName $ fun x => do
-      let x : TSyntax `ident := .mk x
-      let body ← delab
-      if prop && !dep then
-        `(⋃ (_ : $dom), $body)
-      else if prop || ppTypes then
-        `(⋃ ($x:ident : $dom), $body)
-      else
-        `(⋃ $x:ident, $body)
-  -- Cute binders
-  let stx : Term ←
-    match stx with
-    | `(⋃ $x:ident, ⋃ (_ : $y:ident ∈ $s), $body)
-    | `(⋃ ($x:ident : $_), ⋃ (_ : $y:ident ∈ $s), $body) =>
-      if x == y then `(⋃ $x:ident ∈ $s, $body) else pure stx
-    | _ => pure stx
-  return stx
-
-@[delab app.Set.iInter]
-def sInter_delab : Delab := whenPPOption Lean.getPPNotation do
-  let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
-  unless f.isLambda do failure
-  let prop ← Meta.isProp ι
-  let dep := f.bindingBody!.hasLooseBVar 0
-  let ppTypes ← getPPOption getPPFunBinderTypes
-  let stx ← SubExpr.withAppArg do
-    let dom ← SubExpr.withBindingDomain delab
-    withBindingBodyUnusedName $ fun x => do
-      let x : TSyntax `ident := .mk x
-      let body ← delab
-      if prop && !dep then
-        `(⋂ (_ : $dom), $body)
-      else if prop || ppTypes then
-        `(⋂ ($x:ident : $dom), $body)
-      else
-        `(⋂ $x:ident, $body)
-  -- Cute binders
-  let stx : Term ←
-    match stx with
-    | `(⋂ $x:ident, ⋂ (_ : $y:ident ∈ $s), $body)
-    | `(⋂ ($x:ident : $_), ⋂ (_ : $y:ident ∈ $s), $body) =>
-      if x == y then `(⋂ $x:ident ∈ $s, $body) else pure stx
-    | _ => pure stx
-  return stx
-
-
-end UnionInterNotation
-
-
-namespace ProdProjNotation
-open Lean Lean.PrettyPrinter.Delaborator
-
-@[delab app.Prod.fst, delab app.Prod.snd]
-def delabProdProjs : Delab := do
-  let #[_, _, _] := (← SubExpr.getExpr).getAppArgs | failure
-  let stx ← delabProjectionApp
-  match stx with
-  | `($(x).fst) => `($(x).1)
-  | `($(x).snd) => `($(x).2)
-  | _ => failure
-
-/-! That works when the projection is a simple term, but we need
-another approach when the projections are functions with applied arguments. -/
-
-@[app_unexpander Prod.fst]
-def unexpandProdFst : Lean.PrettyPrinter.Unexpander
-  | `($(_) $p $xs*) => `($p.1 $xs*)
-  | _ => throw ()
-
-@[app_unexpander Prod.snd]
-def unexpandProdSnd : Lean.PrettyPrinter.Unexpander
-  | `($(_) $p $xs*) => `($p.2 $xs*)
-  | _ => throw ()
-
-example (p : Nat × Nat) : p.1 = p.2 → True := by simp
-example (p : (Nat → Nat) × (Nat → Nat)) : p.1 22 = p.2 37 → True := by simp
-
-end ProdProjNotation
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,19 +4,11 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "69c11afc3834fd1d0ee62995c5aacc39dabf834c",
+    "rev": "38db825645dc57221fd6572c9c151e2d28b862ea",
     "opts": {},
     "name": "mathlib",
     "inputRev?": "master",
     "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
@@ -25,14 +17,6 @@
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/JLimperg/aesop",
-    "subDir?": null,
-    "rev": "41c6370eb2f0c9052bee6af0e0a017b9ba8da2b8",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -48,5 +32,21 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.18",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "85a0d4891518518edfccee16cbceac139efa460c",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "0bd8465d8a5cfdd53c1ff0fd57ca5eaa53eb455c",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
     "inherited": true}}],
  "name": "mil"}
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc1
+leanprover/lean4:v4.2.0-rc2
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.2.0-rc1
		leanprover/lean4:v4.2.0-rc2