<commit_before>module Decidable.Order

import Decidable.Decidable
import Decidable.Equality

%access public

--------------------------------------------------------------------------------
-- Utility Lemmas
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- Preorders, Posets, total Orders, Equivalencies, Congruencies
--------------------------------------------------------------------------------

class Preorder t (po : t -> t -> Type) where
  total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
  total reflexive : (a : t) -> po a a

class (Preorder t po) => Poset t (po : t -> t -> Type) where
  total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

class (Poset t to) => Ordered t (to : t -> t -> Type) where
  total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
  total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a

class (Equivalence t eq) => Congruence t (eq : t -> t -> Type) where
  total congruent : (a : t) -> 
                    (b : t) -> 
                    (f : t -> t) -> 
                    eq a b -> 
                    eq (f a) (f b)

minimum : (Ordered t to) => t -> t -> t
minimum x y with (order x y)
  | Left _ = x
  | Right _ = y

maximum : (Ordered t to) => t -> t -> t
maximum x y with (order x y)
  | Left _ = y
  | Right _ = x

--------------------------------------------------------------------------------
-- Syntactic equivalence (=)
--------------------------------------------------------------------------------

instance Preorder t ((=) {A = t} {B = t}) where
  transitive a b c = trans {a = a} {b = b} {c = c}
  reflexive a = refl

instance Equivalence t ((=) {A = t} {B = t}) where
  symmetric a b prf = sym prf

instance Congruence t ((=) {A = t} {B = t}) where
  congruent a b f = cong {a = a} {b = b} {f = f}

--------------------------------------------------------------------------------
-- Natural numbers
--------------------------------------------------------------------------------

data NatLTE : Nat -> Nat -> Type where
  nEqn   : NatLTE n n
  nLTESm : NatLTE n m -> NatLTE n (S m)

total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
                           NatLTE m n -> NatLTE n o ->
                           NatLTE m o
NatLTEIsTransitive m n n      mLTEn (nEqn) = mLTEn
NatLTEIsTransitive m n (S o)  mLTEn (nLTESm nLTEo)
  = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)

total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
NatLTEIsReflexive _ = nEqn

instance Preorder Nat NatLTE where
  transitive = NatLTEIsTransitive
  reflexive  = NatLTEIsReflexive

total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
                              NatLTE m n -> NatLTE n m -> m = n
NatLTEIsAntisymmetric n n nEqn nEqn = refl
NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible<commit_msg>Congruence over a single function instead of all functions<commit_after>module Decidable.Order

import Decidable.Decidable
import Decidable.Equality

%access public

--------------------------------------------------------------------------------
-- Utility Lemmas
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- Preorders, Posets, total Orders, Equivalencies, Congruencies
--------------------------------------------------------------------------------

class Preorder t (po : t -> t -> Type) where
  total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
  total reflexive : (a : t) -> po a a

class (Preorder t po) => Poset t (po : t -> t -> Type) where
  total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

class (Poset t to) => Ordered t (to : t -> t -> Type) where
  total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
  total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a

class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
  total congruent : (a : t) -> 
                    (b : t) -> 
                    eq a b -> 
                    eq (f a) (f b)

minimum : (Ordered t to) => t -> t -> t
minimum x y with (order x y)
  | Left _ = x
  | Right _ = y

maximum : (Ordered t to) => t -> t -> t
maximum x y with (order x y)
  | Left _ = y
  | Right _ = x

--------------------------------------------------------------------------------
-- Syntactic equivalence (=)
--------------------------------------------------------------------------------

instance Preorder t ((=) {A = t} {B = t}) where
  transitive a b c = trans {a = a} {b = b} {c = c}
  reflexive a = refl

instance Equivalence t ((=) {A = t} {B = t}) where
  symmetric a b prf = sym prf

instance Congruence t f ((=) {A = t} {B = t}) where
  congruent a b = cong {a = a} {b = b} {f = f}

--------------------------------------------------------------------------------
-- Natural numbers
--------------------------------------------------------------------------------

data NatLTE : Nat -> Nat -> Type where
  nEqn   : NatLTE n n
  nLTESm : NatLTE n m -> NatLTE n (S m)

total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
                           NatLTE m n -> NatLTE n o ->
                           NatLTE m o
NatLTEIsTransitive m n n      mLTEn (nEqn) = mLTEn
NatLTEIsTransitive m n (S o)  mLTEn (nLTESm nLTEo)
  = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)

total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
NatLTEIsReflexive _ = nEqn

instance Preorder Nat NatLTE where
  transitive = NatLTEIsTransitive
  reflexive  = NatLTEIsReflexive

total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
                              NatLTE m n -> NatLTE n m -> m = n
NatLTEIsAntisymmetric n n nEqn nEqn = refl
NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible
{'fraction_non_alphanumeric': 0.30887290167865705, 'fraction_numerical': 0.0, 'mean_word_length': 1.1874125874125874, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 108, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2242170', 'n_tokens_mistral': 1997, 'n_tokens_neox': 1917, 'n_words': 719}