From e3578c2f36c2d4fa9cc55584a7671c0c81c70ed9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 24 Jun 2024 03:18:41 +0200
Subject: [PATCH] fix: discrepancy `theorem` vs `example`  (#4493)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When the type of an `example` is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.

Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for examples when
their type was a proposition.
This discrepancy often confused users.

Additionally, we considered extending the above behavior to definitions
when
1- When their type is a proposition. However, it still caused disruption
in Mathlib.
2- When their type is provided. That is, we would keep the current
behavior only if `: <type>` was omitted. This would make the elaborator
for `def` much closer to the one for `theorem`, but it proved to be too
restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
  ⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
  ⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more
in Mathlib.

closes #4398
closes #4482 Remark: PR #4482 implements option 1 above. We may consider
it again in the future.
---
 src/Lean/Elab/MutualDef.lean                     |  5 ++++-
 tests/lean/1682.lean.expected.out                |  8 ++++----
 tests/lean/813.lean.expected.out                 |  4 ++--
 .../lean/interactive/plainGoal.lean.expected.out | 12 ++++++------
 tests/lean/ppProofs.lean.expected.out            |  2 +-
 tests/lean/run/1575.lean                         |  8 ++++++--
 tests/lean/run/4398.lean                         |  5 +++++
 .../lean/run/multiTargetCasesInductionIssue.lean |  6 +++---
 tests/lean/rwEqThms.lean.expected.out            | 16 ++++++++--------
 9 files changed, 39 insertions(+), 27 deletions(-)
 create mode 100644 tests/lean/run/4398.lean

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index b59cc73330..fa9e3b0bf0 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -846,7 +846,10 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      if view.kind.isTheorem then
+      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
+      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
+      -- Moreover, the type of most definitions are not propositions anyway.
+      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> isProp header.type) then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }
diff --git a/tests/lean/1682.lean.expected.out b/tests/lean/1682.lean.expected.out
index cd49d31eeb..050d08bc51 100644
--- a/tests/lean/1682.lean.expected.out
+++ b/tests/lean/1682.lean.expected.out
@@ -1,21 +1,21 @@
 1682.lean:1:25-2:17: error: unsolved goals
 case a
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 ⊢ p → q
 
 case b
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 ⊢ r
 1682.lean:4:25-5:26: error: unsolved goals
 case a
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 h : p
 ⊢ q
 
 case b
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 ⊢ r
diff --git a/tests/lean/813.lean.expected.out b/tests/lean/813.lean.expected.out
index 3ce42e0faa..7a1bb87901 100644
--- a/tests/lean/813.lean.expected.out
+++ b/tests/lean/813.lean.expected.out
@@ -1,12 +1,12 @@
 p : Nat → Prop
 h : p 1
 ⊢ p 1
-α : Sort ?u
+α : Sort u_1
 a : α
 p : α → Prop
 h : p a
 ⊢ p a
-α : Sort ?u
+α : Sort u_1
 a : α
 f : α → α
 p : α → Prop
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 91a2fdd633..08286c755c 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -82,9 +82,9 @@
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 55, "character": 3}}
 {"rendered":
- "```lean\nα : Sort ?u\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```",
+ "```lean\nα : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```",
  "goals":
- ["α : Sort ?u\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]}
+ ["α : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 61, "character": 3}}
 {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
@@ -110,15 +110,15 @@
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 53}}
 {"rendered":
- "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
+ "```lean\ncase nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
  "goals":
- ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
+ ["case nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 54}}
 {"rendered":
- "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
+ "```lean\ncase nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
  "goals":
- ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
+ ["case nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 86, "character": 38}}
 {"rendered": "no goals", "goals": []}
diff --git a/tests/lean/ppProofs.lean.expected.out b/tests/lean/ppProofs.lean.expected.out
index 76139fc7d6..0aad812ed9 100644
--- a/tests/lean/ppProofs.lean.expected.out
+++ b/tests/lean/ppProofs.lean.expected.out
@@ -13,7 +13,7 @@ a : α
 h : α = β
 ⊢ ⋯ ▸ a = b
 ppProofs.lean:10:50-10:98: error: unsolved goals
-α β : Sort ?u
+α β : Sort u_1
 b : β
 a : α
 h : α = β
diff --git a/tests/lean/run/1575.lean b/tests/lean/run/1575.lean
index 47e677127e..561edb90ce 100644
--- a/tests/lean/run/1575.lean
+++ b/tests/lean/run/1575.lean
@@ -1,2 +1,6 @@
-example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
-  ⟨fun ⟨x, _⟩ ⟨y, _⟩ => Subsingleton.elim x y ▸ sorry⟩
+example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) := by
+  constructor
+  intro ⟨x, _⟩ ⟨y, _⟩
+  have := Subsingleton.elim x y
+  subst this
+  rfl
diff --git a/tests/lean/run/4398.lean b/tests/lean/run/4398.lean
new file mode 100644
index 0000000000..641dc3c89d
--- /dev/null
+++ b/tests/lean/run/4398.lean
@@ -0,0 +1,5 @@
+example {ι : Type _} (n m : ι) (h : n = m) : m = n := by
+  simp only [id h] -- should work
+
+example {ι : Type _} (n m : ι) (h : n = m) : m = n := by
+  simp only [h] -- works
diff --git a/tests/lean/run/multiTargetCasesInductionIssue.lean b/tests/lean/run/multiTargetCasesInductionIssue.lean
index 07e73d21e8..211ccc709c 100644
--- a/tests/lean/run/multiTargetCasesInductionIssue.lean
+++ b/tests/lean/run/multiTargetCasesInductionIssue.lean
@@ -24,7 +24,7 @@ def Vec.casesOn
   | ⟨as, h⟩ => go n as h
 
 /--
-info: α : Type _
+info: α : Type u_1
 n✝ : Nat
 a✝ : α
 as✝ : Vec α n✝
@@ -43,7 +43,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
     constructor
 
 /--
-info: α : Type _
+info: α : Type u_1
 n✝ : Nat
 a✝ : α
 as✝ : Vec α n✝
@@ -62,7 +62,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
     constructor
 
 /--
-info: α : Type _
+info: α : Type u_1
 n : Nat
 a : α
 as : Vec α n
diff --git a/tests/lean/rwEqThms.lean.expected.out b/tests/lean/rwEqThms.lean.expected.out
index 166374b659..cd30d2e7ad 100644
--- a/tests/lean/rwEqThms.lean.expected.out
+++ b/tests/lean/rwEqThms.lean.expected.out
@@ -1,41 +1,41 @@
-α : Type ?u
+α : Type u_1
 a : α
 as bs : List α
 h : bs = a :: as
 ⊢ (?head :: as).length = bs.length
 
 case head
-α : Type ?u
+α : Type u_1
 a : α
 as bs : List α
 h : bs = a :: as
 ⊢ α
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ as.length + 1 + 1 = bs.length + 2
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ as.length + 1 + 1 = (b :: bs).length + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ as.length + 1 + 1 = bs.length + 1 + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ id (a :: b :: as).length = (b :: bs).length + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ (a :: b :: as).length = (b :: bs).length + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs