lean - 为什么这个双重poset定义不类型检查

Question

我创建了以下 poset 定义，双重定义不检查反对称。我不确定如何使它工作，有什么建议吗？

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 }