ab26eaf647
This PR is part 2 of the `implicit_reducible` refactoring (part 1: #12567). **Background.** When Lean checks definitional equality of function applications `f a₁ ... aₙ =?= f b₁ ... bₙ`, it compares arguments `aᵢ =?= bᵢ` at a transparency level determined by the binder type. Previously, only instance-implicit (`[C]`) arguments received a transparency bump to `.instances`. With `backward.isDefEq.implicitBump` enabled, ALL implicit arguments (`{x}`, `⦃x⦄`, and `[x]`) are bumped to `.instances`, so that definitions marked `[implicit_reducible]` unfold when comparing implicit arguments. This is important because implicit arguments often carry type information (e.g., `P (i + 0)` vs `P i`) where the mismatch is in non-proof positions (Sort arguments to `cast`) — proof irrelevance does not help here, so the relevant definitions must actually unfold. **`[implicit_reducible]`** (renamed from `[instance_reducible]` in part 1) marks definitions that should unfold at `TransparencyMode.instances` — between `[reducible]` (unfolds at `.reducible` and above) and the default `[semireducible]` (unfolds only at `.default` and above). This is the right level for core arithmetic operations that appear in type indices. ## Changes - **Enable `backward.isDefEq.implicitBump` by default** and set it in `stage0/src/stdlib_flags.h` so stage0 also compiles with it - **Mark `Nat.add`, `Nat.mul`, `Nat.sub`, `Array.size` as `[implicit_reducible]`** so they unfold when comparing implicit arguments at `.instances` transparency - **Remove redundant unification hints** (`n + 0 =?= n`, `n - 0 =?= n`, `n * 0 =?= 0`) that are now handled by `[implicit_reducible]` - **Rename all remaining `[instance_reducible]` attribute usages** to `[implicit_reducible]` across the codebase (the old name remains as an alias) - **Remove 28 `set_option backward.isDefEq.respectTransparency false in`** workarounds that are no longer needed 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
44 lines
1.6 KiB
Text
44 lines
1.6 KiB
Text
class OfNatSound (α : Type u) [Add α] [(n : Nat) → OfNat α n] : Prop where
|
||
ofNat_add (n m : Nat) : (OfNat.ofNat n : α) + OfNat.ofNat m = OfNat.ofNat (n+m)
|
||
|
||
export OfNatSound (ofNat_add)
|
||
|
||
theorem ex1 {α : Type u} [Add α] [(n : Nat) → OfNat α n] [OfNatSound α] : (10000000 : α) + 10000000 = 20000000 :=
|
||
ofNat_add ..
|
||
|
||
-- Some example structure
|
||
class S (α : Type u) extends Add α, Mul α, Zero α, One α where
|
||
add_assoc (a b c : α) : a + b + c = a + (b + c)
|
||
add_zero (a : α) : a + 0 = a
|
||
zero_add (a : α) : 0 + a = a
|
||
mul_zero (a : α) : a * 0 = 0
|
||
mul_one (a : α) : a * 1 = a
|
||
left_distrib (a b c : α) : a * (b + c) = a * b + a * c
|
||
|
||
-- Very simply default `ofNat` for `S`
|
||
protected def S.ofNat (α : Type u) [S α] : Nat → α
|
||
| 0 => 0
|
||
| n+1 => S.ofNat α n + 1
|
||
|
||
instance [S α] : OfNat α n where
|
||
ofNat := S.ofNat α n
|
||
|
||
instance [S α] : OfNatSound α where
|
||
ofNat_add n m := by
|
||
induction m with
|
||
| zero => simp [OfNat.ofNat, S.ofNat]; erw [S.add_zero]
|
||
| succ m ih => simp [OfNat.ofNat, S.ofNat] at *; erw [← ih]; rw [S.add_assoc]
|
||
|
||
theorem S.ofNat_mul [S α] (n m : Nat) : (OfNat.ofNat n : α) * OfNat.ofNat m = OfNat.ofNat (n * m) := by
|
||
induction m with
|
||
| zero => rw [Nat.mul_zero]; erw [S.mul_zero]; rfl
|
||
| succ m ih =>
|
||
show OfNat.ofNat (α := α) n * OfNat.ofNat (m + 1) = OfNat.ofNat (n * m.succ)
|
||
rw [Nat.mul_succ, ← ofNat_add, ← ofNat_add, ← ih, left_distrib]
|
||
simp [OfNat.ofNat, S.ofNat]
|
||
erw [S.zero_add, S.mul_one]
|
||
|
||
theorem ex2 [S α] : (100000000000000000 : α) * 20000000000000000 = 2000000000000000000000000000000000 :=
|
||
S.ofNat_mul ..
|
||
|
||
#print ex2
|