如何定义任意偏序关系并证明其性质？

Question

我有一个包含所有 nullary 构造函数的简单数据类型，并希望为其定义偏序，包括 Relation.Binary.IsPartialOrder _≡_.

我的用例：类型是抽象语法树（语句、表达式、文字、项）中的排序类型，我想要一个有效向上转换术语（项≤语句、表达式）的 AST 构造函数≤ 语句，文字 ≤ 表达式).

data Sort : Set where stmt expr item lit : Sort

到目前为止我有这个：

data _≤_ : Rel Sort lzero where
    refl : {a : Sort} → a ≤ a
    trans : {a b c : Sort} → a ≤ b → b ≤ c → a ≤ c
    expr≤stmt : expr ≤ stmt
    item≤stmt : item ≤ stmt
    lit≤expr : lit ≤ expr

我可以定义 isPreorder 但不知道如何定义 antisym:

open import Agda.Primitive
open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_)
import Relation.Binary.PropositionalEquality as PropEq

module Core.Sort where

data Sort : Set where
    stmt expr item lit : Sort

data _≤_ : Rel Sort lzero where
    refl : {a : Sort} → a ≤ a
    trans : {a b c : Sort} → a ≤ b → b ≤ c → a ≤ c
    lit≤expr  : lit  ≤ expr
    expr≤stmt : expr ≤ stmt
    item≤stmt : item ≤ stmt

≤-antisymmetric : Antisymmetric _≡_ _≤_
≤-antisymmetric =
    λ { refl _ → PropEq.refl;
        _ refl → PropEq.refl;
        (trans refl x≤y) y≤x → ≤-antisymmetric x≤y y≤x;
        (trans x≤y refl) y≤x → ≤-antisymmetric x≤y y≤x;
        x≤y (trans refl y≤x) → ≤-antisymmetric x≤y y≤x;
        x≤y (trans y≤x refl) → ≤-antisymmetric x≤y y≤x;
        x≤z (trans z≤y (trans y≤w w≤x)) → _ }

我不确定在最后一个子句（以及所有类似的子句）中做什么，无论如何这都很麻烦。

我是否缺少更方便的方法来定义任意偏序？

Answer 1

注意，对于任何给定的 x 和 y，只要 x ≤ y 是可证明的，就有无限多这样的证明.例如，stmt ≤ stmt 由 refl 和 trans refl refl 等证明。这可能（但可能不会）解释为什么证明 ≤-antisymmetric 很麻烦（也许不可能）。

在任何情况下，"less than or equal"、_≼_ 的以下定义具有属性即每当 x ≼ y 可证明时，恰好有一个证明。奖励：我可以证明 antisym。

-- x ≺ y = x is contiguous to and less than y
data _≺_ : Rel Sort lzero where
    lit≺expr  : lit  ≺ expr
    expr≺stmt : expr ≺ stmt
    item≺stmt : item ≺ stmt

-- x ≼ y = x is less than or equal to y
data _≼_ : Rel Sort lzero where
    refl : {a : Sort} → a ≼ a
    trans : {a b c : Sort} → a ≺ b → b ≼ c → a ≼ c

≼-antisymmetric : Antisymmetric _≡_ _≼_
≼-antisymmetric refl _ = PropEq.refl
≼-antisymmetric _ refl = PropEq.refl
≼-antisymmetric (trans lit≺expr _)                   (trans lit≺expr _)     = PropEq.refl
≼-antisymmetric (trans lit≺expr refl)                (trans expr≺stmt (trans () _))
≼-antisymmetric (trans lit≺expr (trans expr≺stmt _)) (trans expr≺stmt (trans () _))
≼-antisymmetric (trans lit≺expr (trans expr≺stmt _)) (trans item≺stmt (trans () _))
≼-antisymmetric (trans expr≺stmt _)                  (trans expr≺stmt _) = PropEq.refl
≼-antisymmetric (trans expr≺stmt (trans () _))       (trans lit≺expr _)
≼-antisymmetric (trans expr≺stmt (trans () _))       (trans item≺stmt _)
≼-antisymmetric (trans item≺stmt (trans () _))       (trans lit≺expr _)
≼-antisymmetric (trans item≺stmt (trans () _))       (trans _ _)

如何定义任意偏序关系并证明其性质？

How to define arbitrary partial order relation and prove its properties?

proof

relation

agda

poset