max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: maintain failing grind tests about Nat as a semiring (#9501)

Browse source 
These tests (still failing until we embed a NatModule in its IntModule
envelope) had further broken because of name changes.
This commit is contained in:
Kim Morrison 2025-07-24 16:44:39 +10:00 • committed by GitHub
parent 3cde12567f
commit 68adcdb475
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/grind/experiments/nat_semiring.lean → tests/lean/grind/algebra/nat_semiring.lean
View file

@ -24,21 +24,21 @@ example {α : Type} [Lean.Grind.IntModule α] [Lean.Grind.Preorder α] [Lean.Gri
(wb : 0 ≤ b) (wc : 0 ≤ c)
(h : a = b + d * c) (w : 1 ≤ d) : a ≥ c := by
subst h
conv => rhs; rw [← IntModule.zero_add c]
conv => rhs; rw [← AddCommMonoid.zero_add c]
apply OrderedAdd.add_le_add
· exact wb
· have := OrderedAdd.hmul_int_le_hmul_int_of_le_of_le_of_nonneg_of_nonneg w (Preorder.le_refl c) (by decide) wc
rwa [IntModule.one_hmul] at this
· have := OrderedAdd.zsmul_le_zsmul_of_le_of_le_of_nonneg_of_nonneg w (Preorder.le_refl c) (by decide) wc
rwa [IntModule.one_zsmul] at this
-- We can prove this directly in an ordered NatModule, from the axioms. (But shouldn't, see below.)
example {α : Type} [Lean.Grind.NatModule α] [Lean.Grind.Preorder α] [Lean.Grind.OrderedAdd α] {a b c : α} {d : Nat}
(wb : 0 ≤ b) (wc : 0 ≤ c)
(h : a = b + d * c) (w : 1 ≤ d) : a ≥ c := by
subst h
conv => rhs; rw [← NatModule.zero_add c]
conv => rhs; rw [← AddCommMonoid.zero_add c]
apply OrderedAdd.add_le_add
· exact wb
· have := OrderedAdd.hmul_le_hmul_of_le_of_le_of_nonneg w (Preorder.le_refl c) wc
rwa [NatModule.one_hmul] at this
· have := OrderedAdd.nsmul_le_nsmul_of_le_of_le_of_nonneg w (Preorder.le_refl c) wc
rwa [NatModule.one_nsmul] at this
-- The correct proof is to embed a NatModule in its IntModule envelope.