feat: allow duplicate theorems to be imported

RELEASES.md

@@ -13,6 +13,8 @@ v4.8.0 (development in progress)
 
 * Lean now generates an error if the type of a theorem is **not** a proposition.
 
+* Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
+
 * New command `derive_functinal_induction`:
 
   Derived from the definition of a (possibly mutually) recursive function

src/Lean/Data/HashMap.lean

@@ -116,6 +116,22 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
       else
         (expand size' buckets', false)
 
+@[inline] def insertIfNew [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Option β :=
+  match m with
+  | ⟨size, buckets⟩ =>
+    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
+    let bkt    := buckets.val[i]
+    if let some b := bkt.find? a then
+      (m, some b)
+    else
+      let size'    := size + 1
+      let buckets' := buckets.update i (AssocList.cons a b bkt) h
+      if numBucketsForCapacity size' ≤ buckets.val.size then
+        ({ size := size', buckets := buckets' }, none)
+      else
+        (expand size' buckets', none)
+
+
 def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
   match m with
   | ⟨ size, buckets ⟩ =>
@@ -125,9 +141,10 @@ def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α
     else m
 
 inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
-  | mkWff     : ∀ n,                    WellFormed (mkHashMapImp n)
-  | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
-  | eraseWff  : ∀ m a,   WellFormed m → WellFormed (erase m a)
+  | mkWff          : ∀ n,                    WellFormed (mkHashMapImp n)
+  | insertWff      : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
+  | insertIfNewWff : ∀ m a b, WellFormed m → WellFormed (insertIfNew m a b |>.1)
+  | eraseWff       : ∀ m a,   WellFormed m → WellFormed (erase m a)
 
 end HashMapImp
 
@@ -156,13 +173,22 @@ def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
     match h:m.insert a b with
     | (m', _) => ⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩
 
-/-- Similar to `insert`, but also returns a Boolean flad indicating whether an existing entry has been replaced with `a -> b`. -/
+/-- Similar to `insert`, but also returns a Boolean flag indicating whether an existing entry has been replaced with `a -> b`. -/
 def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
   match m with
   | ⟨ m, hw ⟩ =>
     match h:m.insert a b with
     | (m', replaced) => (⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩, replaced)
 
+/--
+Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
+If the result is `some old`, the the resulting map is equal to `m`. -/
+def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
+  match m with
+  | ⟨ m, hw ⟩ =>
+    match h:m.insertIfNew a b with
+    | (m', old) => (⟨ m', by have aux := WellFormed.insertIfNewWff m a b hw; rw [h] at aux; assumption ⟩, old)
+
 @[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
   match m with
   | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩

src/Lean/Environment.lean

@@ -770,6 +770,33 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
       moduleNames := s.moduleNames.push i.module
     }
 
+/--
+Return `true` if `cinfo₁` and `cinfo₂` are theorems with the same name, universe parameters,
+and types. We allow different modules to prove the same theorem.
+
+Motivation: We want to generate equational theorems on demand and potentially
+in different files, and we want them to have non-private names.
+We may add support for other kinds of definitions in the future. For now, theorems are
+sufficient for our purposes.
+
+We may have to revise this design decision and eagerly generate equational theorems when
+we implement the module system.
+
+Remark: we do not check whether the theorem `value` field match. This feature is useful and
+ensures the proofs for equational theorems do not need to be identical. This decision
+relies on the fact that theorem types are propositions, we have proof irrelevance,
+and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems
+during type-checking, but we are assuming this is not an issue in practice,
+and we are planning to address this issue in the future.
+-/
+private def equivInfo (cinfo₁ cinfo₂ : ConstantInfo) : Bool := Id.run do
+  let .thmInfo tval₁ := cinfo₁ | false
+  let .thmInfo tval₂ := cinfo₂ | false
+  return tval₁.name == tval₂.name
+    && tval₁.type == tval₂.type
+    && tval₁.levelParams == tval₂.levelParams
+    && tval₁.all == tval₂.all
+
 /--
   Construct environment from `importModulesCore` results.
 
@@ -788,11 +815,13 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   for h:modIdx in [0:s.moduleData.size] do
     let mod := s.moduleData[modIdx]'h.upper
     for cname in mod.constNames, cinfo in mod.constants do
-      match constantMap.insert' cname cinfo with
-      | (constantMap', replaced) =>
+      match constantMap.insertIfNew cname cinfo with
+      | (constantMap', cinfoPrev?) =>
         constantMap := constantMap'
-        if replaced then
-          throwAlreadyImported s const2ModIdx modIdx cname
+        if let some cinfoPrev := cinfoPrev? then
+          -- Recall that the map has not been modified when `cinfoPrev? = some _`.
+          unless equivInfo cinfoPrev cinfo do
+            throwAlreadyImported s const2ModIdx modIdx cname
       const2ModIdx := const2ModIdx.insert cname modIdx
     for cname in mod.extraConstNames do
       const2ModIdx := const2ModIdx.insert cname modIdx

tests/pkg/misc/Misc/Boo.lean

@@ -1,3 +1,5 @@
 local infix:50 " ≺ " => LE.le
 
 #check 1 ≺ 2
+
+theorem simple : 10 = 10 := rfl

tests/pkg/misc/Misc/Foo.lean

@@ -16,3 +16,5 @@ local macro "my_refl" : tactic =>
   `(tactic| rfl)
 
 def f (x y : Nat) (_h : x = y := by my_refl) := x
+
+theorem simple : 10 = 10 := by decide