6871abaa44
This PR replaces the `grind` canonicalizer with a new type-directed normalizer (`Sym.canon`) that goes inside binders and applies targeted reductions in type positions, eliminating the O(n^2) `isDefEq`-based approach. The old canonicalizer maintained a map from `(function, argument_position)` to previously seen arguments, iterating the list and calling `isDefEq` for each new argument. This produced performance problems in some goal. For example, for a goal containing `n` numeric literals, it would produce O(n^2) `isDefEq` comparisons. The new canonicalizer normalizes types directly: - **Instances**: re-synthesized via `synthInstance` with the type normalized first, so `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0` produce the same instance. - **Types**: normalized with targeted reductions — eta, projection, match/ite/cond, and Nat arithmetic (`n.succ + 1` → `n + 2`, `2 + 1` → `3`). - **Values**: traversed but not reduced, preserving lambdas for grind's beta module. The canonicalizer enters binders (the old one did not), using separate caches for type-level and value-level contexts. Propositions are not normalized to avoid interfering with grind's proposition handling. Move `SynthInstance` from `Grind` to `Sym` since the canonicalizer now lives in `Sym` and needs instance synthesis. The `Grind` namespace re-exports the key functions. Add `no_index` annotations to `val_addNat` and `val_castAdd` patterns in `Fin/Lemmas.lean` — arithmetic in type positions is now normalized, so patterns must not rely on the un-normalized form for e-matching indexing. --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
34 lines
803 B
Text
34 lines
803 B
Text
inductive Foo (α : Type) (x : α) where
|
||
| c1 : Foo α x
|
||
| c2 : Foo α x
|
||
|
||
def Foo.mk (n : Nat) : Foo (Fin (n + 1)) 0 :=
|
||
match n with
|
||
| .zero => .c1
|
||
| .succ _ => .c1
|
||
|
||
def Foo.num {α : Type} {x : α} (f : Foo α x) : Nat :=
|
||
0
|
||
|
||
/-
|
||
Issue #12140: `closeGoalWithValuesEq` must check that the two interpreted values
|
||
have the same type before calling `mkEqProof`. When equivalence classes contain
|
||
heterogeneous equalities (e.g., `0 : Fin 3` and `0 : Fin 2` merged via `HEq`),
|
||
`mkEqProof` would fail with an internal error.
|
||
-/
|
||
|
||
/--
|
||
error: `grind` failed
|
||
case grind.1
|
||
n : Nat
|
||
ih : (Foo.mk n).num = 0
|
||
h : ¬(Foo.mk (n + 1)).num = 0
|
||
h_1 : 1 = n + 1
|
||
⊢ False
|
||
-/
|
||
#guard_msgs in
|
||
theorem foo (n : Nat) : (Foo.mk n).num = 0 := by
|
||
induction n with
|
||
| zero => rfl
|
||
| succ n ih =>
|
||
grind -verbose [Foo.mk]
|