自定义偏序集的对偶定义反对称性类型检查失败，求解决建议

我看到你在定义偏序集的对偶结构时，卡在了反对称性的类型检查上，咱们来一步步理清问题并修正它。

首先，先明确核心问题：你的geq定义是geq x y = leq y x，所以对偶偏序集的反对称性需要满足**「若geq x y且geq y x，则x=y」**，展开后就是leq y x ∧ leq x y → x=y——这个逻辑和原偏序集的反对称性是一致的，但你之前的写法没有正确传递前提条件，导致类型不匹配。

下面是修正后的完整代码：

structure Poset {α : Type} (leq : α → (α → Prop)) := mkPoset :: 
(reflexive: (∀x : α, (leq x x))) 
(antisymmetric : (∀x y : α, (leq x y) → (leq y x) → x = y)) 
(transitive : (∀x y z: α, (leq x y) → (leq y z) → (leq x z)))

section Poset
parameter α : Type
parameter leq : α → α → Prop
parameter poset: (Poset leq)
def geq (x: α)(y: α) := leq y x

-- 修正后的对偶偏序集定义
def dual : Poset geq := 
Poset.mkPoset
  -- 自反性：geq x x 等价于 leq x x，直接复用原偏序集的自反性
  poset.reflexive
  -- 反对称性：接收 geq x y（即 leq y x）和 geq y x（即 leq x y），调用原反对称性并调整参数顺序
  (λx y h₁ h₂, poset.antisymmetric y x h₁ h₂)
  -- 传递性：geq x y → geq y z 等价于 leq y x → leq z y，对应原传递性的 z→y→x 顺序
  (λx y z h₁ h₂, poset.transitive z y x h₂ h₁)
end Poset

关键修正点解释： #

1. 反对称性部分：
   原偏序集的反对称性签名是∀a b, leq a b → leq b a → a=b，而我们需要的对偶反对称性是∀x y, geq x y → geq y x → x=y，也就是∀x y, leq y x → leq x y → x=y。
   这里必须显式接收两个前提h₁和h₂，再把它们传递给原反对称性，同时调整原反对称性的参数为y x，这样类型就能完全匹配。

2. 传递性部分：
   原传递性是leq a b → leq b c → leq a c，对偶传递性需要的是geq x y → geq y z → geq x z，也就是leq y x → leq z y → leq z x。
   这里把原传递性的参数设为z y x，并把前提顺序调整为h₂（leq z y）和h₁（leq y x），就能推导出leq z x（即geq x z），满足传递性要求。

内容的提问来源于stack exchange，提问作者Vinothkumar Raman