Skip to content

Commit 3790f8c

Browse files
kim-emkim-em
authored
chore: deduplicate Grind.RatModule and Grind.NoNatZeroDivisors (#8416)
Also adds instances from e.g. `Semiring` to `NatModule` and `Ring` to `IntModule`.
1 parent 3bf95e9 commit 3790f8c

File tree

9 files changed

+115
-90
lines changed

9 files changed

+115
-90
lines changed

‎src/Init/Grind/CommRing/Basic.lean‎

Lines changed: 39 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import Init.Data.Zero
1010
import Init.Data.Int.DivMod.Lemmas
1111
import Init.Data.Int.Pow
1212
import Init.TacticsExtra
13+
import Init.Grind.Module.Basic
1314

1415
/-!
1516
# A monolithic commutative ring typeclass for internal use in `grind`.
@@ -108,6 +109,24 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
108109
next => simp [pow_zero, mul_one]
109110
next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc]
110111

112+
instance : NatModule α where
113+
hMul a x := a * x
114+
add_zero := by simp [add_zero]
115+
zero_add := by simp [zero_add]
116+
add_assoc := by simp [add_assoc]
117+
add_comm := by simp [add_comm]
118+
zero_hmul := by simp [natCast_zero, zero_mul]
119+
one_hmul := by simp [natCast_one, one_mul]
120+
add_hmul := by simp [natCast_add, right_distrib]
121+
hmul_zero := by simp [mul_zero]
122+
hmul_add := by simp [left_distrib]
123+
mul_hmul := by simp [natCast_mul, mul_assoc]
124+
125+
theorem hmul_eq_natCast_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = (k : α) * a := rfl
126+
127+
theorem hmul_eq_ofNat_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = OfNat.ofNat k * a := by
128+
simp [ofNat_eq_natCast, hmul_eq_natCast_mul]
129+
111130
end Semiring
112131

113132
namespace Ring
@@ -243,6 +262,24 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
243262
next => simp [pow_zero, Int.pow_zero, intCast_one]
244263
next k ih => simp [pow_succ, Int.pow_succ, intCast_mul, *]
245264

265+
instance : IntModule α where
266+
hMul a x := a * x
267+
add_zero := by simp [add_zero]
268+
zero_add := by simp [zero_add]
269+
add_assoc := by simp [add_assoc]
270+
add_comm := by simp [add_comm]
271+
zero_hmul := by simp [intCast_zero, zero_mul]
272+
one_hmul := by simp [intCast_one, one_mul]
273+
add_hmul := by simp [intCast_add, right_distrib]
274+
hmul_zero := by simp [mul_zero]
275+
hmul_add := by simp [left_distrib]
276+
mul_hmul := by simp [intCast_mul, mul_assoc]
277+
neg_hmul := by simp [intCast_neg, neg_mul]
278+
neg_add_cancel := by simp [neg_add_cancel]
279+
sub_eq_add_neg := by simp [sub_eq_add_neg]
280+
281+
theorem hmul_eq_intCast_mul {α} [Ring α] {k : Int} {a : α} : HMul.hMul (α := Int) k a = (k : α) * a := rfl
282+
246283
end Ring
247284

248285
namespace CommSemiring
@@ -347,28 +384,20 @@ theorem natCast_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
347384

348385
end IsCharP
349386

350-
/--
351-
Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
352-
-/
353-
class NoNatZeroDivisors (α : Type u) [Ring α] where
354-
no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
355-
356-
export NoNatZeroDivisors (no_nat_zero_divisors)
357-
387+
-- TODO: This should be generalizable to any `IntModule α`, not just `Ring α`.
358388
theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k : Int} {a : α}
359389
: k ≠ 0 → k * a = 0 → a = 0 := by
360390
match k with
361391
| (k : Nat) =>
362392
simp [intCast_natCast]
363393
intro h₁ h₂
364394
replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
365-
rw [← ofNat_eq_natCast] at h₂
366395
exact no_nat_zero_divisors k a h₁ h₂
367396
| -(k+1 : Nat) =>
368397
rw [Int.natCast_add, ← Int.natCast_add, intCast_neg, intCast_natCast]
369398
intro _ h
370399
replace h := congrArg (-·) h; simp at h
371-
rw [← neg_mul, neg_neg, neg_zero, ← ofNat_eq_natCast] at h
400+
rw [← neg_mul, neg_neg, neg_zero, ← hmul_eq_natCast_mul] at h
372401
exact no_nat_zero_divisors (k+1) a (Nat.succ_ne_zero _) h
373402

