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

Question

I have a simple data type with all nullary constructors and wish to define a partial order for it, including a Relation.Binary.IsPartialOrder _≡_.

My use case: the type is the type of sorts in an abstract syntax tree (statement, expression, literal, item), and i want a constructor of the AST which effectively upcasts a term (item ≤ statement, expression ≤ statement, literal ≤ expression).

data Sort : Set where stmt expr item lit : Sort

So far i have this:

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

I can define isPreorder but have no idea how to define 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)) → _ }

I'm not sure what to do in the last clause (and all further clauses like it), and in any case this is cumbersome.

Am i missing a more convenient method to define an arbitrary partial order?

Answer 1

Notice that, for any given x and y, whenever x ≤ y is provable, there are infinitely many such proofs. E.g., stmt ≤ stmt is proved by refl and by trans refl refl and so forth. This may (but probably doesn't) explain why it's troublesome (and maybe impossible) to prove ≤-antisymmetric.

In any case, the following definition of "less than or equal", _≼_, has the property that whenever x ≼ y is provable, there is exactly one proof of it. Bonus: I can prove antisym for it.

-- 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 _ _)