Fix the proofs the hard way

src/Init/Core.lean

@@ -101,6 +101,7 @@ instance : DecidableEq Empty := fun a => a.elim
 /-- Decidable equality for PEmpty -/
 instance : DecidableEq PEmpty := fun a => a.elim
 
+set_option genToCtorIdx false in
 /--
 Delays evaluation. The delayed code is evaluated at most once.
 
@@ -171,6 +172,8 @@ instance thunkCoe : CoeTail α (Thunk α) where
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h
 
+gen_withCtor% Thunk
+
 /-! # definitions  -/
 
 /--
@@ -616,6 +619,7 @@ class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
   sep : (α → Prop) → γ → γ
 
+set_option genToCtorIdx false in
 /--
 `Task α` is a primitive for asynchronous computation.
 It represents a computation that will resolve to a value of type `α`,
@@ -720,6 +724,8 @@ protected def bind (x : Task α) (f : α → Task β) (prio := Priority.default)
     Task β :=
   ⟨(f x.get).get⟩
 
+gen_withCtor% Task
+
 end Task
 
 /--

src/Init/Data/ByteArray/Basic.lean

@@ -15,6 +15,7 @@ public import Init.Data.Option.Basic
 @[expose] public section
 universe u
 
+set_option genToCtorIdx false in
 structure ByteArray where
   data : Array UInt8
 

src/Init/Data/Float.lean

@@ -30,6 +30,7 @@ opaque floatSpec : FloatSpec := {
   decLe := fun _ _ => inferInstanceAs (Decidable True)
 }
 
+set_option genToCtorIdx false in
 /--
 64-bit floating-point numbers.
 

src/Init/Data/Float32.lean

@@ -23,6 +23,7 @@ opaque float32Spec : FloatSpec := {
   decLe := fun _ _ => inferInstanceAs (Decidable True)
 }
 
+set_option genToCtorIdx false in
 /--
 32-bit floating-point numbers.
 

src/Init/Data/FloatArray/Basic.lean

@@ -15,6 +15,7 @@ public import Init.Data.Array.DecidableEq
 public section
 universe u
 
+set_option genToCtorIdx false in
 structure FloatArray where
   data : Array Float
 

src/Init/Data/Int/Basic.lean

@@ -31,6 +31,7 @@ This file defines the `Int` type as well as
 Division and modulus operations are defined in `Init.Data.Int.DivMod.Basic`.
 -/
 
+set_option genToCtorIdx false in
 /--
 The integers.
 

src/Init/Grind/Ring/Poly.lean

@@ -69,8 +69,19 @@ structure Power where
   deriving BEq, Repr, Inhabited, Hashable
 
 instance : LawfulBEq Power where
-  eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-  rfl := by intro a; cases a <;> simp! [BEq.beq]
+  -- These proofs are ugly mostly because the `_beq` function is not accessible
+  -- and we cannot tell `simp` to unfold them. Hopefully ony a problem until
+  -- we can derive LawfulBEq
+  rfl := by
+    intro a
+    cases a
+    · show _ && _; simp
+  eq_of_beq := by
+    intro a b
+    cases a <;> cases b
+    all_goals try intro h; cases h
+    all_goals try show (_ && _) → _; simp
+    all_goals try rfl
 
 protected noncomputable def Power.beq' (pw₁ pw₂ : Power) : Bool :=
   Power.rec (fun x₁ k₁ => Power.rec (fun x₂ k₂ => Nat.beq x₁ x₂ && Nat.beq k₁ k₂) pw₂) pw₁
@@ -96,15 +107,27 @@ inductive Mon where
   deriving BEq, Repr, Inhabited, Hashable
 
 instance : LawfulBEq Mon where
-  eq_of_beq {a} := by
-    induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-    next p₁ m₁ p₂ m₂ ih =>
-      cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*]
-      next h => exact ih h
+  -- These proofs are ugly mostly because the `_beq` function is not accessible
+  -- and we cannot tell `simp` to unfold them. Hopefully ony a problem until
+  -- we can derive LawfulBEq
   rfl := by
     intro a
-    induction a <;> simp! [BEq.beq]
-    assumption
+    induction a
+    · rfl
+    · show _ && _
+      simp [*]
+      assumption
+  eq_of_beq := by
+    intro a b
+    induction a generalizing b <;> cases b
+    · intro; rfl
+    · intro h; cases h
+    · intro h; cases h
+    next ih _ _ =>
+      change (_ &&_ ) → _
+      simp_all
+      intro h
+      exact ih
 
 protected noncomputable def Mon.beq' (m₁ : Mon) : Mon → Bool :=
   Mon.rec

src/Init/Grind/ToInt.lean

