From 52a9fe3b6753399decb685ed4e4ef819ded95a3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 6 Sep 2025 11:58:02 -0700 Subject: [PATCH] feat: missing `NatModule` instances (#10277) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the missing instances `IsPartialOrder`, `IsLinearPreorder` and `IsLinearOrder` for `OfNatModule.Q α`. --- src/Init/Grind/Module/Envelope.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean index 03745526ad..69ac854324 100644 --- a/src/Init/Grind/Module/Envelope.lean +++ b/src/Init/Grind/Module/Envelope.lean @@ -318,6 +318,29 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfNatModule.Q α) rw [this]; clear this exact OrderedAdd.add_le_add h₁ h₂ +instance [LE α] [IsPartialOrder α] [OrderedAdd α] : IsPartialOrder (OfNatModule.Q α) where + le_antisymm a b h₁ h₂ := by + induction a using Q.ind with | _ a + induction b using Q.ind with | _ b + rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩ + simp only [mk_le_mk] at h₁ h₂ + rw [AddCommMonoid.add_comm b₁ a₂, AddCommMonoid.add_comm b₂ a₁] at h₂ + have := IsPartialOrder.le_antisymm _ _ h₁ h₂ + apply Quot.sound + simp; exists 0 + rw [this] + +instance [LE α] [IsLinearPreorder α] [OrderedAdd α] : IsLinearPreorder (OfNatModule.Q α) where + le_total a b := by + induction a using Q.ind with | _ a + induction b using Q.ind with | _ b + rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩ + simp only [mk_le_mk] + rw [AddCommMonoid.add_comm b₁ a₂, AddCommMonoid.add_comm b₂ a₁] + apply le_total + +instance [LE α] [IsLinearOrder α] [OrderedAdd α] : IsLinearOrder (OfNatModule.Q α) where + attribute [-simp] Q.mk @[local simp] private theorem mk_lt_mk