2

我有一个包含所有空构造函数的简单数据类型，并希望为它定义一个偏序，包括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)) → _ }

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

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

4

1 回答 1

2

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

在任何情况下，以下“小于或等于”的定义_≼_，具有以下性质：只要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 _ _)
于 2017-05-03T12:32:01.003 回答