为什么这个双偏序集定义不进行类型检查

Question

我创建了以下偏序集定义，dual定义不会对反对称进行类型检查。我不知道该怎么做，有什么建议吗？

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 poset.reflexive (λx y: α, poset.antisymmetric y x) (λ x y z: α, poset.transitive z y x)
end Poset

Answer 1

让我们来看一下错误消息：

term
  λ (x y : α), poset.antisymmetric y x
has type
  ∀ (x y : α), leq y x → leq x y → y = x
but is expected to have type
  ∀ (x y : α), geq x y → geq y x → x = y

虽然假设是绝对相等的，但结论是不同的。您必须在正确的位置应用eq.symm。

def dual : Poset geq :=
{ reflexive := poset.reflexive,
  antisymmetric := λ x y h₁ h₂, eq.symm (poset.antisymmetric y x h₁ h₂),
  -- note, this is not quite correct yet either
  transitive := λ x y z, poset.transitive z y x }