374403
end Lean.Grind

‎src/Init/Grind/CommRing/Fin.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,11 @@ instance (n : Nat) [NeZero n] : CommRing (Fin n) where
104104
intCast_neg := Fin.intCast_neg
105105

106106
instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where
107-
ofNat_eq_zero_iff x := by simp only [OfNat.ofNat, Fin.ofNat']; simp
107+
ofNat_eq_zero_iff x := by
108+
change Fin.ofNat' _ _ = Fin.ofNat' _ _ ↔ _
109+
simp only [Fin.ofNat']
110+
simp only [Nat.zero_mod]
111+
simp only [Fin.mk.injEq]
108112

109113
end Fin
110114

‎src/Init/Grind/Module/Basic.lean‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -49,13 +49,6 @@ instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
4949
hmul_add := by simp [IntModule.hmul_add]
5050
mul_hmul := by simp [IntModule.mul_hmul] }
5151

52-
/--
53-
We keep track of rational linear combinations as integer linear combinations,
54-
but with the assurance that we can cancel the GCD of the coefficients.
55-
-/
56-
class RatModule (M : Type u) extends IntModule M where
57-
no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k * a = 0 → a = 0
58-
5952
/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
6053
class Preorder (α : Type u) extends LE α, LT α where
6154
le_refl : ∀ a : α, a ≤ a
@@ -73,4 +66,12 @@ class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
7366
hmul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k * a
7467
hmul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k * a ≤ 0
7568

69+
/--
70+
Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
71+
-/
72+
class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where
73+
no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0
74+
75+
export NoNatZeroDivisors (no_nat_zero_divisors)
76+
7677
end Lean.Grind

‎src/Init/Grind/Module/Int.lean‎

Lines changed: 1 addition & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
prelude
99
import Init.Grind.Module.Basic
10+
import Init.Grind.CommRing.Int
1011
import Init.Omega
1112

1213
/-!
@@ -15,21 +16,6 @@ import Init.Omega
1516

1617
namespace Lean.Grind
1718

18-
instance : IntModule Int where
19-
add_zero := Int.add_zero
20-
zero_add := Int.zero_add
21-
add_comm := Int.add_comm
22-
add_assoc := Int.add_assoc
23-
zero_hmul := Int.zero_mul
24-
one_hmul := Int.one_mul
25-
add_hmul := Int.add_mul
26-
neg_hmul := Int.neg_mul
27-
hmul_zero := Int.mul_zero
28-
hmul_add := Int.mul_add
29-
mul_hmul := Int.mul_assoc
30-
neg_add_cancel := Int.add_left_neg
31-
sub_eq_add_neg _ _ := Int.sub_eq_add_neg
32-
3319
instance : Preorder Int where
3420
le_refl := Int.le_refl
3521
le_trans _ _ _ := Int.le_trans

‎src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -111,8 +111,13 @@ where
111111
| trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
112112
trace_goal[grind.ring] "characteristic: {n}"
113113
pure <| some (charInst, n)
114-
let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type ringInst
115-
let noZeroDivInst? := (← trySynthInstance noZeroDivType).toOption
114+
let noZeroDivInst? ← withNewMCtxDepth do
115+
let zeroType := mkApp (mkConst ``Zero [u]) type
116+
let .some zeroInst ← trySynthInstance zeroType | return none
117+
let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
118+
let .some hmulInst ← trySynthInstance hmulType | return none
119+
let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
120+
LOption.toOption <$> trySynthInstance noZeroDivType
116121
trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
117122
let addFn ← getAddFn type u semiringInst
118123
let mulFn ← getMulFn type u semiringInst

‎tests/lean/grind/module_normalization.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ example (a b : R) : a + b = b + a := by grind
1010
example (a : R) : a + 0 = a := by grind
1111
example (a : R) : 0 + a = a := by grind
1212
example (a b c : R) : a + b + c = a + (b + c) := by grind
13-
example (a : R) : 2 • a = a + a := by grind
14-
example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
13+
example (a : R) : 2 * a = a + a := by grind
14+
example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
1515

1616
end NatModule
1717

@@ -23,10 +23,10 @@ example (a b : R) : a + b = b + a := by grind
2323
example (a : R) : a + 0 = a := by grind
2424
example (a : R) : 0 + a = a := by grind
2525
example (a b c : R) : a + b + c = a + (b + c) := by grind
26-
example (a : R) : 2 • a = a + a := by grind
27-
example (a : R) : (-2 : Int) • a = -a - a := by grind
28-
example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
29-
example (a b c : R) : 2 • (b + c) - 3 • c + b + b = c + 5 • b - 2 • c := by grind
30-
example (a b c : R) : 2 • (b + c) + (-3 : Int) • c + b + b = c + (5 : Int) • b - 2 • c := by grind
26+
example (a : R) : 2 * a = a + a := by grind
27+
example (a : R) : (-2 : Int) * a = -a - a := by grind
28+
example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
29+
example (a b c : R) : 2 * (b + c) - 3 * c + b + b = c + 5 * b - 2 * c := by grind
30+
example (a b c : R) : 2 * (b + c) + (-3 : Int) * c + b + b = c + (5 : Int) * b - 2 • c := by grind
3131

3232
end IntModule

‎tests/lean/grind/module_relations.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,20 +8,20 @@ variable (R : Type u) [IntModule R]
88

99
-- In an `IntModule`, we should be able to handle relations
1010
-- this is harder, and less important, than being able to do this in `RatModule`.
11-
example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
12-
example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
11+
example (a b : R) (h : a + b = 0) : 3 * a - 7 * b = 9 * a + a := by grind
12+
example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) + a := by grind
1313

