-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of RefinementExample is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

open import Data.Nat.DivMod
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Function
open import Relation.Binary
open import Data.Product
open import Relation.Unary
open import Relation.Nullary
open import Data.Empty

module RefinementExample where

open import Refinement
open import Data.Sum renaming (inj₁ to l ; inj₂ to r)

_≈₂_ : _
_≈₂_ = _≡_ on _div 5

eq≈₂ : IsEquivalence _≈₂_
eq≈₂ = record { refl = refl ; sym = sym ; trans = trans }

_≺₂_ : _
_≺₂_ = _<_ on _div 5

irr≺₂≈₂ : Irreflexive _≈₂_ _≺₂_
irr≺₂≈₂ {x} {y} with x div 5 | y div 5
irr≺₂≈₂ | suc _ | suc _ = <-irrefl

resp≺₂≈₂ : _≺₂_ Respects₂ _≈₂_
resp≺₂≈₂ =  { {x} {y} {z}  aux₁ {x} {y} {z}}) ,
  λ { {x} {y} {z}  aux₂ {x} {y} {z}}
  where
    aux₁ :  {x y z}  y ≈₂ z  x ≺₂ y  x ≺₂ z
    aux₁ {x} {y} {z} with x div 5 | y div 5 | z div 5
    aux₁ | _ | _ | _ = proj₁ (resp₂ _<_)
    aux₂ :  {x y z}  y ≈₂ z  y ≺₂ x  z ≺₂ x
    aux₂ {x} {y} {z} with x div 5 | y div 5 | z div 5
    aux₂ | _ | _ | _ = proj₂ (resp₂ _<_)

ispo≈₂≺₂ : IsStrictPartialOrder _≈₂_ _≺₂_
ispo≈₂≺₂ = record {
  isEquivalence = eq≈₂ ;
  irrefl = λ { {x} {y}  irr≺₂≈₂ {x} {y}} ;
  trans = <-trans ;
  <-resp-≈ = resp≺₂≈₂ }

_≈₁_ : Rel  _
a ≈₁ b = (a / 5)  (b / 5) × (a % 5  b % 5  a % 5 + b % 5  1)

sym≈₁ : Symmetric _≈₁_
sym≈₁ {a} {b} (fst , snd) with a / 5 | b / 5 | a % 5 | b % 5
sym≈₁ {a} {b} (fst , l x) | _ | _ | _ | _ = (sym fst) , l (sym x)
sym≈₁ {a} {b} (fst , r y) | _ | _ | w | w₁ =
  (sym fst) , r (trans (+-comm w₁ w) y)

trans≈₁ : Transitive _≈₁_
trans≈₁ {a} {b} {c} _ _ with a / 5 | b / 5 | c / 5 | a % 5 | b % 5 | c % 5
trans≈₁ (refl , l refl) (refl , l refl) | _ | _ | _ | _ | _ | _ = refl , l refl
trans≈₁ (refl , l refl) (refl , r y) | _ | _ | _ | _ | _ | _ = refl , r y
trans≈₁ (refl , r y) (refl , l refl) | _ | _ | _ | _ | _ | _ = refl , r y
trans≈₁ (refl , r refl) (refl , r refl) | _ | _ | _ | zero | .1 | .0 = refl , l refl
trans≈₁ (refl , r refl) (refl , r refl) | _ | _ | _ | suc zero | .0 | .1 = refl , l refl

eq≈₁ : IsEquivalence _≈₁_
eq≈₁ = record {
  refl = refl , l refl ;
  sym = λ { {a} {b}  sym≈₁ {a} {b}};
  trans = λ { {a} {b} {c}  trans≈₁ {a} {b} {c} }}

_≺₁_ : Rel  _
a ≺₁ b = a / 5 < b / 5  (a / 5  b / 5 × a % 5 < b % 5 × ¬ b % 5  1)

trans≺₁ : Transitive _≺₁_
trans≺₁ {a} {b} {c} _ _ with a / 5 | b / 5 | c / 5 | a % 5 | b % 5 | c % 5
trans≺₁ (l x) (l x₁) | _ | _ | _ | _ | _ | _ = l (<-trans x x₁)
trans≺₁ (l x) (r (refl , _)) | _ | _ | _ | _ | _ | _ = l x
trans≺₁ (r (refl , _)) (l x) | _ | _ | _ | _ | _ | _ = l x
trans≺₁ (r (refl , u , _)) (r (refl , w , x)) | _ | _ | _ | _ | _ | _ =
  r (refl , (<-trans u w , x))

irr≈₁≺₁ : Irreflexive _≈₁_ _≺₁_
irr≈₁≺₁ {a} {b} _ _ with a / 5 | b / 5 | a % 5 | b % 5
irr≈₁≺₁ (refl , snd) (l (s≤s x)) | _ | _ | _ | _ = <-irrefl refl x
irr≈₁≺₁ (refl , l refl) (r (refl , fst , _)) | _ | _ | _ | _ = <-irrefl refl fst
irr≈₁≺₁ (refl , r y₁) (r (refl , _ , snd)) | _ | _ | zero | _ = snd y₁
irr≈₁≺₁ (refl , r refl) (r (refl , () , snd)) | _ | _ | suc zero | _