@@ -40,8 +40,23 @@ inductive IntInterval : Type where
   deriving BEq, DecidableEq, Inhabited
 
 instance : LawfulBEq IntInterval where
-   rfl := by intro a; cases a <;> simp_all! [BEq.beq]
-   eq_of_beq := by intro a b; cases a <;> cases b <;> simp_all! [BEq.beq]
+  -- These proofs are ugly mostly because the `_beq` function is not accessible
+  -- and we cannot tell `simp` to unfold them. Hopefully ony a problem until
+  -- we can derive LawfulBEq
+  rfl := by
+    intro a
+    cases a
+    · show _ && _; simp
+    · show ((_ : Int) == _); simp
+    · show ((_ : Int) == _); simp
+    · rfl
+  eq_of_beq := by
+    intro a b
+    cases a <;> cases b
+    all_goals try intro h; cases h
+    all_goals try show (_ && _) → _; simp
+    all_goals try show ((_ : Int) == _) → _; simp
+    all_goals try rfl
 
 namespace IntInterval
 

src/Init/Prelude.lean

@@ -11,6 +11,7 @@ public section
 set_option linter.missingDocs true -- keep it documented
 @[expose] section  -- Expose all defs
 
+
 /-!
 # Init.Prelude
 
@@ -1178,6 +1179,7 @@ propositional connective is `Not : Prop → Prop`.
 
 export Bool (or and not)
 
+set_option genToCtorIdx false in
 /--
 The natural numbers, starting at zero.
 
@@ -2020,6 +2022,8 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
 instance instSubNat : Sub Nat where
   sub := Nat.sub
 
+gen_withCtor% Nat
+
 /--
 Gets the word size of the current platform. The word size may be 64 or 32 bits.
 
@@ -2142,6 +2146,7 @@ instance (x y : BitVec w) : Decidable (LE.le x y) :=
 /-- The number of distinct values representable by `UInt8`, that is, `2^8 = 256`. -/
 abbrev UInt8.size : Nat := 256
 
+set_option genToCtorIdx false in
 /--
 Unsigned 8-bit integers.
 
@@ -2199,6 +2204,7 @@ instance : Inhabited UInt8 where
 /-- The number of distinct values representable by `UInt16`, that is, `2^16 = 65536`. -/
 abbrev UInt16.size : Nat := 65536
 
+set_option genToCtorIdx false in
 /--
 Unsigned 16-bit integers.
 
@@ -2257,6 +2263,7 @@ instance : Inhabited UInt16 where
 /-- The number of distinct values representable by `UInt32`, that is, `2^32 = 4294967296`. -/
 abbrev UInt32.size : Nat := 4294967296
 
+set_option genToCtorIdx false in
 /--
 Unsigned 32-bit integers.
 
@@ -2362,6 +2369,7 @@ instance : Min UInt32 := minOfLe
 /-- The number of distinct values representable by `UInt64`, that is, `2^64 = 18446744073709551616`. -/
 abbrev UInt64.size : Nat := 18446744073709551616
 
+set_option genToCtorIdx false in
 /--
 Unsigned 64-bit integers.
 
@@ -2417,6 +2425,8 @@ instance : DecidableEq UInt64 := UInt64.decEq
 instance : Inhabited UInt64 where
   default := UInt64.ofNatLT 0 (of_decide_eq_true rfl)
 
+gen_withCtor% UInt64
+
 /-- The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`. -/
 abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 
@@ -2431,6 +2441,7 @@ theorem USize.size_pos : LT.lt 0 USize.size :=
   | _, Or.inl rfl => of_decide_eq_true rfl
   | _, Or.inr rfl => of_decide_eq_true rfl
 
+set_option genToCtorIdx false in
 /--
 Unsigned integers that are the size of a word on the platform's architecture.
 
@@ -2487,6 +2498,9 @@ instance : DecidableEq USize := USize.decEq
 instance : Inhabited USize where
   default := USize.ofNatLT 0 USize.size_pos
 
+-- This fails in the compiler, but we do not need these constructions urgently here
+-- gen_withCtor% USize
+
 /--
 A `Nat` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a
 surrogate code point (the range `0xd800` to `0xdfff` inclusive).
@@ -2735,6 +2749,7 @@ def List.concat {α : Type u} : List α → α → List α
   | nil,       b => cons b nil
   | cons a as, b => cons a (concat as b)
 
+set_option genToCtorIdx false in
 /--
 A string is a sequence of Unicode code points.
 
@@ -2918,6 +2933,7 @@ def panic {α : Sort u} [Inhabited α] (msg : String) : α :=
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 
+set_option genToCtorIdx false in
 /--
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
 from `α`. This type has special support in the runtime.