1414
end IntModule
1515

1616
section RatModule
1717

18-
variable (R : Type u) [RatModule R]
18+
variable (R : Type u) [IntModule R] [NoNatZeroDivisors R]
1919

20-
example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
21-
example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
20+
example (a b : R) (h : a + b = 0) : 3 * a - 7 * b = 9 * a + a := by grind
21+
example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) + a := by grind
2222

2323
-- In a `RatModule` we can clear common divisors.
2424
example (a : R) (h : a + a = 0) : a = 0 := by grind
25-
example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - 3 • b := by grind
25+
example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - 3 * b := by grind
2626

2727
end RatModule

‎tests/lean/grind/ordered_modules.lean‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ open Lean.Grind
22

33
set_option grind.warning false
44

5-
variable (R : Type u) [RatModule R] [Preorder R] [IntModule.IsOrdered R]
5+
variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [Preorder R] [IntModule.IsOrdered R]
66

77
example (a b c : R) (h : a < b) : a + c < b + c := by grind
88
example (a b c : R) (h : a < b) : c + a < c + b := by grind
@@ -15,50 +15,50 @@ example (a b : R) (h : a ≤ b) : -b ≤ -a := by grind
1515
example (a b : R) (h : a ≤ b) : -a ≤ -b := by grind
1616

1717
example (a : R) (h : 0 < a) : 0 ≤ a := by grind
18-
example (a : R) (h : 0 < a) : -2 • a < 0 := by grind
18+
example (a : R) (h : 0 < a) : -2 * a < 0 := by grind
1919

2020
example (a b c : R) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c := by grind
2121
example (a b c : R) (_ : a ≤ b) (_ : b < c) : a < c := by grind
2222
example (a b c : R) (_ : a < b) (_ : b ≤ c) : a < c := by grind
2323
example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
2424

25-
example (a : R) (h : 2 • a < 0) : a < 0 := by grind
26-
example (a : R) (h : 2 • a < 0) : 0 ≤ -a := by grind
25+
example (a : R) (h : 2 * a < 0) : a < 0 := by grind
26+
example (a : R) (h : 2 * a < 0) : 0 ≤ -a := by grind
2727

2828
example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
2929
example (a b : R) (_ : a < b ∧ b < a) : False := by grind
3030
example (a b : R) (_ : a < b) : a ≠ b := by grind
3131

32-
example (a b c e v0 v1 : R) (h1 : v0 = 5 • a) (h2 : v1 = 3 • b) (h3 : v0 + v1 + c = 10 • e) :
33-
v0 + 5 • e + (v1 - 3 • e) + (c - 2 • e) = 10 • e := by
32+
example (a b c e v0 v1 : R) (h1 : v0 = 5 * a) (h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10 * e) :
33+
v0 + 5 * e + (v1 - 3 * e) + (c - 2 * e) = 10 * e := by
3434
grind
3535

