-- Advanced Functional Programming course 2016 Chalmers/GU
--
-- 2016-02-25 Guest lecture by Andreas Abel
--
-- Introduction to Agda
--
-- File 5: Inductive relations

module Le where

open import Data.Nat.Base using (; zero; suc)
open import Logic

-- We can define our own propositions as we can define data types.

-- The less-or-equal-than relation on natural numbers n ≤ m
-- is given as the smallest relation closed under the following
-- two rules:

data _≤_ : (n m : )  prop where
  z≤  : ∀{m}  zero  m
  s≤s : ∀{n m} (p : n  m)  suc n  suc m

-- n ≤ m is a dependent type.
-- Which derivations inhabit it depends on the values of n and m

-- Example derivation:

1≤3 : 1  3
1≤3 = s≤s z≤

¬1≤0 : ¬ (1  0)
¬1≤0 ()

-- Theorem : n ≤ n
-- By induction on n

≤refl :  n  n  n
≤refl zero = z≤
≤refl (suc n) = s≤s (≤refl n)

-- Theorem: ≤ is transitive
-- By induction on the two derivations.

≤trans :  {n m k} (p : n  m) (q : m  k)  n  k
≤trans z≤ q = z≤
≤trans (s≤s p) (s≤s q) = s≤s (≤trans p q)

-- Theorem: ≤ is total
-- By induction on n and cases on m

≤total :  n m  (n  m)  (m  n)
≤total zero m = inl z≤
≤total (suc n) zero = inr z≤
≤total (suc n) (suc m) with ≤total n m
... | inl p = inl (s≤s p)
... | inr q = inr (s≤s q)