feat: declaration form to document welcome proofs (#401)

Add proof_wanted, a declaration form that is elaborated as an axiom
and then thrown away. This can serve as a guide for new contributors
who are looking for high-impact work that can be more quickly
reviewed.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

README.md

@@ -48,3 +48,9 @@ Note that documentation for the latest nightly of `std4` is available as part of
 documentation][mathlib4 docs].
 
 [mathlib4 docs]: https://leanprover-community.github.io/mathlib4_docs/Std.html
+
+# Contributing
+
+The easiest way to contribute is to find a missing proof and complete it. The `proof_wanted`
+declaration documents statements that have been identified as being useful, but that have not yet
+been proven.

Std.lean

@@ -34,6 +34,7 @@ import Std.Data.Fin.Init.Lemmas
 import Std.Data.Fin.Lemmas
 import Std.Data.HashMap
 import Std.Data.HashMap.Basic
+import Std.Data.HashMap.Lemmas
 import Std.Data.HashMap.WF
 import Std.Data.Int.Basic
 import Std.Data.Int.DivMod
@@ -158,5 +159,6 @@ import Std.Util.Cache
 import Std.Util.ExtendedBinder
 import Std.Util.LibraryNote
 import Std.Util.Pickle
+import Std.Util.ProofWanted
 import Std.Util.TermUnsafe
 import Std.WF

Std/Data/Array/Lemmas.lean

@@ -9,6 +9,7 @@ import Std.Data.List.Lemmas
 import Std.Data.Array.Basic
 import Std.Tactic.HaveI
 import Std.Tactic.Simpa
+import Std.Util.ProofWanted
 
 local macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 
@@ -76,13 +77,17 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 
 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp
 
+proof_wanted get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]?
+
 theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
     (a.push x)[i]? = some a[i] := by
   rw [getElem?_pos, get_push_lt]
 
 theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
   rw [getElem?_pos, get_push_eq]
 
+@[simp] proof_wanted get?_size {a : Array α} : a[a.size]? = none
+
 @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
 
 @[simp] theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
@@ -388,3 +393,7 @@ theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p :=
 
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [all_def, List.all_eq_true, mem_def]
+
+/-! ### erase -/
+
+@[simp] proof_wanted erase_data [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a

Std/Data/HashMap/Lemmas.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Std.Data.HashMap.Basic
+import Std.Util.ProofWanted
+
+namespace Std.HashMap
+
+@[simp] proof_wanted empty_find? [BEq α] [Hashable α] {a : α} :
+    (∅ : HashMap α β).find? a = none
+
+proof_wanted insert_find? [BEq α] [Hashable α] (m : HashMap α β) (a a' : α) (b : β) :
+    (m.insert a b).find? a' = if a' == a then some b else m.find? a'

Std/Util/ProofWanted.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+import Lean.Elab.Exception
+import Lean.Elab.Command
+import Lean.Parser
+
+
+open Lean Parser Elab Command
+
+/-- This proof would be a welcome contribution to the library!
+
+The syntax of `proof_wanted` declarations is just like that of `theorem`, but without `:=` or the
+proof. Lean checks that `proof_wanted` declarations are well-formed (e.g. it ensures that all the
+mentioned names are in scope, and that the theorem statement is a valid proposition), but they are
+discarded afterwards. This means that they cannot be used as axioms.
+
+Typical usage:
+```
+@[simp] proof_wanted empty_find? [BEq α] [Hashable α] {a : α} :
+    (∅ : HashMap α β).find? a = none
+```
+-/
+@[command_parser]
+def «proof_wanted» := leading_parser
+  declModifiers false >> "proof_wanted" >> declId >> ppIndent declSig
+
+/-- Elaborate a `proof_wanted` declaration. The declaration is translated to an axiom during
+elaboration, but it's then removed from the environment.
+-/
+@[command_elab «proof_wanted»]
+def elabProofWanted : CommandElab
+  | `($mods:declModifiers proof_wanted $name $args* : $res) => withoutModifyingEnv do
+    -- The helper axiom is used instead of `sorry` to avoid spurious warnings
+    elabCommand <| ← `(axiom helper (p : Prop) : p
+                       $mods:declModifiers
+                       theorem $name $args* : $res := helper _)
+  | _ => throwUnsupportedSyntax