3636
example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
3737
grind
38-
example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) : False := by
38+
example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
3939
grind
4040

4141
example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
4242
False := by grind
43-
example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) :
43+
example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) :
4444
False := by grind
4545

4646
example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3*y := by
4747
grind
48-
example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
48+
example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
4949
grind
5050

5151
example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
5252
grind
53-
example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) : ¬ 12 • y - 4 • z < 0 := by
53+
example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12 * y - 4 * z < 0 := by
5454
grind
5555

5656
example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
5757
grind
58-
example (x y z : R) (hx : ¬ x > 3 • y) (h2 : ¬ y > 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
58+
example (x y z : R) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
5959
grind
6060

6161
example (x y z : Nat) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
6262
grind
63-
example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
63+
example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
6464
grind

‎tests/lean/run/infoFromFailure.lean‎

Lines changed: 30 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -16,21 +16,7 @@ info: B.foo "hello" : String × String
1616
---
1717
trace: [Meta.synthInstance] ❌️ Add String
1818
[Meta.synthInstance] new goal Add String
19-
[Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
20-
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
21-
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
22-
[Meta.synthInstance] new goal Lean.Grind.IntModule String
23-
[Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
24-
[Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule String
25-
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
26-
[Meta.synthInstance] no instances for Lean.Grind.RatModule String
27-
[Meta.synthInstance.instances] #[]
28-
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
29-
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
30-
[Meta.synthInstance] new goal Lean.Grind.NatModule String
31-
[Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
32-
[Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
33-
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
19+
[Meta.synthInstance.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd, @Lean.Grind.Semiring.toAdd]
3420
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
3521
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
3622
[Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -51,6 +37,20 @@ trace: [Meta.synthInstance] ❌️ Add String
5137
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
5238
[Meta.synthInstance] no instances for Lean.Grind.CommRing String
5339
[Meta.synthInstance.instances] #[]
40+
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
41+
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
42+
[Meta.synthInstance] new goal Lean.Grind.IntModule String
43+
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.instIntModule]
44+
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.instIntModule to Lean.Grind.IntModule String
45+
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
46+
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
47+
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
48+
[Meta.synthInstance] new goal Lean.Grind.NatModule String
49+
[Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.instNatModule]
50+
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.instNatModule to Lean.Grind.NatModule String
51+
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
52+
[Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
53+
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
5454
[Meta.synthInstance] result <not-available>
5555
-/
5656
#guard_msgs in
@@ -61,21 +61,7 @@ trace: [Meta.synthInstance] ❌️ Add String
6161
/--
6262
trace: [Meta.synthInstance] ❌️ Add Bool
6363
[Meta.synthInstance] new goal Add Bool
64-
[Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
65-
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
66-
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
67-
[Meta.synthInstance] new goal Lean.Grind.IntModule Bool
68-
[Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
69-
[Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule Bool
70-
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
71-
[Meta.synthInstance] no instances for Lean.Grind.RatModule Bool
72-
[Meta.synthInstance.instances] #[]
73-
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
74-
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
75-
[Meta.synthInstance] new goal Lean.Grind.NatModule Bool
76-
[Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
77-
[Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
78-
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
64+
[Meta.synthInstance.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd, @Lean.Grind.Semiring.toAdd]
7965
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
8066
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
8167
[Meta.synthInstance] new goal Lean.Grind.Semiring Bool
@@ -96,6 +82,20 @@ trace: [Meta.synthInstance] ❌️ Add Bool
9682
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
9783
[Meta.synthInstance] no instances for Lean.Grind.CommRing Bool
9884
[Meta.synthInstance.instances] #[]
85+
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
86+
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
87+
[Meta.synthInstance] new goal Lean.Grind.IntModule Bool
88+
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.instIntModule]
89+
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.instIntModule to Lean.Grind.IntModule Bool
90+
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
91+
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
92+
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
93+
[Meta.synthInstance] new goal Lean.Grind.NatModule Bool
94+
[Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.instNatModule]
95+
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.instNatModule to Lean.Grind.NatModule Bool
96+
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
97+
[Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
98+
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
9999
[Meta.synthInstance] result <not-available>
100100
-/
101101
#guard_msgs in

0 commit comments

Comments
 (0)