Ninny

NIN.agda

open import Data.Empty renaming (⊥ to FALSE)
open import Data.Nat renaming (ℕ to Nat ; _≤_ to _<=_)
open import Data.Sum renaming (_⊎_ to Either ; inj₁ to left ; inj₂ to right)
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

module NIN where

nin : forall {m n : Nat} -> m <= n -> n <= suc m -> Either (m == n) (suc m == n)
nin z≤n z≤n = left refl
nin z≤n (s≤s z≤n) = right refl
nin (s≤s p) (s≤s q) with nin p q
... | left refl = left refl
... | right refl = right refl

nin2 : forall (m n : Nat) -> m <= n -> n <= suc m -> Either (m == n) (suc m == n)
nin2 zero zero z≤n z≤n = left refl
nin2 zero (suc .0) z≤n (s≤s z≤n) = right refl
nin2 (suc m) (suc n) (s≤s p) (s≤s q) with nin2 m n p q
nin2 (suc m) (suc .m) (s≤s p) (s≤s q) | left refl = left refl
nin2 (suc m) (suc .(suc m)) (s≤s p) (s≤s q) | right refl = right refl

nobleem : forall {n : Nat} -> 3 <= n -> n <= 4 -> Either (3 == n) (4 == n)
nobleem {n} = nin {3} {n}

data PPC {A : Set} (z : A) (s : A -> A) : A -> Set where
  is-z : PPC z s z
  is-s : (n : A) -> PPC z s (s n)

data NC {A : Set} (z : A) (s : A -> A) : A -> A -> Set where
  z-z : NC z s z z
  s-s : {m n : A} -> m == n -> NC z s (s m) (s n)

record Natty (A : Set) : Set1 where
  field
    z : A
    s : A -> A
    ppc : forall (x : A) -> PPC z s x
    nc : forall (x : A) -> s x == z -> FALSE
    uc : forall (x y : A) -> s x == s y -> x == y
    -- ind : forall (P : A -> Set) -> P z -> (forall n -> P n -> P (s n)) -> forall n -> P n
    -- rec :    forall {R : Set}      -> R   -> (R -> R)                            -> A -> R

open Natty public


data LE {A : Set} (N : Natty A) : A -> A -> Set where
  z<=s : forall {z' s' n} -> z' == z N -> s' == s N n ->  LE N z' s'
  s<=s : forall {s' s'' m n} -> s' == s N m -> s'' == s N n -> LE N m n -> LE N s' s''

ninny : forall {A} -> (N : Natty A) -> {m n : A} -> LE N m n -> LE N n (s N m) -> Either (m == n) (s N m == n)
ninny N {m} {n} p q with ppc N m | ppc N n
ninny N {.(z N)} {.(z N)} p q | is-z | is-z = left refl
ninny N {.(z N)} {.(s N n)} (z<=s x x₁) (z<=s x₂ x₃) | is-z | is-s n with nc N _ x₂
ninny N {.(z N)} {.(s N n)} (z<=s x x₁) (z<=s x₂ x₃) | is-z | is-s n | ()
ninny N {.(z N)} {.(s N n)} (z<=s x x₁) (s<=s x₂ x₃ (z<=s x₄ x₅)) | is-z | is-s n with trans (uc N _ _ x₂) x₄
ninny N {.(z N)} {.(s N (z N))} (z<=s x x₁) (s<=s x₂ x₃ (z<=s x₄ x₅)) | is-z | is-s .(z N) | refl = right refl
ninny N {.(z N)} {.(s N n)} (z<=s x x₁) (s<=s x₂ x₃ (s<=s x₄ x₅ q)) | is-z | is-s n with nc N _ (sym (trans (uc N _ _ x₃) x₅))
ninny N {.(z N)} {.(s N n)} (z<=s x x₁) (s<=s x₂ x₃ (s<=s x₄ x₅ q)) | is-z | is-s n | ()
ninny N {.(z N)} {.(s N n)} (s<=s x x₁ p) q | is-z | is-s n with nc N _ (sym x)
ninny N {.(z N)} {.(s N n)} (s<=s x x₁ p) q | is-z | is-s n | ()
ninny N {.(s N n)} {.(z N)} (z<=s x x₁) q | is-s n | is-z with nc N _ x
ninny N {.(s N n)} {.(z N)} (z<=s x x₁) q | is-s n | is-z | ()
ninny N {.(s N n)} {.(z N)} (s<=s x x₁ p) q | is-s n | is-z with nc N _ (sym x₁)
ninny N {.(s N n)} {.(z N)} (s<=s x x₁ p) q | is-s n | is-z | ()
ninny N {.(s N n)} {.(s N n₁)} (z<=s x x₁) (z<=s x₂ x₃) | is-s n | is-s n₁ with nc N _ x
ninny N {.(s N n)} {.(s N n₁)} (z<=s x x₁) (z<=s x₂ x₃) | is-s n | is-s n₁ | ()
ninny N {.(s N n)} {.(s N n₁)} (z<=s x x₁) (s<=s x₂ x₃ q) | is-s n | is-s n₁ with nc N _ x
ninny N {.(s N n)} {.(s N n₁)} (z<=s x x₁) (s<=s x₂ x₃ q) | is-s n | is-s n₁ | ()
ninny N {.(s N n)} {.(s N n₁)} (s<=s x x₁ p) (z<=s x₂ x₃) | is-s n | is-s n₁ with nc N _ x₂
ninny N {.(s N n)} {.(s N n₁)} (s<=s x x₁ p) (z<=s x₂ x₃) | is-s n | is-s n₁ | ()
ninny N {.(s N a)} {.(s N b)} (s<=s x x₁ p) (s<=s x₂ x₃ q) | is-s a | is-s b with uc N _ _ x | uc N _ _ x₁ | uc N _ _ x₂ | uc N _ _ x₃
ninny N {.(s N a)} {.(s N b)} (s<=s x x₁ p) (s<=s x₂ x₃ q) | is-s a | is-s b | refl | refl | refl | refl with ninny N p q
ninny N {.(s N a)} {.(s N a)} (s<=s x x₁ p) (s<=s x₂ x₃ q) | is-s a | is-s .a | refl | refl | refl | refl | left refl = left refl
ninny N {.(s N a)} {.(s N (s N a))} (s<=s x x₁ p) (s<=s x₂ x₃ q) | is-s a | is-s .(s N a) | refl | refl | refl | refl | right refl = right refl