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

feat: missing NatModule instances (#10277)

Browse source 
This PR adds the missing instances `IsPartialOrder`, `IsLinearPreorder`
and `IsLinearOrder` for `OfNatModule.Q α`.
This commit is contained in:
Leonardo de Moura 2025-09-06 11:58:02 -07:00 • committed by GitHub
parent 316ff35afd
commit 52a9fe3b67
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/Init/Grind/Module/Envelope.lean
View file

@ -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