resp≺≈₁ᵣ : _≺₁_ Respectsʳ _≈₁_
resp≺≈₁ᵣ {a} {b} {c} _ _ with a / 5 | b / 5 | c / 5 | a % 5 | b % 5 | c % 5
resp≺≈₁ᵣ (refl , _) (l x) | _ | _ | _ | _ | _ | _ = l x
resp≺≈₁ᵣ (refl , l refl) (r y) | _ | _ | _ | _ | _ | _ = r y
resp≺≈₁ᵣ (refl , r refl) (r (refl , _ , snd)) | _ | _ | _ | _ | suc zero | .0 =
  ⊥-elim (snd refl)

resp≺≈₁ₗ : _≺₁_ Respectsˡ _≈₁_
resp≺≈₁ₗ {a} {b} {c} _ _ with a / 5 | b / 5 | c / 5 | a % 5 | b % 5 | c % 5
resp≺≈₁ₗ (refl , _) (l x) | _ | _ | _ | _ | _ | _ = l x
resp≺≈₁ₗ (refl , l refl) (r y) | _ | _ | _ | _ | _ | _ = r y
resp≺≈₁ₗ (refl , r refl) (r (refl , fst , snd)) | _ | _ | _ | suc _ | zero | .1 =
  r (refl , ≤∧≢⇒< fst (snd  sym) , snd)
resp≺≈₁ₗ (refl , r refl) (r (refl , _ , snd)) | _ | _ | _ | suc _ | suc zero | _ =
  r (refl , s≤s z≤n , snd)

resp≺₁≈₁ : _≺₁_ Respects₂ _≈₁_
resp≺₁≈₁ =
   { {x} {y} {z}  resp≺≈₁ᵣ {x} {y} {z}}) ,
  λ { {x} {y} {z}  resp≺≈₁ₗ {x} {y} {z}}

ispo≈₁≺₁ : IsStrictPartialOrder _≈₁_ _≺₁_
ispo≈₁≺₁ = record {
  isEquivalence = eq≈₁ ;
  irrefl = λ { {x} {y}  irr≈₁≺₁ {x} {y}} ;
  trans = λ { {x} {y} {z}  trans≺₁ {x} {y} {z}} ;
  <-resp-≈ = resp≺₁≈₁ }

aux₁ :  {a b}  a ≺₁ b  a ≺₂ b  a ≈₂ b
aux₁ {a} {b} _ with a / 5 | b / 5 | a % 5 | b % 5
aux₁ (l x) | _ | _ | _ | _ = l x
aux₁ (r (refl , _)) | _ | _ | _ | _ = r refl

aux₂ :  {a b}  a ≈₂ b  a ≈₁ b  a ≺₁ b  b ≺₁ a
aux₂ {a} {b} _ with a / 5 | b / 5 | a % 5 | b % 5
aux₂ refl | _ | _ | zero | zero = l (refl , l refl)
aux₂ refl | _ | _ | zero | suc zero = l (refl , r refl)
aux₂ refl | _ | _ | zero | suc (suc _) = r (l (r (refl , s≤s z≤n ,  ()))))
aux₂ refl | _ | _ | suc zero | zero = l (refl , r refl)
aux₂ refl | _ | _ | suc (suc _) | zero = r (r (r (refl , s≤s z≤n ,  ()))))
aux₂ refl | _ | _ | suc zero | suc zero = l (refl , l refl)
aux₂ refl | _ | _ | suc zero | suc (suc _) =
  r (l (r (refl , s≤s (s≤s z≤n) ,  ()))))
aux₂ refl | _ | _ | suc (suc w) | suc zero =
  r (r (r (refl , s≤s (s≤s z≤n) ,  ()))))
aux₂ refl | _ | _ | suc (suc w) | suc (suc w₁) with <-cmp w w₁
aux₂ refl | _ | _ | suc (suc _) | suc (suc _) | tri< a _ _ =
  r (l (r (refl , s≤s (s≤s a) ,  ()))))
aux₂ refl | _ | _ | suc (suc _) | suc (suc ._) | tri≈ _ refl _ =
  l (refl , l refl)
aux₂ refl | _ | _ | suc (suc _) | suc (suc _) | tri> _ _ c =
  r (r (r (refl , s≤s (s≤s c) ,  ()))))

refines : (_≈₁_ , _≺₁_) ≺≈ (_≈₂_ , _≺₂_)
refines = record {
  ≈₁→₂ = proj₁ ;
  ≈₂→₁ = λ { {a} {b}  aux₂ {a} {b}} ;
  ≺₁→₂ = λ { {a} {b}  aux₁ {a} {b}} ;
  ≺₂→₁ = l }