Order.agda

{-# OPTIONS --universe-polymorphism #-}

module Order where

data Level : Set where
  zero : Level
  suc  : (i : Level) → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

_$_ : forall {a} {A B : Set a} -> (A -> B) -> A -> B
f $ a = f a

infixr 6 _==_
infixr 20 _$_

data N : Set where
    O : N
    S : N -> N

_==_ : forall {A : Set} -> A -> A -> Set1
a == b = (P : _ -> Set) -> P a -> P b

eqrefl : forall {A : Set} {x : A} -> x == x
eqrefl _ p = p

eqsym : forall {A : Set} {n m : A} -> n == m -> m == n
eqsym {A}{n}{m} n=m P = n=m (\l -> P l -> P n) (\x -> x) 

eqtrans : forall {A : Set} {n m l : A} -> n == m -> m == l -> n == l
eqtrans n=m m=l P Pn = m=l P (n=m P Pn)

eqsuc : {n m : N} -> n == m -> S n == S m
eqsuc n=m P = n=m (\ l -> P (S l))

cong : forall {A : Set} -> (f : A -> A) -> {x y : A} -> x == y -> f x == f y 
cong f x=y P = x=y (\y -> P (f y))

data _<=_ : N -> N -> Set1 where
    O<=x : {n : N} -> O <= n
    S<=S : {n m : N} -> n <= m -> S n <= S m

<=refl : {n : N} -> n <= n
<=refl {O} = O<=x
<=refl {S n} = S<=S (<=refl {n})

<=trans : {n m l : N} -> n <= m -> m <= l -> n <= l
<=trans O<=x _ = O<=x
<=trans (S<=S p) (S<=S q) = S<=S (<=trans p q)

<=asym : {n m : N} -> n <= m -> m <= n -> n == m
<=asym O<=x O<=x = eqrefl
<=asym (S<=S p) (S<=S q) = eqsuc (<=asym p q)

<=O : {n : N} -> n <= O -> n == O
<=O O<=x = eqrefl

infixr 8 _::_

data List (A : Set) : Set where
    [] : List A
    _::_ : A -> List A -> List A

record IsOrder {A : Set}(_<=_ : A -> A -> Set1) : Set1 where
    field
        refl : forall {a : A} -> a <= a
        trans : forall {a b c : A} -> a <= b -> b <= c -> a <= c
        asym : forall {a b : A} -> a <= b -> b <= a -> a == b

data leList (A : Set) (p : A -> A -> Set1) (Op : IsOrder p) : List A -> List A -> Set1 where
    nille : forall {l1} -> leList A p Op [] l1
    headle : forall {l1 l2}{x y} (l1<=l2 : leList A p Op l1 l2) -> (pxy : p x y) -> leList A p Op (x :: l1) (y :: l2)

leListRefl : forall {A : Set}{p : A -> A -> Set1}(Op : IsOrder p){l : List A} -> leList A p Op l l
leListRefl _  {[]} = nille
leListRefl Op {x :: xs} = headle (leListRefl Op) (IsOrder.refl Op)

leListTrans : forall {A : Set}{p : A -> A -> Set1}(Op : IsOrder p){l1 l2 l3 : List A} -> leList A p Op l1 l2 -> leList A p Op l2 l3 -> leList A p Op l1 l3
leListTrans _  {[]} nille _ = nille
leListTrans Op {x :: xs} (headle xs<=ys pxy) (headle ys<=zs pyz) = headle (leListTrans Op xs<=ys ys<=zs) (IsOrder.trans Op pxy pyz)

--leListAsym : forall {A : Set}{p : A -> A -> Set1}(Op : IsOrder p){l1 l2 : List A} -> leList A p Op l1 l2 -> leList A p Op l2 l1 -> l1 == l2
--leListAsym Op nille nille = eqrefl
--leListAsym Op (headle xs<=ys pxy) (headle ys<=xs pys) = eqcons (leListAsym Op xs<=ys ys<=zs)