text:
{- https://lists.chalmers.se/pipermail/agda/2013/006033.html http://code.haskell.org/~Saizan/unification/ 18-Nov-2013 Andrea Vezzosi -}
module Unify-monolithic-EnhancedTerm where

-- some equivalences needed to adapt Tactic.Nat to the standard library
module EquivalenceOf≤ where
  open import Agda.Builtin.Equality
  open import Agda.Builtin.Nat

  open import Data.Nat using (less-than-or-equal) renaming (_≤_ to _≤s_)
  open import Data.Nat.Properties using (≤⇒≤″; ≤″⇒≤)
  open import Prelude using (diff; id) renaming (_≤_ to _≤p_)

  open import Tactic.Nat.Generic (quote _≤p_) (quote id) (quote id) using (by)

  ≤p→≤s : ∀ {a b} → a ≤p b → a ≤s b
  ≤p→≤s (diff k b₊₁≡k₊₁+a) = ≤″⇒≤ (less-than-or-equal {k = k} (by b₊₁≡k₊₁+a))

  ≤s→≤p : ∀ {a b} → a ≤s b → a ≤p b
  ≤s→≤p a≤sb with ≤⇒≤″ a≤sb
  ≤s→≤p _ | less-than-or-equal {k = k} a+k≡b = diff k (by a+k≡b)

module _ where
  open EquivalenceOf≤
  open import Data.Nat
  open import Tactic.Nat.Generic (quote _≤_) (quote ≤s→≤p) (quote ≤p→≤s) public

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat hiding (_≤_)
--open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function
open import Relation.Nullary
--open import Data.Product
open import Data.Product renaming (map to _***_)
open import Data.Empty
open import Data.List renaming (_++_ to _++L_)

{- -- not enhanced
data Term (n : ℕ) : Set where
  i : (x : Fin n) -> Term n
  leaf : Term n
  _fork_ : (s t : Term n) -> Term n
-}

data Term (n : _) : Set where
  i : (x : Fin n) -> Term n
  function : ℕ → List (Term n) → Term n

term-function-inj₁ : ∀ {x₁ x₂} {n} {ts₁ : List (Term n)} {ts₂} → Term.function x₁ ts₁ ≡ function x₂ ts₂ → x₁ ≡ x₂
term-function-inj₁ refl = refl

term-function-inj₂ : ∀ {x₁ x₂} {n} {ts₁ : List (Term n)} {ts₂} → Term.function x₁ ts₁ ≡ function x₂ ts₂ → ts₁ ≡ ts₂
term-function-inj₂ refl = refl

--data Term (n : ℕ) (I : Size) : Set where
--  i : (x : Fin n) -> Term n I
--  function : ℕ → (J : Size< I) → SizedList J (Term n J) → Term n I
{-
data Term : ℕ -> Set where
  i : ∀ ..{n} -> (x : Fin n) -> Term n
  leaf : ∀ ..{n} -> Term n
  _fork_ : ∀ ..{n} -> (s t : Term n) -> Term n
-}
_~>_ : (m n : ℕ) -> Set
(m ~> n) = Fin m -> Term n

▹ : ∀ {m n} -> (r : Fin m -> Fin n) -> Fin m -> Term n
▹ r = i ∘ r

mutual

  infixr 20 _◃s_
  _◃s_ : ∀ {m n} -> (f : m ~> n) -> List (Term m) -> List (Term n)
  _◃s_ f [] = []
  _◃s_ f (x ∷ xs) = (f ◃ x) ∷ f ◃s xs

  _◃_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
  f ◃ (i x) = f x
  f ◃ (function n ts) = function n (f ◃s ts)

{-
_◃_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
_◃_ = _◃
-}

_≐_ : {m n : ℕ} -> (Fin m -> Term n) -> (Fin m -> Term n) -> Set
f ≐ g = ∀ x -> f x ≡ g x

mutual

  ◃ext : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ t -> f ◃ t ≡ g ◃ t
  ◃ext p (i x) = p x
  ◃ext p (function x ts) = cong (function x) (◃exts p ts)

  ◃exts : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ ts -> f ◃s ts ≡ g ◃s ts
  ◃exts p [] = refl
  ◃exts p (t ∷ ts) = cong₂ _∷_ (◃ext p t) (◃exts p ts)

_◇_ : ∀ {l m n : ℕ } -> (f : Fin m -> Term n) (g : Fin l -> Term m) -> Fin l -> Term n
f ◇ g = (f ◃_) ∘ g

≐-cong : ∀ {m n o} {f : m ~> n} {g} (h : _ ~> o) -> f ≐ g -> (h ◇ f) ≐ (h ◇ g)
≐-cong h f≐g t = cong (h ◃_) (f≐g t)

≐-sym : ∀ {m n} {f : m ~> n} {g} -> f ≐ g -> g ≐ f
≐-sym f≐g = sym ∘ f≐g

module Sub where
  mutual

    fact1 : ∀ {n} -> (t : Term n) -> i ◃ t ≡ t
    fact1 (i x) = refl
    fact1 (function x ts) = cong (function x) (fact1s ts)

    fact1s : ∀ {n} -> (ts : List (Term n)) -> i ◃s ts ≡ ts
    fact1s [] = refl
    fact1s (t ∷ ts) = cong₂ _∷_ (fact1 t) (fact1s ts)

  mutual

    fact2 : ∀ {l m n} -> (f : Fin m -> Term n) (g : _) (t : Term l)
      -> (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
    fact2 f g (i x) = refl
    fact2 f g (function x ts) = cong (function x) (fact2s f g ts)

    fact2s : ∀ {l m n} -> (f : Fin m -> Term n) (g : _) (ts : List (Term l))
      -> (f ◇ g) ◃s ts ≡ f ◃s g ◃s ts
    fact2s f g [] = refl
    fact2s f g (t ∷ ts) = cong₂ _∷_ (fact2 f g t) (fact2s f g ts)

  fact3 : ∀ {l m n} (f : Fin m -> Term n) (r : Fin l -> Fin m) -> (f ◇ (▹ r)) ≡ (f ∘ r)
  fact3 f r = refl -- ext (λ _ -> refl)

◃ext' : ∀ {m n o} {f : Fin m -> Term n}{g : Fin m -> Term o}{h} -> f ≐ (h ◇ g) -> ∀ t -> f ◃ t ≡ h ◃ (g ◃ t)
◃ext' p t = trans (◃ext p t) (Sub.fact2 _ _ t)
s : ℕ -> ℕ
s = suc

thin : ∀ {n} -> (x : Fin (s n)) (y : Fin n) -> Fin (s n)
thin zero y = suc y
thin (suc x) zero = zero
thin (suc x) (suc y) = suc (thin x y)

p : ∀ {n} -> Fin (suc (suc n)) -> Fin (suc n)
p (suc x) = x
p zero = zero

module Thin where
  fact1 : ∀ {n} x y z -> thin {n} x y ≡ thin x z -> y ≡ z
  fact1 zero y .y refl = refl
  fact1 (suc x) zero zero r = refl
  fact1 (suc x) zero (suc z) ()
  fact1 (suc x) (suc y) zero ()
  fact1 (suc x) (suc y) (suc z) r = cong suc (fact1 x y z (cong p r))

  fact2 : ∀ {n} x y -> ¬ thin {n} x y ≡ x
  fact2 zero y ()
  fact2 (suc x) zero ()
  fact2 (suc x) (suc y) r = fact2 x y (cong p r)

  fact3 : ∀{n} x y -> ¬ x ≡ y -> ∃ λ y' -> thin {n} x y' ≡ y
  fact3 zero zero ne = ⊥-elim (ne refl)
  fact3 zero (suc y) _ = y , refl
  fact3 {zero} (suc ()) _ _
  fact3 {suc n} (suc x) zero ne = zero , refl
  fact3 {suc n} (suc x) (suc y) ne with y | fact3 x y (ne ∘ cong suc)
  ... | .(thin x y') | y' , refl = suc y' , refl

open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

thick : ∀ {n} -> (x y : Fin (suc n)) -> Maybe (Fin n)
thick zero zero = nothing
thick zero (suc y) = just y
thick {zero} (suc ()) _
thick {suc _} (suc x) zero = just zero
thick {suc _} (suc x) (suc y) = suc <$> (thick x y)

open import Data.Sum

_≡Fin_ : ∀ {n} -> (x y : Fin n) -> Dec (x ≡ y)
zero ≡Fin zero = yes refl
zero ≡Fin suc y = no λ ()
suc x ≡Fin zero = no λ ()
suc {suc _} x ≡Fin suc y with x ≡Fin y
...              | yes r = yes (cong suc r)
...              | no r = no λ e -> r (cong p e)
suc {zero} () ≡Fin _

module Thick where
  half1 : ∀ {n} (x : Fin (suc n)) -> thick x x ≡ nothing
  half1 zero = refl
  half1 {suc _} (suc x) = cong (_<$>_ suc) (half1 x)
  half1 {zero} (suc ())

  half2 : ∀ {n} (x : Fin (suc n)) y -> ∀ y' -> thin x y' ≡ y -> thick x y ≡ just y'
  half2 zero zero y' ()
  half2 zero (suc y) .y refl = refl
  half2 {suc n} (suc x) zero zero refl = refl
  half2 {suc _} (suc _) zero (suc _) ()
  half2 {suc n} (suc x) (suc y) zero ()
  half2 {suc n} (suc x) (suc .(thin x y')) (suc y') refl with thick x (thin x y') | half2 x (thin x y') y' refl
  ...                                                       | .(just y')          | refl = refl
  half2 {zero} (suc ()) _ _ _

  fact1 : ∀ {n} (x : Fin (suc n)) y r
    -> thick x y ≡ r
    -> x ≡ y × r ≡ nothing ⊎ ∃ λ y' -> thin x y' ≡ y × r ≡ just y'
  fact1 x y .(thick x y) refl with x ≡Fin y
  fact1 x .x ._ refl | yes refl = inj₁ (refl , half1 x)
  ... | no el with Thin.fact3 x y el
  ...            | y' , thinxy'=y = inj₂ (y' , ( thinxy'=y , half2 x y y' thinxy'=y ))

mutual

  check : ∀{n} (x : Fin (suc n)) (t : Term (suc n)) -> Maybe (Term n)
  check x (i y) = i <$> thick x y
  check x (function v ts) = (function v) <$> checks x ts

  checks : ∀{n} (x : Fin (suc n)) (t : List (Term (suc n))) -> Maybe (List (Term n))
  checks x [] = just []
  checks x (t ∷ ts) = _∷_ <$> check x t ⊛ checks x ts

_for_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) -> Fin (suc n) -> Term n
(t' for x) y = maybe′ i t' (thick x y)

data AList : ℕ -> ℕ -> Set where
  anil : ∀ {n} -> AList n n
  _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
               -> AList (suc m) n

sub : ∀ {m n} (σ : AList m n) -> Fin m -> Term n
sub anil = i
sub (σ asnoc t' / x) = sub σ ◇ (t' for x)

_++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n
ρ ++ anil = ρ
ρ ++ (σ asnoc t' / x) = (ρ ++ σ) asnoc t' / x

++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) -> ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
++-assoc ρ σ anil = refl
++-assoc ρ σ (τ asnoc t / x) = cong (λ s -> s asnoc t / x) (++-assoc ρ σ τ)

module SubList where
  anil-id-l : ∀ {m n} (σ : AList m n) -> anil ++ σ ≡ σ
  anil-id-l anil = refl
  anil-id-l (σ asnoc t' / x) = cong (λ σ -> σ asnoc t' / x) (anil-id-l σ)

  fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> sub (ρ ++ σ) ≐ (sub ρ ◇ sub σ)
  fact1 ρ anil v = refl
  fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
    where
      t = (t' for x) v
      hyp-on-terms = ◃ext (fact1 r s) t
      ◃-assoc = Sub.fact2 (sub r) (sub s) t

_∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
  -> ∃ (AList (suc m))
(n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

flexFlex : ∀ {m} (x y : Fin m) -> ∃ (AList m)
flexFlex {suc m} x y with thick x y
...              | just y' = m , anil asnoc i y' / x
...              | nothing = suc m , anil
flexFlex {zero} () _

flexRigid : ∀ {m} (x : Fin m) (t : Term m) -> Maybe (∃(AList m))
flexRigid {suc m} x t with check x t
...                   | just t' = just (m , anil asnoc t' / x)
...                   | nothing = nothing
flexRigid {zero} () _

mutual

  amgu : ∀ {m} (s t : Term m) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))
  amgu (function x ts) (function x' ts') acc with x ≟ x'
  … | yes refl = amgus ts ts' acc
  … | no neq = nothing
  amgu (i x) (i y) (m , anil) = just (flexFlex x y)
  amgu (i x) t     (m , anil) = flexRigid x t
  amgu t     (i x) (m , anil) = flexRigid x t
  amgu s     t  (n , σ asnoc r / z) =
           (λ σ -> σ ∃asnoc r / z) <$>
             amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)

  amgus : ∀ {m} (ss ts : List (Term m)) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))
  amgus [] [] acc = just acc
  amgus [] (_ ∷ _) acc = nothing
  amgus (_ ∷ _) [] acc = nothing
  amgus (s ∷ ss) (t ∷ ts) acc = amgus ss ts =<< amgu s t acc

mgu : ∀ {m} -> (s t : Term m) -> Maybe (∃ (AList m))
mgu {m} s t = amgu s t (m , anil)

{-
open import Data.Fin using (Fin; suc; zero)
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function
open import Relation.Nullary
open import Data.Product renaming (map to _***_)
open import Data.Empty
-}
open import Data.Maybe using (maybe; maybe′; nothing; just; monad; Maybe)
open import Data.Sum
--open import Unify
--open import Data.List renaming (_++_ to _++L_)
open ≡-Reasoning
open import Category.Functor
open import Category.Monad
import Level as L
--open RawMonad (Data.Maybe.monad {L.zero})

record Σ₁ (A : Set1) (F : A -> Set) : Set1 where
  field
    π₁ : A
    π₂ : F π₁

_,,_ : ∀ {A F} (x : A) -> F x -> Σ₁ A F
x ,, b = record{ π₁ = x; π₂ = b }

open Σ₁

Property⋆ : (m : ℕ) -> Set1
Property⋆ m = ∀ {n} -> (Fin m -> Term n) -> Set

Extensional : {m : ℕ} -> Property⋆ m -> Set
Extensional P = ∀ {m f g} -> f ≐ g -> P {m} f -> P g

Property : (m : ℕ) -> Set1
Property m = Σ₁ (Property⋆ m) Extensional

prop-id : ∀ {m n} {f : _ ~> n} {P : Property m} -> π₁ P f -> π₁ P (i ◇ f)
prop-id {_} {_} {f} {P'} Pf = π₂ P' (λ x → sym (Sub.fact1 (f x))) Pf

Unifies⋆ : ∀ {m} (s t : Term m) -> Property⋆ m
Unifies⋆ s t f = f ◃ s ≡ f ◃ t

Unifies : ∀ {m} (s t : Term m) -> Property m
Unifies s t = (λ {_} -> Unifies⋆ s t) ,, λ {_} {f} {g} f≐g f◃s=f◃t ->
  begin
    g ◃ s
  ≡⟨ sym (◃ext f≐g s) ⟩
    f ◃ s
  ≡⟨ f◃s=f◃t ⟩
    f ◃ t
  ≡⟨ ◃ext f≐g t ⟩
    g ◃ t
  ∎

_∧⋆_ : ∀{m} -> (P Q : Property⋆ m) -> Property⋆ m
P ∧⋆ Q = (λ f -> P f × Q f)

_∧_ : ∀{m} -> (P Q : Property m) -> Property m
P ∧ Q = (λ {_} f -> π₁ P f × π₁ Q f) ,, λ {_} {_} {_} f≐g Pf×Qf -> π₂ P f≐g (proj₁ Pf×Qf) , π₂ Q f≐g (proj₂ Pf×Qf)

_⇔⋆_ : ∀{m} -> (P Q : Property⋆ m) -> Set
P ⇔⋆ Q = ∀ {n} f -> (P {n} f -> Q f) × (Q f -> P f)

_⇔_ : ∀{m} -> (P Q : Property m) -> Set
P ⇔ Q = ∀ {n} f -> (π₁ P {n} f -> π₁ Q f) × (π₁ Q f -> π₁ P f)

switch⋆ : ∀ {m} (P Q : Property⋆ m) -> P ⇔⋆ Q -> Q ⇔⋆ P
switch⋆ _ _ P⇔Q f = proj₂ (P⇔Q f) , proj₁ (P⇔Q f)

switch : ∀ {m} (P Q : Property m) -> P ⇔ Q -> Q ⇔ P
switch _ _ P⇔Q f = proj₂ (P⇔Q f) , proj₁ (P⇔Q f)

Nothing⋆ : ∀{m} -> (P : Property⋆ m) -> Set
Nothing⋆ P = ∀{n} f -> P {n} f -> ⊥

Nothing : ∀{m} -> (P : Property m) -> Set
Nothing P = ∀{n} f -> π₁ P {n} f -> ⊥

_[-◇⋆_] : ∀{m n} (P : Property⋆ m) (f : Fin m -> Term n) -> Property⋆ n
(P [-◇⋆ f ]) g = P (g ◇ f)

_[-◇_] : ∀{m n} (P : Property m) (f : Fin m -> Term n) -> Property n
P [-◇ f ] = (λ {_} g -> π₁ P (g ◇ f)) ,, λ {_} {f'} {g'} f'≐g' Pf'◇f -> π₂ P (◃ext f'≐g' ∘ f)  Pf'◇f

module Properties where
  fact1 : ∀ {m} {s t : Term m} -> (Unifies s t) ⇔ (Unifies t s)
  fact1 _ = sym , sym

{-
  fact1'⋆ : ∀ {m} {x1 x2} {s1 t1 : Term m} {s2 t2 : List (Term m)}
         -> Unifies⋆ (function x1 (s1 ∷ s2)) (function x2 (t1 ∷ t2)) ⇔⋆ (Unifies⋆ s1 t1 ∧⋆ Unifies⋆ (function x1 s2) (function x2 t2))
  fact1'⋆ f = (λ x → {!deconstr!}) , {!!} -- deconstr _ _ _ _ _ _ _ , {!uncurry (cong₂ function)!}
    where deconstr : ∀ {m} x1 x2 (s1 t1 : Term m) (s2 t2 : List (Term m))
                   -> function x1 (s1 ∷ s2) ≡ function x2 (t1 ∷ t2)
                   -> (x1 ≡ x2) × (s1 ≡ t1) × (s2 ≡ t2)
          deconstr x1 .x1 s1 .s1 s2 .s2 refl = refl , refl , refl
-}
{-
  fact1' : ∀ {m} {s1 s2 t1 t2 : Term m}
         -> Unifies (s1 fork s2) (t1 fork t2) ⇔ (Unifies s1 t1 ∧ Unifies s2 t2)
  fact1' f = deconstr _ _ _ _ , uncurry (cong₂ _fork_)
    where deconstr : ∀ {m} (s1 s2 t1 t2 : Term m)
                   -> (s1 fork s2) ≡ (t1 fork t2)
                   -> (s1 ≡ t1) × (s2 ≡ t2)
          deconstr s1 s2 .s1 .s2 refl = refl , refl
-}

  fact2⋆ : ∀ {m} (P Q : Property⋆ m) -> P ⇔⋆ Q -> Nothing⋆ P -> Nothing⋆ Q
  fact2⋆ P Q iff notp f q with iff f
  ...                        | (p2q , q2p) = notp f (q2p q)

  fact2 : ∀ {m} (P Q : Property m) -> P ⇔ Q -> Nothing P -> Nothing Q
  fact2 P Q iff notp f q with iff f
  ...                       | (p2q , q2p) = notp f (q2p q)

  fact3 : ∀ {m} {P : Property m} -> P ⇔ (P [-◇ i ])
  fact3 f = id , id

  fact4 : ∀{m n} {P : Property m} (f : _ -> Term n)
          -> Nothing P -> Nothing (P [-◇ f ])
  fact4 f nop g = nop (g ◇ f)

  fact5⋆ : ∀{m n} (P Q : Property⋆ _) (f : m ~> n) -> P ⇔⋆ Q -> (P [-◇⋆ f ]) ⇔⋆ (Q [-◇⋆ f ])
  fact5⋆ _ _ f P⇔Q f' = P⇔Q (f' ◇ f)

  fact5 : ∀{m n} (P Q : Property _) (f : m ~> n) -> P ⇔ Q -> (P [-◇ f ]) ⇔ (Q [-◇ f ])
  fact5 _ _ f P⇔Q f' = P⇔Q (f' ◇ f)

  fact6 : ∀{m n} P {f g : m ~> n} -> f ≐ g -> (P [-◇ f ]) ⇔ (P [-◇ g ])
  fact6 P f≐g h = π₂ P (≐-cong h f≐g) , π₂ P (≐-sym (≐-cong h f≐g))
{-
  fact5 : ∀ {l m n} {f : Fin n -> Term l} {g : Fin m -> Term n}
            {P : Property _ }
        -> (P [-◇ g ]) [-◇ f ] ⇔ P [-◇ (f ◇ g) ]
  fact5 h = {!!} , {!!}
-}

_≤_ : ∀ {m n n'} (f : Fin m -> Term n) (g : Fin m -> Term n') -> Set
f ≤ g = ∃ λ f' -> f ≐ (f' ◇ g)

module Order where

  reflex : ∀ {m n} {f : Fin m -> Term n} -> f ≤ f
  reflex = i  , λ _ -> sym (Sub.fact1 _)

  transitivity : ∀ {l m n o} {f : Fin l -> Term m}{g : _ -> Term n}
                             {h : _ -> Term o}
                   -> f ≤ g -> g ≤ h -> f ≤ h
  transitivity {l} {_} {_} {_} {f} {g} {h} (fg , pfg) (gh , pgh) =
                   fg ◇ gh , proof
    where
      proof : (x : Fin l) → f x ≡ (λ x' → fg ◃ (gh x')) ◃ (h x)
      proof x = trans z (sym (Sub.fact2 fg gh (h x)))
        where z = trans (pfg x) (cong (fg ◃_) (pgh x))

  i-max : ∀ {m n} (f : Fin m -> Term n) -> f ≤ i
  i-max f = f , λ _ -> refl

  dist : ∀{l m n o}{f : Fin l -> Term m}{g : _ -> Term n}(h : Fin o -> _) -> f ≤ g -> (f ◇ h) ≤ (g ◇ h)
  dist h (fg , pfg) = fg  , λ x -> trans (◃ext pfg (h x)) (Sub.fact2 _ _ (h x))

Max⋆ : ∀ {m} (P : Property⋆ m) -> Property⋆ m
Max⋆ P f = P f × (∀ {n} f' -> P {n} f' -> f' ≤ f)

Max : ∀ {m} (P : Property m) -> Property m
Max P' = (λ {_} → Max⋆ P) ,, λ {_} {_} {_} -> lemma1
  where
    open Σ₁ P' renaming (π₁ to P; π₂ to Peq)
    lemma1 : {m : ℕ} {f : Fin _ → Term m} {g : Fin _ → Term m} →
             f ≐ g →
             P f × ({n : ℕ} (f' : Fin _ → Term n) → P f' → f' ≤ f) →
             P g × ({n : ℕ} (f' : Fin _ → Term n) → P f' → f' ≤ g)
    lemma1 {_} {f} {g} f≐g (Pf , MaxPf) = Peq f≐g Pf , λ {_} -> lemma2
      where
        lemma2 : ∀ {n} f' → P {n} f' → ∃ λ f0 → f' ≐ (f0 ◇ g)
        lemma2 f' Pf' = f0 , λ x -> trans (f'≐f0◇f x) (cong (f0 ◃_) (f≐g x))
              where
                f0 = proj₁ (MaxPf f' Pf')
                f'≐f0◇f = proj₂ (MaxPf f' Pf')

module Max where
  fact : ∀{m}(P Q : Property m) -> P ⇔ Q -> Max P ⇔ Max Q
  fact {m} P Q a f =
   (λ maxp → pq (proj₁ maxp) , λ f' → proj₂ maxp f' ∘ qp)
    , λ maxq → qp (proj₁ maxq) , λ f'  → proj₂ maxq f' ∘ pq
    where
      pq : {n : ℕ} {f0 : Fin m → Term n} → (π₁ P f0 → π₁ Q f0)
      pq {_} {f} =  proj₁ (a f)
      qp : {n : ℕ} {f0 : Fin m → Term n} → (π₁ Q f0 → π₁ P f0)
      qp {_} {f} = proj₂ (a f)

DClosed : ∀{m} (P : Property m) -> Set
DClosed P = ∀ {n} f {o} g -> f ≤ g -> π₁ P {o} g -> π₁ P {n} f

module DClosed where

  fact1 : ∀ {m} s t -> DClosed {m} (Unifies s t)
  fact1 s t f g (f≤g , p) gs=gt =
         begin
         f ◃ s
         ≡⟨ ◃ext' p s ⟩
         f≤g ◃ (g ◃ s)
         ≡⟨ cong (f≤g ◃_) gs=gt ⟩
         f≤g ◃ (g ◃ t)
         ≡⟨ sym (◃ext' p t) ⟩
         f ◃ t
         ∎

optimist : ∀ {l m n o} (a : Fin _ -> Term n) (p : Fin _ -> Term o)
                 (q : Fin _ -> Term l) (P Q : Property m)
           -> DClosed P -> π₁ (Max (P [-◇ a ])) p
           -> π₁ (Max (Q [-◇ (p ◇ a) ])) q
           -> π₁ (Max ((P ∧ Q) [-◇ a ])) (q ◇ p)
optimist a p q P' Q' DCP (Ppa , pMax) (Qqpa , qMax) =
     (Peq (sym ∘ (Sub.fact2 _ _) ∘ a) (DCP (q ◇ (p ◇ a)) (p ◇ a) (q , λ _ -> refl) Ppa)
      , Qeq (sym ∘ (Sub.fact2 _ _) ∘ a) Qqpa )
     , λ {_} -> aux
  where
    open Σ₁ P' renaming (π₁ to P; π₂ to Peq)
    open Σ₁ Q' renaming (π₁ to Q; π₂ to Qeq)
    aux : ∀ {n} (f : _ -> Term n) -> P (f ◇ a) × Q (f ◇ a) -> f ≤ (q ◇ p)
    aux f (Pfa , Qfa) = h ,
                        λ x -> trans (f≐g◇p x) (◃ext' g≐h◇q (p x))
      where
        one = pMax f Pfa
        g = proj₁ one
        f≐g◇p = proj₂ one
        Qgpa : Q (g ◇ (p ◇ a))
        Qgpa = Qeq (λ x -> ◃ext' f≐g◇p (a x)) Qfa
        g≤q = qMax g Qgpa
        h = proj₁ g≤q
        g≐h◇q = proj₂ g≤q

module failure-propagation where

  first⋆ : ∀ {m n} (a : _ ~> n) (P Q : Property⋆ m) ->
         Nothing⋆ (P [-◇⋆ a ]) -> Nothing⋆ ((P ∧⋆ Q) [-◇⋆ a ])
  first⋆ a P' Q' noP-a f (Pfa , Qfa) = noP-a f Pfa

  first : ∀ {m n} (a : _ ~> n) (P Q : Property m) ->
         Nothing (P [-◇ a ]) -> Nothing ((P ∧ Q) [-◇ a ])
  first a P' Q' noP-a f (Pfa , Qfa) = noP-a f Pfa
{-
  second⋆ : ∀ {m n o} (a : _ ~> n) (p : _ ~> o)(P Q : Property⋆ m) ->
             (Max⋆ (P [-◇⋆ a ])) p -> Nothing⋆ (Q [-◇⋆ (p ◇ a)])
             -> Nothing⋆ ((P ∧⋆ Q) [-◇⋆ a ])
  second⋆ a p P' Q' (Ppa , pMax) noQ-p◇a f (Pfa , Qfa) = noQ-p◇a g Qgpa
       where
         f≤p = pMax f Pfa
         g = proj₁ f≤p
         f≐g◇p = proj₂ f≤p
         Qgpa : Q' (g ◇ (p ◇ a))
         Qgpa = {!!}
  {-
                                                      noQ-p◇a g Qgpa
       where
         f≤p = pMax f Pfa
         g = proj₁ f≤p
         f≐g◇p = proj₂ f≤p
         Qgpa : π₁ Q' (g ◇ (p ◇ a))
         Qgpa = π₂ Q' (◃ext' f≐g◇p ∘ a)  Qfa
  -}
-}
  second⋆ : ∀ {m n o} (a : _ ~> n) (p : _ ~> o)(P : Property⋆ m)(Q : Property m) ->
             (Max⋆ (P [-◇⋆ a ])) p -> Nothing⋆ (π₁ Q [-◇⋆ (p ◇ a)])
             -> Nothing⋆ ((P ∧⋆ π₁ Q) [-◇⋆ a ])
  second⋆ a p P' Q' (Ppa , pMax) noQ-p◇a f (Pfa , Qfa) = noQ-p◇a g Qgpa
       where
         f≤p = pMax f Pfa
         g = proj₁ f≤p
         f≐g◇p = proj₂ f≤p
         Qgpa : π₁ Q' (g ◇ (p ◇ a))
         Qgpa = π₂ Q' (◃ext' f≐g◇p ∘ a)  Qfa

  second : ∀ {m n o} (a : _ ~> n) (p : _ ~> o)(P Q : Property m) ->
             π₁ (Max (P [-◇ a ])) p -> Nothing (Q [-◇ (p ◇ a)])
             -> Nothing ((P ∧ Q) [-◇ a ])
  second a p P' Q' (Ppa , pMax) noQ-p◇a f (Pfa , Qfa) =
                                                      noQ-p◇a g Qgpa
       where
         f≤p = pMax f Pfa
         g = proj₁ f≤p
         f≐g◇p = proj₂ f≤p
         Qgpa : π₁ Q' (g ◇ (p ◇ a))
         Qgpa = π₂ Q' (◃ext' f≐g◇p ∘ a)  Qfa

trivial-problem : ∀ {m n t} {f : m ~> n} -> π₁ (Max ((Unifies t t) [-◇ f ])) i
trivial-problem = refl , λ f' _ → f' , λ _ → refl

var-elim : ∀ {m} (x : Fin (suc m)) (t' : Term _)
              -> π₁ (Max ((Unifies (i x) ((▹ (thin x) ◃_) t')))) (t' for x)
var-elim x t' = first , \{_} -> second
  where
    lemma : ∀{m}(x : Fin (suc m)) t → i ≐ ((t for x) ◇ (▹ (thin x)))
    lemma x t x' = sym (cong (maybe i t) (Thick.half2 x _ x' refl))
    first = begin
             (t' for x) ◃ (i x) ≡⟨ cong (maybe i t') (Thick.half1 x) ⟩
             t'                 ≡⟨ sym (Sub.fact1 t') ⟩
             i ◃ t'             ≡⟨ ◃ext' (lemma x t') t' ⟩
             (t' for x) ◃ ((▹ (thin x) ◃_) t') ∎

    second : ∀ {n} (f : _ ~> n) → f x ≡ f ◃ ((▹ (thin x) ◃_) t') → f ≤ (t' for x)
    second f Unifiesf = (f ∘ thin x) , third
        where
          third : ((x' : Fin _) →  f x' ≡ (f ∘ thin x) ◃ (maybe′ i t' (thick x x')))
          third x' with thick x x' | Thick.fact1 x x' (thick x x') refl
          third .x | .nothing | inj₁ (refl , refl)  =
                                       sym (begin
                                           (f ∘ thin x) ◃ t'  ≡⟨ cong (λ g -> (g ◃_) t') (sym (Sub.fact3 f (thin x))) ⟩
                                           (f ◇ (▹ (thin x))) ◃ t' ≡⟨ Sub.fact2 f (▹ (thin x)) t' ⟩
                                           f ◃ ((▹ (thin x) ◃_) t') ≡⟨ sym Unifiesf ⟩
                                           f x ∎)
          third x' | .(just y) | inj₂ (y , ( thinxy≡x' , refl))  = sym (cong f thinxy≡x')

var-elim-i : ∀ {m} (x : Fin (suc m)) (t' : Term _)
              -> π₁ (Max ((Unifies (i x) ((▹ (thin x) ◃_) t')))) (i ◇ (t' for x))
var-elim-i {m} x t = prop-id {_} {_} {t for x} {Max (Unifies (i x) ((▹ (thin x) ◃_) t))} (var-elim {m} x t)

var-elim-i-≡ : ∀ {m} {t'} (x : Fin (suc m)) t1  -> t1 ≡ (i ∘ thin x) ◃ t' -> π₁ (Max (Unifies (i x) t1)) (i ◇ (t' for x))
var-elim-i-≡ {_} {t'} x .((i ∘ thin x) ◃ t') refl = var-elim-i x t'

data Step (n : ℕ) : Set where
  step : ℕ → List (Term n) → List (Term n) → Step n

open Data.List using () renaming (map to mapL)

fmapS : ∀ {n m} (f : Term n -> Term m) (s : Step n) -> Step m
fmapS f (step x ls rs) = step x (mapL f ls) (mapL f rs)

infixl 10 _⊹_
_⊹_ : ∀ {n} (ps : List (Step n)) (t : Term n) -> Term n
([] ⊹ t)                  = t
((step x ls rs ∷ ps) ⊹ t) = function x (ls ++L (ps ⊹ t ∷ rs))

_◃S_ : ∀ {n m} (f : n ~> m) -> List (Step n) -> List (Step m)
_◃S_ f = mapL (fmapS (f ◃_))

map-[] : ∀ {n m} (f : n ~> m) ps -> f ◃S ps ≡ [] -> ps ≡ []
map-[] f [] _ = refl
map-[] f (x ∷ xs) ()

module StepM where

  lemma1 : ∀ {n} (x : Step n) xs t -> [ x ] ⊹ ( xs ⊹ t ) ≡ (x ∷ xs) ⊹ t
  lemma1 (step x ls rs) xs t = refl

  lemma2 : ∀ {n} {r} {t} {xs} (x : Step n) -> xs ⊹ t ≡ r -> ((x ∷ xs) ⊹ t ) ≡ [ x ] ⊹ r
  lemma2 (step x ls rs) eq = cong (λ t → function x (ls ++L t ∷ rs)) eq -- cong (λ t -> t fork y) eq

  fact1 : ∀ {n} ps qs (t : Term n) -> (ps ++L qs) ⊹ t ≡ ps ⊹ (qs ⊹ t)
  fact1 [] qs t = refl
  fact1 (p ∷ ps) qs t = begin (p ∷ (ps ++L qs)) ⊹ t ≡⟨ lemma2 p (fact1 ps qs t) ⟩
                              [ p ] ⊹ (ps ⊹ (qs ⊹ t)) ≡⟨ lemma1 p ps (qs ⊹ t)  ⟩
                              (p ∷ ps) ⊹ (qs ⊹ t) ∎

  lemma3 : ∀ {m n} (f : m ~> n) ls rs → f ◃s (ls ++L rs) ≡ mapL (f ◃_) ls ++L mapL (f ◃_) rs
  lemma3 f [] (r ∷ rs) = cong (f ◃ r ∷_) (lemma3 f [] rs)
  lemma3 f (l ∷ ls) rs = cong (f ◃ l ∷_) (lemma3 f ls rs)
  lemma3 f [] [] = refl

  fact2 : ∀ {m n} (f : m ~> n) t ps ->
               f ◃ (ps ⊹ t) ≡ f ◃S ps ⊹ f ◃ t
  fact2 f t [] = refl
  fact2 f t (step x [] [] ∷ xs) = cong (function x) (cong (λ section → section ∷ []) (fact2 f t xs))
  fact2 f t (step x [] (r ∷ rs) ∷ xs) rewrite lemma3 f [] rs = cong (function x) (cong₂ _∷_ (fact2 f t xs) refl)
  fact2 f t (step x (l ∷ ls) rs ∷ xs) rewrite sym $ fact2 f t xs | lemma3 f ls (xs ⊹ t ∷ rs) = cong (function x) (cong (f ◃ l ∷_) refl)

mutual

  check-prop : ∀ {m} (x : Fin (suc m)) t ->
             (∃ λ t' -> t ≡ ▹ (thin x) ◃ t' × check x t ≡ just t')
             ⊎ (∃ λ ps -> t ≡ (ps ⊹ i x) × check x t ≡ nothing)
  check-prop x (i x') with Thick.fact1 x x' (thick x x') refl
  check-prop x (i .x) | inj₁ (refl , e) = inj₂ ([] , refl , cong (_<$>_ i) e)
  ... | inj₂ (y , thinxy≡x' , thickxx'≡justy')
      = inj₁ (i y
             , cong i (sym (thinxy≡x'))
             , cong (_<$>_ i) thickxx'≡justy' )
  check-prop x (function xx ts) with checks-prop x ts
  … | inj₁ (asdf , df , er) rewrite df | er = inj₁ (function xx asdf , refl , refl)
  … | inj₂ (ls , ps , rs , ts= , checks=) rewrite ts= | checks= = inj₂ (step xx ls rs ∷ ps , refl , refl)

  checks-prop : ∀ {m} (x : Fin (suc m)) ts ->
              (∃ λ ts' -> ts ≡ (▹ (thin x) ◃s_) ts' × checks x ts ≡ just ts')
              ⊎ ∃ λ ls → ∃ λ ps → ∃ λ rs -> ts ≡ ls ++L (ps ⊹ i x) ∷ rs × checks x ts ≡ nothing -- (∃ λ pss -> ts ≡ (pss ⊹s i x) × checks x ts ≡ nothing)
  checks-prop x [] = inj₁ ([] , refl , refl)
  checks-prop x (t ∷ ts) with check-prop x t | checks-prop x ts
  … | inj₁ (t' , t= , check=) | inj₁ (ts' , ts= , checks=)
    rewrite t= | check= | ts= | checks=
    = inj₁ (t' ∷ ts' , refl , refl)
  … | inj₂ (ps , t= , check=) | _
    rewrite t= | check=
    = inj₂ ([] , ps , ts , refl , refl)
  … | _ | inj₂ (ls , ps , rs , ts= , checks=)
    rewrite ts= | checks=
    = inj₂ (t ∷ ls , ps , rs , refl , lemma (_ <$> check _ t))
    where
      lemma : ∀ {a b : Set} {y : b} (x : Maybe a) -> maybe (λ _ → y) y x ≡ y
      lemma (just x') = refl
      lemma nothing = refl

function++ : ∀ {m} {x} {t : Term m} {ls rs : List (Term m)} ps ->
                   (ps ⊹ (function x (ls ++L t ∷ rs)) ≡ (ps ++L [ step x ls rs ]) ⊹ t)
function++ [] = refl
function++ (step x ls rs ∷ ps) = cong (function x) (cong (λ t → ls ++L t ∷ rs)
  (sym $ StepM.fact1 ps (step _ _ _ ∷ []) _))

open import Data.List.Properties using (∷-injective; ∷ʳ-injective)

list-craz : ∀ {a} {A : Set a} {x : A} {xs} → x ∷ xs ≡ [] → ⊥
list-craz ()

listʳ-craz : ∀ {a} {A : Set a} {x : A} {xs} → xs ∷ʳ x ≡ [] → ⊥
listʳ-craz {x = x} {[]} ()
listʳ-craz {x = x} {x₁ ∷ xs} ()

mutual

  termSize : ∀ {m} → Term m → ℕ
  termSize (i x₁) = 1
  termSize (function x₁ x₂) = suc (termsSize x₂)

  termsSize : ∀ {m} → List (Term m) → ℕ
  termsSize [] = 0
  termsSize (x₁ ∷ x₂) = termSize x₁ + termsSize x₂

sizeFact1 : ∀ {m} (ls rs : List (Term m)) → termsSize (ls ++L rs) ≡ termsSize ls + termsSize rs
sizeFact1 [] rs = refl
sizeFact1 (x ∷ ls) rs rewrite sizeFact1 ls rs = auto

sizeFact2a : ∀ {m} (p : Step m) (ps : List (Step m)) (t : Term m)
  → termSize (ps ⊹ t) Data.Nat.≤ termSize ((p ∷ ps) ⊹ t)
sizeFact2a (step x x₁ x₂) ps t rewrite sizeFact1 x₁ (ps ⊹ t ∷ x₂) = auto

≤-trans : ∀ {x y z} → x Data.Nat.≤ y → y Data.Nat.≤ z → x Data.Nat.≤ z
≤-trans z≤n z≤n = auto
≤-trans z≤n (s≤s x₂) = auto
≤-trans (s≤s x₁) (s≤s x₂) = by (≤-trans x₁ x₂)

sizeFact2 : ∀ {m} (ps : List (Step m)) x (t : Term m) (ts : List (Term m))
  → suc (termSize t + termsSize ts) Data.Nat.≤ termSize (ps ⊹ function x (t ∷ ts))
sizeFact2 [] x t ts = auto
sizeFact2 (p ∷ ps) x t ts
  with sizeFact2 ps x t ts | sizeFact2a p ps (function x (t ∷ ts))
… | siz1 | siz2 = ≤-trans siz1 siz2 where
  open import Data.Nat.Properties

No-Cycle : ∀{m} (t : Term m) ps -> t ≡ ps ⊹ t -> ps ≡ []
No-Cycle _ [] ref = refl
No-Cycle (i x) (step x₁ x₂ x₃ ∷ ps) ()
No-Cycle (function x []) (step x' [] rs ∷ ps) ()
No-Cycle (function x []) (step x' (x₁ ∷ ls) rs ∷ ps) ()
No-Cycle (function x (t ∷ ts)) (step x' [] rs ∷ ps) r
  with No-Cycle t (ps ++L step x [] ts ∷ []) $ trans (proj₁ ∘ ∷-injective $ term-function-inj₂ r) (function++ {x = x} {t = t} {ls = []} {rs = ts} ps)
… | dfsd = ⊥-elim (listʳ-craz {x = step x [] ts} {xs = ps} dfsd)
No-Cycle (function x (t ∷ ts)) (step x' ls@(l ∷ ls') rs ∷ ps) r
  with (proj₂ ∘ ∷-injective $ term-function-inj₂ r)
… | ts=ls+ps+rs with cong termsSize ts=ls+ps+rs
… | sizs with sizeFact1 ls' (ps ⊹ function x (t ∷ ts) ∷ rs)
… | siz1 rewrite siz1 | sizs with sizeFact2 ps x t ts
… | siz2 with termsSize ts | termSize t | termsSize rs | termsSize ls' | termSize (ps ⊹ function x (t ∷ ts))
… | a | b | c | d | e rewrite sizs = refute siz2 where

module Step2 where
  fact : ∀{m} (x : Fin m) p ps -> Nothing (Unifies (i x) ((p ∷ ps) ⊹ i x))
  fact x p ps f r with No-Cycle (f x) (f ◃S (p ∷ ps)) (trans r (StepM.fact2 f (i x) (p ∷ ps)))
  ... | ()

◇-assoc : ∀ {l m n o} (f : l ~> m) (g : n ~> _) (h : o ~> _) ->
               (f ◇ (g ◇ h)) ≐ ((f ◇ g) ◇ h)
◇-assoc f g h x = sym (Sub.fact2 f g (h x))

bind-assoc : ∀ {l m n o} (f : l ~> m) (g : n ~> _) (h : o ~> _) t -> (f ◇ g) ◃ (h ◃ t) ≡ (f ◇ (g ◇ h)) ◃ t
bind-assoc f g h t = sym (begin
           (f ◇ (g ◇ h)) ◃ t  ≡⟨ ◃ext (◇-assoc f g h) t ⟩
           ((f ◇ g) ◇ h) ◃ t  ≡⟨ Sub.fact2 (f ◇ g) h t ⟩
           (f ◇ g) ◃ (h  ◃ t)
                              ∎)

step-prop : ∀ {m n} (s t : Term (suc m)) (σ : AList m n) r z ->
          (Unifies s t [-◇ sub (σ asnoc r / z) ]) ⇔ (Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub σ ])
step-prop s t σ r z f = to , from
  where
    lemma1 : ∀ t -> (f ◇ sub σ) ◃ ((r for z) ◃ t) ≡ (f ◇ (sub σ ◇ (r for z))) ◃ t
    lemma1 t = bind-assoc f (sub σ) (r for z) t
    to = λ a → begin
                 (f ◇ sub σ) ◃ ((r for z) ◃ s) ≡⟨ lemma1 s ⟩
                 (f ◇ (sub σ ◇ (r for z))) ◃ s ≡⟨ a ⟩
                 (f ◇ (sub σ ◇ (r for z))) ◃ t ≡⟨ sym (lemma1 t) ⟩
                 (f ◇ sub σ) ◃ ((r for z) ◃ t) ∎
    from = λ a → begin
                   (f ◇ (sub σ ◇ (r for z))) ◃ s ≡⟨ sym (lemma1 s) ⟩
                   (f ◇ sub σ) ◃ ((r for z) ◃ s) ≡⟨ a ⟩
                   (f ◇ sub σ) ◃ ((r for z) ◃ t) ≡⟨ lemma1 t ⟩
                   (f ◇ (sub σ ◇ (r for z))) ◃ t ∎

-- We use a view so that we need to handle fewer cases in the main proof
data Amgu : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Maybe (∃ (AList m)) -> Set where
  Flip : ∀ {m s t acc} -> amgu t s acc ≡ amgu s t acc ->
    Amgu {m} t s acc (amgu t s acc) ->   Amgu           s                       t                      acc        (amgu s t acc)
  fn-neq     : ∀ {m x y ss ts acc} -> x ≢ y →  Amgu {m} (function x ss)         (function y ts)        acc        nothing
  leaf-leaf  : ∀ {m x acc} ->            Amgu {m}       (function x [])         (function x [])        acc        (just acc)
  leaf-fork  : ∀ {m x t ts acc} ->       Amgu {m}       (function x [])         (function x (t ∷ ts))  acc        nothing
  fork-leaf  : ∀ {m x s ss acc} ->       Amgu {m}       (function x (s ∷ ss))   (function x [])        acc        nothing
  fork-fork  : ∀ {m x s ss t ts acc} →   Amgu {m}       (function x (s ∷ ss))   (function x (t ∷ ts))  acc        (amgus ss ts =<< amgu s t acc)
  var-var   : ∀ {m x y} ->               Amgu           (i x)                   (i y)                  (m , anil) (just (flexFlex x y))
  var-t : ∀ {m x t} -> i x ≢ t ->        Amgu           (i x)                   t                      (m , anil) (flexRigid x t)
  s-t : ∀{m s t n σ r z} ->              Amgu {suc m}   s                       t                      (n , σ asnoc r / z) ((λ σ -> σ ∃asnoc r / z) <$>
                                                                                amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ))

view : ∀ {m : ℕ} -> (s t : Term m) -> (acc : ∃ (AList m)) -> Amgu s t acc (amgu s t acc)
view (function x ss) (function y ts) acc with x ≟ y
view (function x []) (function .x []) acc | yes refl = leaf-leaf
view (function x []) (function .x (x₁ ∷ ts)) acc | yes refl = leaf-fork
view (function x (x₁ ∷ ss)) (function .x []) acc | yes refl = fork-leaf
view (function x (s ∷ ss)) (function .x (t ∷ ts)) acc | yes refl = fork-fork
… | no neq = fn-neq neq
view (i x) (i x₁) (proj₃ , anil) = var-var
view (i x) (i x₁) (proj₃ , (proj₄ asnoc t' / x₂)) = s-t
view (i x) (function x₁ x₂) (proj₃ , anil) = var-t (λ ())
view (i x) (function x₁ x₂) (proj₃ , (proj₄ asnoc t' / x₃)) = s-t
view (function x x₁) (i x₂) (proj₃ , anil) = Flip refl (var-t (λ ()))
view (function x x₁) (i x₂) (proj₃ , (proj₄ asnoc t' / x₃)) = s-t

amgu-Correctness : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Set
amgu-Correctness s t (l , ρ) =
    (∃ λ n → ∃ λ σ → π₁ (Max (Unifies s t [-◇ sub ρ ])) (sub σ) × amgu s t (l , ρ) ≡ just (n , σ ++ ρ ))
  ⊎ (Nothing ((Unifies s t) [-◇ sub ρ ]) ×  amgu s t (l , ρ) ≡ nothing)

amgu-Correctness⋆ : {m : ℕ} -> (s t : Term m) -> ∃ (AList m) -> Set
amgu-Correctness⋆ s t (l , ρ) =
    (∃ λ n → ∃ λ σ → π₁ (Max (Unifies s t [-◇ sub ρ ])) (sub σ) × amgu s t (l , ρ) ≡ just (n , σ ++ ρ ))
  ⊎ (Nothing ((Unifies s t) [-◇ sub ρ ]) ×  amgu s t (l , ρ) ≡ nothing)

amgu-Ccomm : ∀ {m} s t acc -> amgu {m} s t acc ≡ amgu t s acc -> amgu-Correctness s t acc -> amgu-Correctness t s acc
amgu-Ccomm s t (l , ρ) st≡ts = lemma
  where
    Unst = (Unifies s t) [-◇ sub ρ ]
    Unts = (Unifies t s) [-◇ sub ρ ]

    Unst⇔Unts : ((Unifies s t) [-◇ sub ρ ]) ⇔ ((Unifies t s) [-◇ sub ρ ])
    Unst⇔Unts = Properties.fact5 (Unifies s t) (Unifies t s) (sub ρ) (Properties.fact1 {_} {s} {t})

    lemma : amgu-Correctness s t (l , ρ) -> amgu-Correctness t s (l , ρ)
    lemma (inj₁ (n , σ , MaxUnst , amgu≡just)) =
      inj₁ (n , σ , proj₁ (Max.fact Unst Unts Unst⇔Unts (sub σ)) MaxUnst , trans (sym st≡ts) amgu≡just)
    lemma (inj₂ (NoUnst , amgu≡nothing)) =
      inj₂ ((λ {_} → Properties.fact2 Unst Unts Unst⇔Unts NoUnst) , trans (sym st≡ts) amgu≡nothing)

amgu-Ccomm⋆ : ∀ {m} s t acc -> amgu {m} s t acc ≡ amgu t s acc -> amgu-Correctness⋆ s t acc -> amgu-Correctness⋆ t s acc
amgu-Ccomm⋆ s t (l , ρ) st≡ts = lemma
  where
    Unst = (Unifies s t) [-◇ sub ρ ]
    Unts = (Unifies t s) [-◇ sub ρ ]

    Unst⇔Unts : ((Unifies s t) [-◇ sub ρ ]) ⇔ ((Unifies t s) [-◇ sub ρ ])
    Unst⇔Unts = Properties.fact5 (Unifies s t) (Unifies t s) (sub ρ) (Properties.fact1 {_} {s} {t})

    lemma : amgu-Correctness s t (l , ρ) -> amgu-Correctness t s (l , ρ)
    lemma (inj₁ (n , σ , MaxUnst , amgu≡just)) =
      inj₁ (n , σ , proj₁ (Max.fact Unst Unts Unst⇔Unts (sub σ)) MaxUnst , trans (sym st≡ts) amgu≡just)
    lemma (inj₂ (NoUnst , amgu≡nothing)) =
      inj₂ ((λ {_} → Properties.fact2 Unst Unts Unst⇔Unts NoUnst) , trans (sym st≡ts) amgu≡nothing)

amgu-c⋆ : ∀ {m s t l ρ} -> Amgu s t (l , ρ) (amgu s t (l , ρ)) ->
           (∃ λ n → ∃ λ σ → (Max⋆ ((Unifies⋆ s t) [-◇⋆ sub ρ ])) (sub σ) × amgu {m} s t (l , ρ) ≡ just (n , σ ++ ρ ))
         ⊎ (Nothing⋆ ((Unifies⋆ s t) [-◇⋆ sub ρ ])                       × amgu {m} s t (l , ρ) ≡ nothing)
amgu-c⋆ {m} {s} {t} {l} {ρ} amg with amgu s t (l , ρ)
amgu-c⋆ {m} {l = l} {ρ} leaf-leaf | _ = inj₁ (l , anil , (refl , λ f' x → f' , λ x₁ → refl) , cong (just ∘ _,_ l) (sym $ SubList.anil-id-l ρ))
amgu-c⋆ {m} {s} {t} {l} {ρ} (Flip amguts≡amgust amguts) | _ = amgu-Ccomm⋆ t s (l , ρ) amguts≡amgust (amgu-c⋆ amguts)
amgu-c⋆ {m} {l = l} {ρ} (fn-neq x₁) | _ = inj₂ ((λ f x → x₁ (term-function-inj₁ x)) , refl)
amgu-c⋆ {m} {l = l} {ρ} leaf-fork | _ = inj₂ ((λ f x → case term-function-inj₂ x of λ ()) , refl)
amgu-c⋆ {m} {l = l} {ρ} fork-leaf | _ = inj₂ (((λ f x → case term-function-inj₂ x of λ ()) , refl))
amgu-c⋆ {m} {function x1 (s1 ∷ s1s)} {function .x1 (t1 ∷ t1s)} {l = l} {ρ} fork-fork | _
  with amgu s1 t1 (l , ρ)  | amgu-c⋆ $ view s1 t1 (l , ρ)
… | nothing | inj₂ (nounify , refl) = inj₂ ((λ {n} f x → {!!}) , refl)
{-
  where
    P = Unifies⋆ (function x1 (s1 ∷ s1s)) (function x1 (t1 ∷ t1s))
    Q = (Unifies⋆ s1 t1 ∧⋆ {!Unifies⋆ s2 t2!})
    Q⇔P : Q ⇔⋆ P
    Q⇔P = switch⋆ P Q (Properties.fact1' {_} {s1} {s2} {t1} {t2})
    No[Q◇ρ]→No[P◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ]) -> Nothing⋆ (P [-◇⋆ sub ρ ])
    No[Q◇ρ]→No[P◇ρ] = Properties.fact2⋆ (Q [-◇⋆ sub ρ ]) (P [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q P (sub ρ) Q⇔P)
    No[Q◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ])
    No[Q◇ρ] = failure-propagation.first⋆ (sub ρ) (Unifies⋆ s1 t1) (Unifies⋆ s2 t2) nounify
-}
… | just x | (inj₁ x₁) = {!!}
… | nothing | inj₁ (_ , _ , _ , ())
… | just x | (inj₂ (_ , ()))
amgu-c⋆ {m} var-var | _ = {!!}
amgu-c⋆ {m} {t = t} (var-t x₁) | _ = {!!}
amgu-c⋆ {s = s} {t} {l} s-t | _ = {!!}
-- amgu-c⋆ {m} {s} {t} {l} {ρ} amg with amgu s t (l , ρ)
-- amgu-c⋆ {l = l} {ρ} leaf-leaf | ._
--   = inj₁ (l , anil , trivial-problem {_} {_} {leaf} {sub ρ} , cong (λ x -> just (l , x)) (sym (SubList.anil-id-l ρ)) )
-- amgu-c⋆ leaf-fork | .nothing = inj₂ ((λ _ () ) , refl)
-- amgu-c⋆ {m} {s1 fork s2} {t1 fork t2} {l} {ρ} fork-fork | ._
--   with amgu s1 t1 (l , ρ)  | amgu-c⋆ $ view s1 t1 (l , ρ)
-- ...  | .nothing            | inj₂ (nounify , refl) = inj₂ ((λ {_} -> No[Q◇ρ]→No[P◇ρ] No[Q◇ρ]) , refl)
--   where
--     P = Unifies⋆ (s1 fork s2) (t1 fork t2)
--     Q = (Unifies⋆ s1 t1 ∧⋆ Unifies⋆ s2 t2)
--     Q⇔P : Q ⇔⋆ P
--     Q⇔P = switch⋆ P Q (Properties.fact1' {_} {s1} {s2} {t1} {t2})
--     No[Q◇ρ]→No[P◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ]) -> Nothing⋆ (P [-◇⋆ sub ρ ])
--     No[Q◇ρ]→No[P◇ρ] = Properties.fact2⋆ (Q [-◇⋆ sub ρ ]) (P [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q P (sub ρ) Q⇔P)
--     No[Q◇ρ] : Nothing⋆ (Q [-◇⋆ sub ρ ])
--     No[Q◇ρ] = failure-propagation.first⋆ (sub ρ) (Unifies⋆ s1 t1) (Unifies⋆ s2 t2) nounify

-- ... | .(just (n , σ ++ ρ)) | inj₁ (n , σ , a , refl)
--  with amgu s2 t2 (n , σ ++ ρ) | amgu-c⋆ (view s2 t2 (n , (σ ++ ρ)))
-- ... | .nothing                | inj₂ (nounify , refl) = inj₂ ( (λ {_} -> No[Q◇ρ]→No[P◇ρ]⋆ No[Q◇ρ]⋆) , refl)
--     where
--     P⋆ = Unifies⋆ (s1 fork s2) (t1 fork t2)
--     Q⋆ = (Unifies⋆ s1 t1 ∧⋆ Unifies⋆ s2 t2)
--     Q⇔P⋆ : Q⋆ ⇔⋆ P⋆
--     Q⇔P⋆ = switch⋆ P⋆ Q⋆ (Properties.fact1'⋆ {_} {s1} {s2} {t1} {t2})
--     No[Q◇ρ]→No[P◇ρ]⋆ : Nothing⋆ (Q⋆ [-◇⋆ sub ρ ]) -> Nothing⋆ (P⋆ [-◇⋆ sub ρ ])
--     No[Q◇ρ]→No[P◇ρ]⋆ = Properties.fact2⋆ (Q⋆ [-◇⋆ sub ρ ]) (P⋆ [-◇⋆ sub ρ ]) (Properties.fact5⋆ Q⋆ P⋆ (sub ρ) Q⇔P⋆)
--     No[Q◇ρ]⋆ : Nothing⋆ (Q⋆ [-◇⋆ sub ρ ])
--     No[Q◇ρ]⋆ = failure-propagation.second⋆ (sub ρ) (sub σ) (Unifies⋆ s1 t1) (Unifies s2 t2) a
--        (λ f → nounify f ∘ π₂ (Unifies s2 t2) (cong (f ◃) ∘ sym ∘ SubList.fact1 σ ρ))
-- {-
--     No[Q◇ρ]⋆ = failure-propagation.second (sub ρ) (sub σ) (Unifies s1 t1) (Unifies s2 t2) a
-- --       (λ f Unifs2t2-f◇σ◇ρ → nounify f ((π₂ (Unifies s2 t2) (λ t → cong (f ◃) (sym (SubList.fact1 σ ρ t))) Unifs2t2-f◇σ◇ρ)))
-- --       (λ f → nounify f ∘ π₂ (Unifies s2 t2) (λ t → cong (f ◃) (sym (SubList.fact1 σ ρ t))))
--        (λ f → nounify f ∘ π₂ (Unifies s2 t2) (cong (f ◃) ∘ sym ∘ SubList.fact1 σ ρ))
-- -}
--     P = Unifies (s1 fork s2) (t1 fork t2)
--     Q = (Unifies s1 t1 ∧ Unifies s2 t2)
--     Q⇔P : Q ⇔ P
--     Q⇔P = switch P Q (Properties.fact1' {_} {s1} {s2} {t1} {t2})
--     No[Q◇ρ]→No[P◇ρ] : Nothing (Q [-◇ sub ρ ]) -> Nothing (P [-◇ sub ρ ])
--     No[Q◇ρ]→No[P◇ρ] = Properties.fact2 (Q [-◇ sub ρ ]) (P [-◇ sub ρ ]) (Properties.fact5 Q P (sub ρ) Q⇔P)
--     No[Q◇ρ] : Nothing (Q [-◇ sub ρ ])
--     No[Q◇ρ] = failure-propagation.second (sub ρ) (sub σ) (Unifies s1 t1) (Unifies s2 t2) a
--        (λ f Unifs2t2-f◇σ◇ρ → nounify f (π₂ (Unifies s2 t2) (λ t → cong (f ◃) (sym (SubList.fact1 σ ρ t))) Unifs2t2-f◇σ◇ρ))

-- ... | .(just (n1 , σ1 ++ (σ ++ ρ))) | inj₁ (n1 , σ1 , b , refl)
--     = inj₁ (n1 , σ1 ++ σ , Max[P∧Q◇ρ][σ1++σ] , cong (λ σ -> just (n1 , σ)) (++-assoc σ1 σ ρ))
--     where
--       P = Unifies s1 t1
--       Q = Unifies s2 t2
--       P∧Q = P ∧ Q
--       C = Unifies (s1 fork s2) (t1 fork t2)
--       Max[C◇ρ]⇔Max[P∧Q◇ρ] : Max (C [-◇ sub ρ ]) ⇔ Max (P∧Q [-◇ sub ρ ])
--       Max[C◇ρ]⇔Max[P∧Q◇ρ] = Max.fact (C [-◇ sub ρ ]) (P∧Q [-◇ sub ρ ]) (Properties.fact5 C P∧Q (sub ρ)
--                       (Properties.fact1' {_} {s1} {s2} {t1} {t2}))
--       Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] : Max (Q [-◇ sub (σ ++ ρ)]) ⇔ Max (Q [-◇ sub σ ◇ sub ρ ])
--       Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] = Max.fact (Q [-◇ sub (σ ++ ρ)]) (Q [-◇ sub σ ◇ sub ρ ]) (Properties.fact6 Q (SubList.fact1 σ ρ))
--       Max[P∧Q◇ρ][σ1++σ] : π₁ (Max (C [-◇ sub ρ ])) (sub (σ1 ++ σ))
--       Max[P∧Q◇ρ][σ1++σ] = π₂ (Max (C [-◇ sub ρ ])) (≐-sym (SubList.fact1 σ1 σ))
--                (proj₂ (Max[C◇ρ]⇔Max[P∧Q◇ρ] (sub σ1 ◇ sub σ))
--                       (optimist (sub ρ) (sub σ) (sub σ1) P Q (DClosed.fact1 s1 t1) a (proj₁ (Max[Q◇σ++ρ]⇔Max[Q◇σ◇ρ] (sub σ1)) b)))

-- amgu-c⋆ {suc l} {i x} {i y} (var-var) | .(just (flexFlex x y))
--    with thick x y | Thick.fact1 x y (thick x y) refl
-- ...  | .(just y') | inj₂ (y' , thinxy'≡y , refl )
--   = inj₁ (l , anil asnoc i y' / x , var-elim-i-≡ x (i y) (sym (cong i thinxy'≡y)) , refl )
-- ...  | .nothing | inj₁ ( x≡y , refl ) rewrite sym x≡y
--   = inj₁ (suc l , anil , trivial-problem {_} {_} {i x} {sub anil} , refl)
-- amgu-c⋆ {suc l} {i x} {t} (var-t ix≢t) | .(flexRigid x t)
--  with check x t | check-prop x t
-- ... | .nothing  | inj₂ ( ps , r , refl) = inj₂ ( (λ {_} -> No-Unifier )  , refl)
--   where
--     No-Unifier : {n : ℕ} (f : Fin (suc l) → Term n) → f x ≡ f ◃ t → ⊥
--     No-Unifier f fx≡f◃t = ix≢t (sym (trans r (cong (λ ps -> ps ⊹ i x) ps≡[])))
--           where
--             ps≡[] : ps ≡ []
--             ps≡[] = map-[] f ps (No-Cycle (f x) ((f ◃S) ps)
--                   (begin f x             ≡⟨ fx≡f◃t ⟩
--                          f ◃ t           ≡⟨ cong (f ◃) r ⟩
--                          f ◃ (ps ⊹ i x)  ≡⟨ StepM.fact2 f (i x) ps ⟩
--                          (f ◃S) ps ⊹ f x ∎))

-- ... | .(just t') | inj₁ (t' , r , refl) = inj₁ ( l , anil asnoc t' / x , var-elim-i-≡ x t r , refl )

-- amgu-c⋆ {suc m} {s} {t} {l} {ρ asnoc r / z} s-t
--   | .((λ x' → x' ∃asnoc r / z) <$>
--       (amgu ((r for z) ◃ s) ((r for z) ◃ t) (l , ρ)))
--   with amgu-c⋆ (view ((r for z) ◃ s) ((r for z) ◃ t) (l , ρ))
-- ... | inj₂ (nounify , ra) = inj₂ ( (λ {_} -> NoQ→NoP nounify) , cong (_<$>_ (λ x' → x' ∃asnoc r / z)) ra )
--       where
--         P = Unifies s t [-◇ sub (ρ asnoc r / z) ]
--         Q = Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub ρ ]
--         NoQ→NoP : Nothing Q → Nothing P
--         NoQ→NoP = Properties.fact2 Q P (switch P Q (step-prop s t ρ r z))
-- ... | inj₁ (n , σ , a , ra)  = inj₁ (n , σ , proj₂ (MaxP⇔MaxQ (sub σ)) a , cong (_<$>_ (λ x' → x' ∃asnoc r / z)) ra)
--       where
--         P = Unifies s t [-◇ sub (ρ asnoc r / z) ]
--         Q = Unifies ((r for z) ◃ s) ((r for z) ◃ t) [-◇ sub ρ ]
--         MaxP⇔MaxQ : Max P ⇔ Max Q
--         MaxP⇔MaxQ = Max.fact P Q (step-prop s t ρ r z)
-- amgu-c⋆ {m} {s} {t} {l} {ρ} (Flip amguts≡amgust amguts) | ._ = amgu-Ccomm⋆ t s (l , ρ) amguts≡amgust (amgu-c⋆ amguts)
-- amgu-c⋆ {zero} {i ()}  _ | _

mgu-c⋆ : ∀ {m} (s t : Term m) ->
           (∃ λ n → ∃ λ σ → (Max⋆ (Unifies⋆ s t)) (sub σ) × mgu s t ≡ just (n , σ))
         ⊎ (Nothing⋆ (Unifies⋆ s t)                         × mgu s t ≡ nothing)
mgu-c⋆ {m} s t = amgu-c⋆ (view s t (m , anil))


text:
------------------------------------------------------------------------------
-- The Collatz function: A function without a termination proof
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Program.Collatz.CollatzConditionals where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Program.Collatz.Data.Nat

------------------------------------------------------------------------------
-- The Collatz function.
postulate
  collatz    : D → D
  collatz-eq : ∀ n → collatz n ≡
                     (if (iszero₁ n)
                        then 1'
                        else (if (iszero₁ (pred₁ n))
                                then 1'
                                else (if (even n)
                                        then collatz (div n 2')
                                        else collatz (3' * n + 1'))))
{-# ATP axiom collatz-eq #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module STLC.Kovacs.Completeness where

open import STLC.Kovacs.Normalisation public
open import STLC.Kovacs.Convertibility public

--------------------------------------------------------------------------------

-- (_≈_)
infix 3 _≫_
_≫_ : ∀ {A Γ} → Γ ⊢ A → Γ ⊩ A → Set

_≫_ {⎵}      {Γ} M N = M ∼ embⁿᶠ N

_≫_ {A ⇒ B} {Γ} M f = ∀ {Γ′} → (η : Γ′ ⊇ Γ) {N : Γ′ ⊢ A} {a : Γ′ ⊩ A}
                                 (p : N ≫ a)
                              → ren η M ∙ N ≫ f η a

-- (_≈ᶜ_)
infix 3 _≫⋆_
data _≫⋆_ : ∀ {Γ Ξ} → Γ ⊢⋆ Ξ → Γ ⊩⋆ Ξ → Set
  where
    ∅   : ∀ {Γ} → ∅ {Γ = Γ} ≫⋆ ∅

    _,_ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ} {M : Γ ⊢ A} {a : Γ ⊩ A}
                    → (χ : σ ≫⋆ ρ) (p : M ≫ a)
                    → σ , M ≫⋆ ρ , a

--------------------------------------------------------------------------------

-- (_∼◾≈_)
coe≫ : ∀ {A Γ} → {M₁ M₂ : Γ ⊢ A} {a : Γ ⊩ A}
               → M₁ ∼ M₂ → M₁ ≫ a
               → M₂ ≫ a
coe≫ {⎵}      p q = p ⁻¹ ⦙ q
coe≫ {A ⇒ B} p f = λ η q →
                      coe≫ (ren∼ η p ∙∼ refl∼)
                           (f η q)

--------------------------------------------------------------------------------

-- (≈ₑ)
acc≫ : ∀ {A Γ Γ′} → (η : Γ′ ⊇ Γ)
                  → {M : Γ ⊢ A} {a : Γ ⊩ A}
                  → M ≫ a
                  → ren η M ≫ acc η a
acc≫ {⎵}      η {M} {N} p = coe ((λ N′ → ren η M ∼ N′) & (natembⁿᶠ η N ⁻¹))
                                (ren∼ η p)
acc≫ {A ⇒ B} η {M} {f} g η′
                          rewrite ren○ η′ η M ⁻¹
                          = g (η ○ η′)

-- (≈ᶜₑ)
-- NOTE: _⬖≫_ = ∂acc≫⋆
_⬖≫_ : ∀ {Γ Γ′ Ξ} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                  → (χ : σ ≫⋆ ρ) (η : Γ′ ⊇ Γ)
                  → σ ◐ η ≫⋆ ρ ⬖ η
∅       ⬖≫ η = ∅
(χ , p) ⬖≫ η = χ ⬖≫ η , acc≫ η p

--------------------------------------------------------------------------------

-- (∈≈)
get≫ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                 → σ ≫⋆ ρ → (i : Ξ ∋ A)
                 → getₛ σ i ≫ getᵥ ρ i
get≫ (χ , p) zero    = p
get≫ (χ , p) (suc i) = get≫ χ i

-- (Tm≈)
eval≫ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
                  → σ ≫⋆ ρ → (M : Ξ ⊢ A)
                  → sub σ M ≫ eval ρ M

eval≫ χ (𝓋 i)
  = get≫ χ i

eval≫ {σ = σ} χ (ƛ M) η {N} q
  = coe≫ (coe (((ƛ (ren (liftₑ η) (sub (liftₛ σ) M)) ∙ N) ∼_)
               & ( sub◑ (idₛ , N) (liftₑ η) (sub (liftₛ σ) M) ⁻¹
                 ⦙ sub● (liftₑ η ◑ (idₛ , N)) (liftₛ σ) M ⁻¹
                 ⦙ (λ σ′ → sub (σ′ , N) M)
                   & ( comp●◑ (η ◑ idₛ , N) (wkₑ idₑ) σ
                     ⦙ (σ ●_) & lid◑ (η ◑ idₛ)
                     ⦙ comp●◑ idₛ η σ ⁻¹
                     ⦙ rid● (σ ◐ η)
                     )
                 ))
              (red⇒ (ren (liftₑ η) (sub (liftₛ σ) M)) N) ⁻¹)
         (eval≫ (χ ⬖≫ η , q) M)

eval≫ {σ = σ} χ (M ∙ N)
  rewrite idren (sub σ M) ⁻¹
  = eval≫ χ M idₑ (eval≫ χ N)

--------------------------------------------------------------------------------

mutual
  -- (q≈)
  reify≫ : ∀ {A Γ} → {M : Γ ⊢ A} {a : Γ ⊩ A}
                   → (p : M ≫ a)
                   → M ∼ embⁿᶠ (reify a)
  reify≫ {⎵}      {M = M} p = p
  reify≫ {A ⇒ B} {M = M} f = exp⇒ M
                            ⦙ ƛ∼ (reify≫ (f (wkₑ idₑ) (reflect≫ 0)))

  -- (u≈)
  reflect≫ : ∀ {A Γ} → (M : Γ ⊢ⁿᵉ A)
                     → embⁿᵉ M ≫ reflect M
  reflect≫ {⎵}      M = refl∼
  reflect≫ {A ⇒ B} M η {N} {a} p
                      rewrite natembⁿᵉ η M ⁻¹
                      = coe≫ (refl∼ ∙∼ reify≫ p ⁻¹)
                             (reflect≫ (renⁿᵉ η M ∙ reify a))

-- (uᶜ≈)
id≫⋆ : ∀ {Γ} → idₛ {Γ} ≫⋆ idᵥ
id≫⋆ {∅}     = ∅
id≫⋆ {Γ , A} = id≫⋆ ⬖≫ wkₑ idₑ , reflect≫ 0

complete : ∀ {Γ A} → (M : Γ ⊢ A)
                   → M ∼ embⁿᶠ (nf M)
complete M = coe ((_∼ embⁿᶠ (reify (eval idᵥ M))) & idsub M)
                 (reify≫ (eval≫ id≫⋆ M))

--------------------------------------------------------------------------------

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------
-- Upper bounds of colists containing natural numbers
------------------------------------------------------------------------

module Upper-bounds where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Colist equality-with-J as Colist
open import Conat equality-with-J as Conat
  hiding (pred) renaming (_+_ to _⊕_; _∸_ to _⊖_)
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import Nat equality-with-J as Nat using (_≤_; _<_; pred)
open import Omniscience equality-with-J

------------------------------------------------------------------------
-- Upper bounds

-- [ ∞ ] ms ⊑ n means that n is an upper bound of every number in ms.

infix 4 [_]_⊑_ [_]_⊑′_

[_]_⊑_ : Size → Colist ℕ ∞ → Conat ∞ → Type
[ i ] ms ⊑ n = □ i (λ m → [ ∞ ] ⌜ m ⌝ ≤ n) ms

[_]_⊑′_ : Size → Colist ℕ ∞ → Conat ∞ → Type
[ i ] ms ⊑′ n = □′ i (λ m → [ ∞ ] ⌜ m ⌝ ≤ n) ms

-- The conatural number infinity is always an upper bound.

infix 4 _⊑infinity

_⊑infinity : ∀ {i} ns → [ i ] ns ⊑ infinity
_⊑infinity = □-replicate (_≤infinity ∘ ⌜_⌝)

-- A form of transitivity.

transitive-⊑≤ :
  ∀ {i ms n o} → [ i ] ms ⊑ n → [ ∞ ] n ≤ o → [ i ] ms ⊑ o
transitive-⊑≤ p q = □-map (flip transitive-≤ q) p

-- Another form of transitivity.

transitive-◇≤⊑ :
  ∀ {m ns o i} → ◇ i (m ≤_) ns → [ i ] ns ⊑ o → [ i ] ⌜ m ⌝ ≤ o
transitive-◇≤⊑ {m} {ns} {o} {i} = curry (
  ◇ i (m ≤_) ns × [ i ] ns ⊑ o       ↝⟨ Σ-map id swap ∘ uncurry □◇-witness ∘ swap ⟩
  (∃ λ n → m ≤ n × [ i ] ⌜ n ⌝ ≤ o)  ↝⟨ (λ { (_ , m≤n , n≤o) → transitive-≤ (⌜⌝-mono m≤n) n≤o }) ⟩□
  [ i ] ⌜ m ⌝ ≤ o                    □)

-- If m is an upper bound of ms, and no natural number is an upper
-- bound, then m is bisimilar to infinity.

no-finite→infinite :
  ∀ {m ms} →
  (∀ n → ¬ [ ∞ ] ms ⊑ ⌜ n ⌝) →
  [ ∞ ] ms ⊑ m →
  Conat.[ ∞ ] m ∼ infinity
no-finite→infinite {m} {ms} no-finite =
  [ ∞ ] ms ⊑ m               ↝⟨ (λ ms⊑n → uncurry λ n →

      Conat.[ ∞ ] m ∼ ⌜ n ⌝        ↝⟨ ∼→≤ ⟩
      [ ∞ ] m ≤ ⌜ n ⌝              ↝⟨ transitive-⊑≤ ms⊑n ⟩
      [ ∞ ] ms ⊑ ⌜ n ⌝             ↝⟨ no-finite n ⟩□
      ⊥                            □) ⟩

  Infinite m                 ↝⟨ Infinite→∼infinity ⟩□
  Conat.[ ∞ ] m ∼ infinity   □

-- No natural number is an upper bound of nats.

nats⋢ : ∀ n → ¬ [ ∞ ] nats ⊑ ⌜ n ⌝
nats⋢ zero =
  [ ∞ ] nats ⊑ ⌜ 0 ⌝         ↝⟨ □-head ∘ □-tail ⟩
  Conat.[ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝  ↝⟨ ≮0 ⟩□
  ⊥                          □
nats⋢ (suc n) =
  [ ∞ ] nats ⊑ ⌜ suc n ⌝          ↝⟨ □-tail ⟩
  [ ∞ ] map suc nats ⊑ ⌜ suc n ⌝  ↝⟨ □-map′ (⌜⌝-mono ∘ Nat.suc≤suc⁻¹ ∘ ⌜⌝-mono⁻¹) ⟩
  [ ∞ ] map id nats ⊑ ⌜ id n ⌝    ↝⟨ □-∼ (map-id _) ⟩
  [ ∞ ] nats ⊑ ⌜ n ⌝              ↝⟨ nats⋢ n ⟩□
  ⊥                               □

-- The number ⌜ n ⌝ is an upper bound of replicate m n.

replicate⊑ : ∀ {i} m {n} → [ i ] replicate m n ⊑ ⌜ n ⌝
replicate⊑ {i} zero    {n} = []
replicate⊑ {i} (suc m) {n} =                                      $⟨ (λ { _ refl → reflexive-≤ _ }) ⟩
  (∀ o → o ≡ n → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝)                             ↝⟨ (λ hyp _ → hyp _ ∘ _⇔_.to ◇-replicate-suc⇔) ⟩
  (∀ o → ◇ i (o ≡_) (replicate (suc m) n) → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝)  ↔⟨⟩
  (∀ o → [ i ] o ∈ replicate (suc m) n → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝)     ↝⟨ _⇔_.from □⇔∈→ ⟩
  □ i (λ o → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝) (replicate (suc m) n)           ↝⟨ id ⟩□
  [ i ] replicate (suc m) n ⊑ ⌜ n ⌝                               □

------------------------------------------------------------------------
-- Least upper bounds

-- The least upper bound of a colist of natural numbers.

LUB : Colist ℕ ∞ → Conat ∞ → Type
LUB ns n =
  [ ∞ ] ns ⊑ n
    ×
  (∀ n′ → [ ∞ ] ns ⊑ n′ → [ ∞ ] n ≤ n′)

-- Least upper bounds are unique.

lub-unique :
  ∀ {ns n₁ n₂ i} →
  LUB ns n₁ → LUB ns n₂ → Conat.[ i ] n₁ ∼ n₂
lub-unique (lub₁₁ , lub₁₂) (lub₂₁ , lub₂₂) =
  antisymmetric-≤ (lub₁₂ _ lub₂₁) (lub₂₂ _ lub₁₁)

-- LUB respects bisimilarity.

LUB-∼ :
  ∀ {ms ns m n} →
  Colist.[ ∞ ] ms ∼ ns → Conat.[ ∞ ] m ∼ n →
  LUB ms m → LUB ns n
LUB-∼ {ms} {ns} {m} {n} p q = Σ-map
  ([ ∞ ] ms ⊑ m  ↝⟨ □-∼ p ⟩
   [ ∞ ] ns ⊑ m  ↝⟨ □-map (flip transitive-≤ (∼→≤ q)) ⟩□
   [ ∞ ] ns ⊑ n  □)
  (λ hyp n′ →
     [ ∞ ] ns ⊑ n′  ↝⟨ □-∼ (Colist.symmetric-∼ p) ⟩
     [ ∞ ] ms ⊑ n′  ↝⟨ hyp n′ ⟩
     [ ∞ ] m ≤ n′   ↝⟨ transitive-≤ (∼→≤ (Conat.symmetric-∼ q)) ⟩□
     [ ∞ ] n ≤ n′   □)

-- The least upper bound of the empty colist is 0.

lub-[] : LUB [] ⌜ 0 ⌝
lub-[] = [] , λ _ _ → zero

-- Some lemmas that can be used to establish the least upper bound of
-- a non-empty colist.

lub-∷ˡ :
  ∀ {m ms n} →
  [ ∞ ] n ≤ ⌜ m ⌝ →
  LUB (ms .force) n →
  LUB (m ∷ ms) ⌜ m ⌝
lub-∷ˡ {m} {ms} {n} n≤m = Σ-map
  ([ ∞ ] ms .force ⊑ n      ↝⟨ (λ hyp → reflexive-≤ _ ∷ λ { .force → □-map (flip transitive-≤ n≤m) hyp }) ⟩□
   [ ∞ ] m ∷ ms    ⊑ ⌜ m ⌝  □)
  ((∀ n′ → [ ∞ ] ms .force ⊑ n′ → [ ∞ ] n     ≤ n′)  ↝⟨ (λ _ _ → □-head) ⟩□
   (∀ n′ → [ ∞ ] m ∷ ms    ⊑ n′ → [ ∞ ] ⌜ m ⌝ ≤ n′)  □)

lub-∷ʳ :
  ∀ {m ms n} →
  [ ∞ ] ⌜ m ⌝ ≤ n →
  LUB (ms .force) n →
  LUB (m ∷ ms) n
lub-∷ʳ {m} {ms} {n} m≤n = Σ-map
  ([ ∞ ] ms .force ⊑ n  ↝⟨ (λ hyp → m≤n ∷ λ { .force → hyp }) ⟩□
   [ ∞ ] m ∷ ms    ⊑ n  □)
  ((∀ n′ → [ ∞ ] ms .force ⊑ n′ → [ ∞ ] n ≤ n′)  ↝⟨ (λ hyp n′ → hyp n′ ∘ □-tail) ⟩□
   (∀ n′ → [ ∞ ] m ∷ ms    ⊑ n′ → [ ∞ ] n ≤ n′)  □)

-- If m ∷ ms has a least upper bound, then cycle m ms has the same
-- least upper bound.

lub-cycle :
  ∀ {m ms n} →
  LUB (m ∷ ms) n →
  LUB (cycle m ms) n
lub-cycle {m} {ms} {n} = Σ-map
  ([ ∞ ] m ∷ ms     ⊑ n  ↝⟨ _⇔_.from □-cycle⇔ ⟩□
   [ ∞ ] cycle m ms ⊑ n  □)
  ((∀ n′ → [ ∞ ] m ∷ ms     ⊑ n′ → [ ∞ ] n ≤ n′)  ↝⟨ (∀-cong _ λ _ → →-cong-→ (_⇔_.to □-cycle⇔) id) ⟩□
   (∀ n′ → [ ∞ ] cycle m ms ⊑ n′ → [ ∞ ] n ≤ n′)  □)

-- The least upper bound of nats is infinity.

lub-nats-infinity : LUB nats Conat.infinity
lub-nats-infinity =
    (nats ⊑infinity)
  , λ n →
      [ ∞ ] nats ⊑ n                                             ↝⟨ flip no-finite→infinite ⟩
      ((∀ n → ¬ [ ∞ ] nats ⊑ ⌜ n ⌝) → Conat.[ ∞ ] n ∼ infinity)  ↝⟨ _$ nats⋢ ⟩
      Conat.[ ∞ ] n ∼ infinity                                   ↝⟨ Conat.symmetric-∼ ⟩
      Conat.[ ∞ ] infinity ∼ n                                   ↝⟨ ∼→≤ ⟩□
      [ ∞ ] infinity ≤ n                                         □

-- If WLPO holds, then the least upper bound of a colist of natural
-- numbers can be determined.
--
-- (In fact, WLPO is logically equivalent to the codomain of this
-- lemma, see Unbounded-space.wlpo⇔lub.)
--
-- I received help with this proof from Andreas Abel and Ulf Norell: I
-- had presented a proof that used LPO. Andreas Abel came up with the
-- idea for the following, less complicated proof, and Ulf Norell
-- suggested that one could get away with WLPO instead of LPO.

wlpo→lub : WLPO → (∀ ms → ∃ λ n → LUB ms n)
wlpo→lub wlpo = λ ms → lub ms , □ˢ∞→□∞ (upper-bound ms) , least ms
  where
  -- The boolean >0 ms n is true if the n-th number (counting from
  -- zero) of ms is positive.

  >0 : Colist ℕ ∞ → ℕ → Bool
  >0 []           _       = false
  >0 (m     ∷ ms) (suc n) = >0 (ms .force) n
  >0 (zero  ∷ ms) zero    = false
  >0 (suc m ∷ ms) zero    = true

  -- The number lub ms is the least upper bound of ms.

  lub : ∀ {i} → Colist ℕ ∞ → Conat i
  lub ms with wlpo (>0 ms)
  ... | inj₁ _ = zero
  ... | inj₂ _ = suc λ { .force → lub (map pred ms) }

  -- Zero is an upper bound of ms iff >0 ms is universally false.

  ⊑0⇔≡false : ∀ ms → [ ∞ ] ms ⊑ zero ⇔ (∀ n → >0 ms n ≡ false)
  ⊑0⇔≡false = λ ms → record { to = to ms; from = from ms }
    where
    to : ∀ ms → [ ∞ ] ms ⊑ zero → (∀ n → >0 ms n ≡ false)
    to _            []         _       = refl
    to (zero  ∷ ms) _          zero    = refl
    to (suc _ ∷ _)  (() ∷ _)   _
    to (m     ∷ ms) (_ ∷ ms⊑0) (suc n) = to (ms .force) (ms⊑0 .force) n

    from : ∀ {i} ms → (∀ n → >0 ms n ≡ false) → [ i ] ms ⊑ zero
    from []           _      = []
    from (suc m ∷ ms) ≡false = ⊥-elim (Bool.true≢false (≡false zero))
    from (zero  ∷ ms) ≡false =
      zero ∷ λ { .force → from (ms .force) (≡false ∘ suc) }

  -- If n .force is an upper bound of map pred ms, then suc n is an
  -- upper bound of ms. Note that the lemma is size-preserving and
  -- takes □ˢ′ to □ˢ.

  pred-lemma₁ :
    ∀ {i n} ms →
    □ˢ′ i (λ i m → [ i ] ⌜ m ⌝ ≤ n .force) (map pred ms) →
    □ˢ i (λ i m → [ i ] ⌜ m ⌝ ≤ suc n) ms
  pred-lemma₁ []       hyp = []
  pred-lemma₁ (m ∷ ms) hyp =
    helper m hyp
      ∷ λ { .force →
    pred-lemma₁ (ms .force) λ { .force → □ˢ-tail (hyp .force) }}
    where
    helper :
      ∀ {i n} m →
      □ˢ′ i (λ i m → [ i ] ⌜ m ⌝ ≤ n .force) (map pred (m ∷ ms)) →
      [ i ] ⌜ m ⌝ ≤ suc n
    helper zero    hyp = zero
    helper (suc m) hyp = suc λ { .force → □ˢ-head (hyp .force) }

  -- If suc n is an upper bound of ms, then n .force is an upper bound
  -- of map pred ms.

  pred-lemma₂ :
    ∀ {n ms i} →
    [ i ] ms ⊑ suc n →
    [ i ] map pred ms ⊑ n .force
  pred-lemma₂     []                         = []
  pred-lemma₂ {n} (_∷_ {x = m} m≤1+n ms⊑1+n) =
    (⌜ pred m ⌝        ∼⟨ ⌜⌝-pred m ⟩≤
     Conat.pred ⌜ m ⌝  ≤⟨ pred-mono m≤1+n ⟩∎
     n .force          ∎≤)
      ∷ λ { .force →
    pred-lemma₂ (ms⊑1+n .force) }

  -- The number lub ms is an upper bound of ms.

  upper-bound : ∀ {i} ms → □ˢ i (λ i m → [ i ] ⌜ m ⌝ ≤ lub ms) ms
  upper-bound {i} ms with wlpo (>0 ms)
  ... | inj₂ _ =
    pred-lemma₁ _ (λ { .force → upper-bound (map pred ms) })

  ... | inj₁ ≡false =                     $⟨ ≡false ⟩
    (∀ n → >0 ms n ≡ false)               ↝⟨ _⇔_.from (⊑0⇔≡false ms) ⟩
    [ ∞ ] ms ⊑ zero                       ↝⟨ id ⟩
    [ i ] ms ⊑ zero                       ↝⟨ _⇔_.from □ˢ⇔□ ⟩
    □ˢ i (λ _ m → [ ∞ ] ⌜ m ⌝ ≤ zero) ms  ↝⟨ id ⟩□
    □ˢ i (λ i m → [ i ] ⌜ m ⌝ ≤ zero) ms  □

  -- The number lub ms is less than or equal to every number that is
  -- an upper bound of ms.

  least :
    ∀ {i} ms ub →
    [ ∞ ] ms ⊑ ub →
    [ i ] lub ms ≤ ub
  least ms ub ms⊑ub with wlpo (>0 ms)
  least ms ub ms⊑ub | inj₁ _ = zero

  least ms (suc ub) ms⊑1+ub | inj₂ _ =
    suc λ { .force →
      least (map pred ms) (ub .force) (pred-lemma₂ ms⊑1+ub) }

  least ms zero ms⊑0 | inj₂ ¬≡false =
                             $⟨ ms⊑0 ⟩
    [ ∞ ] ms ⊑ zero          ↝⟨ _⇔_.to (⊑0⇔≡false _) ⟩
    (∀ n → >0 ms n ≡ false)  ↝⟨ ¬≡false ⟩
    ⊥                        ↝⟨ ⊥-elim ⟩□
    _                        □

------------------------------------------------------------------------
-- A relation that can be used to relate the least upper bounds of two
-- colists

-- [ ∞ ] ms ≲ ns means that every upper bound of ns is also an upper
-- bound of ms.

infix 4 [_]_≲_ [_]_≲′_

[_]_≲_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Type
[ i ] ms ≲ ns = ∀ {n} → [ ∞ ] ns ⊑ n → [ i ] ms ⊑ n

[_]_≲′_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Type
[ i ] ms ≲′ ns = ∀ {n} → [ ∞ ] ns ⊑ n → [ i ] ms ⊑′ n

-- Bounded m ns means that m is smaller than or equal to some element
-- in ns, or equal to zero.

Bounded : ℕ → Colist ℕ ∞ → Type
Bounded m ns = ◇ ∞ (m ≤_) ns ⊎ m ≡ zero

-- If Bounded m ns holds, then m is less than or equal to every upper
-- bound of ns.

bounded-lemma :
  ∀ {m ns n} →
  Bounded m ns → [ ∞ ] ns ⊑ n → [ ∞ ] ⌜ m ⌝ ≤ n
bounded-lemma (inj₁ ◇m≤ns) = transitive-◇≤⊑ ◇m≤ns
bounded-lemma (inj₂ refl)  = const zero

-- The empty colist is bounded by any other.

[]≲ : ∀ {ns i} → [ i ] [] ≲ ns
[]≲ = λ _ → []

-- Some derived cons-like operations.

consʳ-≲ :
  ∀ {ms ns n i} →
  [ i ] ms ≲ ns .force →
  [ i ] ms ≲ n ∷ ns
consʳ-≲ = _∘ □-tail

consˡ-≲ :
  ∀ {i m ms ns} →
  Bounded m ns →
  [ i ] ms .force ≲′ ns →
  [ i ] m ∷ ms ≲ ns
consˡ-≲ ◇m≤ns ms≲′ns ns⊑n =
  bounded-lemma ◇m≤ns ns⊑n ∷ λ { .force →
  ms≲′ns ns⊑n .force }

cons-≲ :
  ∀ {i m ms n ns} →
  Bounded m (n ∷ ns) →
  [ i ] ms .force ≲′ ns .force →
  [ i ] m ∷ ms ≲ n ∷ ns
cons-≲ {i} {m} {ms} {n} {ns} ◇m≤n∷ns =
  [ i ] ms .force ≲′ ns .force  ↝⟨ (λ { ms≲′ns hyp .force → consʳ-≲ (λ hyp → ms≲′ns hyp .force) hyp }) ⟩
  [ i ] ms .force ≲′ n ∷ ns     ↝⟨ consˡ-≲ ◇m≤n∷ns ⟩□
  [ i ] m ∷ ms ≲ n ∷ ns         □

cons′-≲ :
  ∀ {i m ms ns} →
  [ i ] ms .force ≲′ ns .force →
  [ i ] m ∷ ms ≲ m ∷ ns
cons′-≲ = cons-≲ (inj₁ (here Nat.≤-refl))

-- If the combinator consʳ-≲ had taken the primed variant of the
-- relation as an argument instead of the unprimed variant, then any
-- colist would have been bounded by any infinite colist.

consʳ-≲′→≲-infinite :
  (∀ {i ms ns n} → [ i ] ms ≲′ ns .force → [ i ] ms ≲ n ∷ ns) →
  (∀ {i ms ns} → Conat.[ ∞ ] length ns ∼ infinity → [ i ] ms ≲ ns)
consʳ-≲′→≲-infinite consʳ-≲′ {ns = []}    ()
consʳ-≲′→≲-infinite consʳ-≲′ {ns = _ ∷ _} (suc p) =
  consʳ-≲′ λ { hyp .force →
    consʳ-≲′→≲-infinite consʳ-≲′ (p .force) hyp }

-- Thus one cannot make this argument's type primed.

¬-consʳ-≲′ :
  ¬ (∀ {i ms ns n} → [ i ] ms ≲′ ns .force → [ i ] ms ≲ n ∷ ns)
¬-consʳ-≲′ =
  (∀ {i ms ns n} → [ i ] ms ≲′ ns .force → [ i ] ms ≲ n ∷ ns)       ↝⟨ consʳ-≲′→≲-infinite ⟩
  (∀ {i ms ns} → Conat.[ ∞ ] length ns ∼ infinity → [ i ] ms ≲ ns)  ↝⟨ (λ hyp → hyp (length-replicate _)) ⟩
  [ ∞ ] repeat 1 ≲ repeat 0                                         ↝⟨ _$ replicate⊑ _ ⟩
  [ ∞ ] repeat 1 ⊑ zero                                             ↝⟨ □-head ⟩
  [ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝                                               ↝⟨ ≮0 ⟩□
  ⊥                                                                 □

-- Bisimilarity is contained in the relation.

∼→≲ : ∀ {i ms ns} → Colist.[ i ] ms ∼ ns → [ i ] ms ≲ ns
∼→≲ []          = []≲
∼→≲ (refl ∷ ps) = cons′-≲ λ { hyp .force → ∼→≲ (ps .force) hyp }

-- "Equational" reasoning combinators.

infix  -1 _□≲ finally-≲ finally-≲∼
infixr -2 step-≲ step-≡≲ _≡⟨⟩≲_ step-∼≲

step-≲ : ∀ {i} ms {ns os} →
         [ ∞ ] ns ≲ os → [ i ] ms ≲ ns → [ i ] ms ≲ os
step-≲ {i} ms {ns} {os} ns≲os ms≲ns {n = n} =
  [ ∞ ] os ⊑ n  ↝⟨ ns≲os ⟩
  [ ∞ ] ns ⊑ n  ↝⟨ ms≲ns ⟩□
  [ i ] ms ⊑ n  □

syntax step-≲ ms ns≲os ms≲ns = ms ≲⟨ ms≲ns ⟩ ns≲os

step-≡≲ : ∀ {i} ms {ns os} → [ i ] ns ≲ os → ms ≡ ns → [ i ] ms ≲ os
step-≡≲ _ ns≲os refl = ns≲os

syntax step-≡≲ ms ns≲os ms≡ns = ms ≡⟨ ms≡ns ⟩≲ ns≲os

_≡⟨⟩≲_ : ∀ {i} ms {ns} → [ i ] ms ≲ ns → [ i ] ms ≲ ns
_ ≡⟨⟩≲ ms≲ns = ms≲ns

step-∼≲ : ∀ {i} ms {ns os} →
          [ i ] ns ≲ os → Colist.[ i ] ms ∼ ns → [ i ] ms ≲ os
step-∼≲ {i} ms {ns} {os} ns≲os ms∼ns {n} =
  [ ∞ ] os ⊑ n  ↝⟨ ns≲os ⟩
  [ i ] ns ⊑ n  ↝⟨ □-∼ (Colist.symmetric-∼ ms∼ns) ⟩□
  [ i ] ms ⊑ n  □

syntax step-∼≲ ms ns≲os ms∼ns = ms ∼⟨ ms∼ns ⟩≲ ns≲os

finally-≲ : ∀ {i} ms ns → [ i ] ms ≲ ns → [ i ] ms ≲ ns
finally-≲ _ _ = id

syntax finally-≲ ms ns ms≲ns = ms ≲⟨ ms≲ns ⟩□ ns

finally-≲∼ : ∀ {i} ms ns → Colist.[ i ] ms ∼ ns → [ i ] ms ≲ ns
finally-≲∼ _ _ = ∼→≲

syntax finally-≲∼ ms ns ms∼ns = ms ∼⟨ ms∼ns ⟩□≲ ns

_□≲ : ∀ {i} ns → [ i ] ns ≲ ns
_□≲ {i} ns {n} =
  [ ∞ ] ns ⊑ n  ↝⟨ id ⟩□
  [ i ] ns ⊑ n  □

-- The transitivity proof can not be made size-preserving in the other
-- argument.

¬-transitivity-size-preservingʳ :
  ¬ (∀ {i ms ns os} → [ ∞ ] ms ≲ ns → [ i ] ns ≲ os → [ i ] ms ≲ os)
¬-transitivity-size-preservingʳ trans = contradiction
  where
  ones : ∀ {i} → Colist′ ℕ i
  ones .force = repeat 1

  bad : ∀ {i} → [ i ] 0 ∷ ones ≲ repeat 0
  bad {n = n} hyp = zero ∷ λ { .force {j} →  $⟨ (λ {_} → consʳ-≲ (repeat 1 □≲)) ⟩
    [ ∞ ] repeat 1 ≲ 0 ∷ ones                ↝⟨ flip trans bad ⟩
    [ j ] repeat 1 ≲ repeat 0                ↝⟨ (λ f → f hyp) ⟩□
    [ j ] repeat 1 ⊑ n                       □ }

  contradiction =              $⟨ (λ {_} → bad) ⟩
    [ ∞ ] 0 ∷ ones ≲ repeat 0  ↝⟨ _$ replicate⊑ _ ⟩
    [ ∞ ] 0 ∷ ones ⊑ zero      ↝⟨ □-head ∘ □-tail ⟩
    [ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝        ↝⟨ ≮0 ⟩□
    ⊥                          □

-- The transitivity proof can not be made size-preserving in both
-- arguments.

¬-transitivity-size-preserving :
  ¬ (∀ {i ms ns os} → [ i ] ms ≲ ns → [ i ] ns ≲ os → [ i ] ms ≲ os)
¬-transitivity-size-preserving = ¬-transitivity-size-preservingʳ

-- If the least upper bound of ms is m and the least upper bound of ns
-- is n, then [ ∞ ] ms ≲ ns holds if and only if [ ∞ ] m ≤ n holds.

≲⇔least-upper-bounds-≤ :
  ∀ {m n ms ns} →
  LUB ms m → LUB ns n →
  [ ∞ ] ms ≲ ns ⇔ [ ∞ ] m ≤ n
≲⇔least-upper-bounds-≤ {⨆ms} {⨆ns} {ms} {ns} ⨆ms-lub ⨆ns-lub = record
  { to   = λ ms≲ns →          $⟨ proj₁ ⨆ns-lub ⟩
             [ ∞ ] ns ⊑ ⨆ns   ↝⟨ ms≲ns ⟩
             [ ∞ ] ms ⊑ ⨆ns   ↝⟨ proj₂ ⨆ms-lub _ ⟩□
             [ ∞ ] ⨆ms ≤ ⨆ns  □
  ; from = λ ⨆ms≤⨆ns {n} →
             [ ∞ ] ns ⊑ n   ↝⟨ proj₂ ⨆ns-lub n ⟩
             [ ∞ ] ⨆ns ≤ n  ↝⟨ transitive-≤ ⨆ms≤⨆ns ⟩
             [ ∞ ] ⨆ms ≤ n  ↝⟨ transitive-⊑≤ (proj₁ ⨆ms-lub) ⟩□
             [ ∞ ] ms ⊑ n   □
  }

------------------------------------------------------------------------
-- Another relation that can be used to relate the least upper bounds
-- of two colists

-- [ ∞ ] ms ≂ ns means that every upper bound of ns is also an upper
-- bound of ms, and vice versa.

infix 4 [_]_≂_ [_]_≂′_

[_]_≂_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Type
[ i ] ms ≂ ns = [ i ] ms ≲ ns × [ i ] ns ≲ ms

[_]_≂′_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Type
[ i ] ms ≂′ ns = [ i ] ms ≲′ ns × [ i ] ns ≲′ ms

-- The relation is symmetric.

symmetric-≂ : ∀ {i ms ns} → [ i ] ms ≂ ns → [ i ] ns ≂ ms
symmetric-≂ = swap

-- Some derived cons-like operations.

consʳ-≂ :
  ∀ {i ms n ns} →
  Bounded n ms →
  [ i ] ms ≂ ns .force →
  [ i ] ms ≂ n ∷ ns
consʳ-≂ ◇n≤ms = Σ-map
  consʳ-≲
  (λ ns≲ms → consˡ-≲ ◇n≤ms λ hyp → λ { .force → ns≲ms hyp })

consˡ-≂ :
  ∀ {i m ms ns} →
  Bounded m ns →
  [ i ] ms .force ≂ ns →
  [ i ] m ∷ ms ≂ ns
consˡ-≂ ◇m≤ns = symmetric-≂ ∘ consʳ-≂ ◇m≤ns ∘ symmetric-≂

cons-≂ :
  ∀ {i m ms n ns} →
  Bounded m (n ∷ ns) →
  Bounded n (m ∷ ms) →
  [ i ] ms .force ≂′ ns .force →
  [ i ] m ∷ ms ≂ n ∷ ns
cons-≂ ◇m≤n∷ns ◇n≤m∷ms = Σ-map (cons-≲ ◇m≤n∷ns) (cons-≲ ◇n≤m∷ms)

cons′-≂ :
  ∀ {i m ms ns} →
  [ i ] ms .force ≂′ ns .force →
  [ i ] m ∷ ms ≂ m ∷ ns
cons′-≂ = Σ-map cons′-≲ cons′-≲

cons″-≂ :
  ∀ {i m ms ns} →
  [ i ] ms .force ≂ ns .force →
  [ i ] m ∷ ms ≂ m ∷ ns
cons″-≂ = cons′-≂ ∘ Σ-map (λ { ms≲ns hyp .force → ms≲ns hyp })
                          (λ { ns≲ms hyp .force → ns≲ms hyp })

-- Bisimilarity is contained in the relation.

∼→≂ : ∀ {i ms ns} → Colist.[ i ] ms ∼ ns → [ i ] ms ≂ ns
∼→≂ ms∼ns = ∼→≲ ms∼ns , ∼→≲ (Colist.symmetric-∼ ms∼ns)

-- "Equational" reasoning combinators.

infix  -1 _□≂ finally-≂ finally-≂∼
infixr -2 step-≂ step-≡≂ _≡⟨⟩≂_ step-∼≂ step-≂∼

step-≂ : ∀ {i} ms {ns os} →
         [ ∞ ] ns ≂ os → [ ∞ ] ms ≂ ns → [ i ] ms ≂ os
step-≂ _ = Σ-zip (step-≲ _) (flip (step-≲ _))

syntax step-≂ ms ns≂os ms≂ns = ms ≂⟨ ms≂ns ⟩ ns≂os

step-≡≂ : ∀ {i} ms {ns os} → [ i ] ns ≂ os → ms ≡ ns → [ i ] ms ≂ os
step-≡≂ _ ns≂os refl = ns≂os

syntax step-≡≂ ms ns≂os ms≡ns = ms ≡⟨ ms≡ns ⟩≂ ns≂os

_≡⟨⟩≂_ : ∀ {i} ms {ns} → [ i ] ms ≂ ns → [ i ] ms ≂ ns
_ ≡⟨⟩≂ ms≂ns = ms≂ns

step-∼≂ : ∀ {i} ms {ns os} →
          [ i ] ns ≂ os → Colist.[ ∞ ] ms ∼ ns → [ i ] ms ≂ os
step-∼≂ {i} ms {ns} {os} (ns≲os , os≲ns) ms∼ns =
    step-∼≲ ms ns≲os ms∼ns
  , λ {n} →
      [ ∞ ] ms ⊑ n  ↝⟨ □-∼ ms∼ns ⟩
      [ ∞ ] ns ⊑ n  ↝⟨ os≲ns ⟩□
      [ i ] os ⊑ n  □

syntax step-∼≂ ms ns≂os ms∼ns = ms ∼⟨ ms∼ns ⟩≂ ns≂os

step-≂∼ : ∀ {i} ms {ns os} →
          Colist.[ ∞ ] ns ∼ os → [ i ] ms ≂ ns → [ i ] ms ≂ os
step-≂∼ _ ns∼os ms≂ns =
  symmetric-≂
    (step-∼≂ _ (symmetric-≂ ms≂ns) (Colist.symmetric-∼ ns∼os))

syntax step-≂∼ ms ns∼os ms≂ns = ms ≂⟨ ms≂ns ⟩∼ ns∼os

finally-≂ : ∀ {i} ms ns → [ i ] ms ≂ ns → [ i ] ms ≂ ns
finally-≂ _ _ = id

syntax finally-≂ ms ns ms≂ns = ms ≂⟨ ms≂ns ⟩□ ns

finally-≂∼ : ∀ {i} ms ns → Colist.[ i ] ms ∼ ns → [ i ] ms ≂ ns
finally-≂∼ _ _ = ∼→≂

syntax finally-≂∼ ms ns ms∼ns = ms ∼⟨ ms∼ns ⟩□≂ ns

_□≂ : ∀ {i} ns → [ i ] ns ≂ ns
ns □≂ = (ns □≲) , (ns □≲)

-- If the least upper bound of ms is m and the least upper bound of ns
-- is n, then [ ∞ ] ms ≂ ns holds if and only if m and n are
-- bisimilar.

≂⇔least-upper-bounds-∼ :
  ∀ {m n ms ns} →
  LUB ms m → LUB ns n →
  [ ∞ ] ms ≂ ns ⇔ Conat.[ ∞ ] m ∼ n
≂⇔least-upper-bounds-∼ {⨆ms} {⨆ns} {ms} {ns} ⨆ms-lub ⨆ns-lub =
  [ ∞ ] ms ≂ ns                      ↝⟨ ≲⇔least-upper-bounds-≤ ⨆ms-lub ⨆ns-lub
                                          ×-cong
                                        ≲⇔least-upper-bounds-≤ ⨆ns-lub ⨆ms-lub ⟩
  [ ∞ ] ⨆ms ≤ ⨆ns × [ ∞ ] ⨆ns ≤ ⨆ms  ↝⟨ record { to   = uncurry antisymmetric-≤
                                               ; from = λ hyp → ∼→≤ hyp , ∼→≤ (Conat.symmetric-∼ hyp)
                                               } ⟩□
  Conat.[ ∞ ] ⨆ms ∼ ⨆ns              □

-- The predicate flip LUB n respects [ ∞ ]_≂_.

LUB-≂ : ∀ {ms ns n} → [ ∞ ] ms ≂ ns → LUB ms n → LUB ns n
LUB-≂ {ms} {ns} {n} (ms≲ns , ns≲ms) = Σ-map
  ([ ∞ ] ms ⊑ n  ↝⟨ ns≲ms ⟩□
   [ ∞ ] ns ⊑ n  □)
  ((∀ n′ → [ ∞ ] ms ⊑ n′ → [ ∞ ] n ≤ n′)  ↝⟨ (λ hyp n′ → hyp n′ ∘ ms≲ns) ⟩□
   (∀ n′ → [ ∞ ] ns ⊑ n′ → [ ∞ ] n ≤ n′)  □)

-- If [ ∞ ] ms ≂ ns holds, then ms and ns have the same least upper
-- bounds.

LUB-cong : ∀ {ms ns n} → [ ∞ ] ms ≂ ns → LUB ms n ⇔ LUB ns n
LUB-cong ms≂ns = record
  { to   = LUB-≂              ms≂ns
  ; from = LUB-≂ (symmetric-≂ ms≂ns)
  }

-- A workaround for what might be an Agda bug.

cast-≂ :
  ∀ {i} {j : Size< i} {ms ns} →
  [ i ] ms ≂ ns → [ j ] ms ≂ ns
cast-≂ p = proj₁ p , proj₂ p

------------------------------------------------------------------------
-- Variants of [_]_≲′_ and [_]_≂′_ that are intended to make certain
-- proofs easier to write

-- Using consˡ-≲/cons-≲/cons′-≲ in recursive proofs can be awkward.
-- [_]_≲″_ is intended to make it a little easier.

infix 4 [_]_≲″_

record [_]_≲″_ (i : Size) (ms ns : Colist ℕ ∞) : Type where
  coinductive
  field
    force : {j : Size< i} → [ j ] ms ≲ ns

open [_]_≲″_ public

-- Interprets [_]_≲″_.

⌊_⌋≲″ : ∀ {i ms ns} → [ i ] ms ≲″ ns → [ i ] ms ≲′ ns
⌊ p ⌋≲″ hyp .force = p .force hyp

-- [_]_≲′_ and [_]_≲″_ are pointwise logically equivalent.

≲′⇔≲″ : ∀ {i ms ns} → [ i ] ms ≲′ ns ⇔ [ i ] ms ≲″ ns
≲′⇔≲″ = record
  { to   = λ { p .force hyp → p hyp .force }
  ; from = λ { p hyp .force → p .force hyp }
  }

-- Using cons-≂/cons′-≂ in recursive proofs can be awkward. [_]_≂″_ is
-- intended to make it a little easier.

infix 4 [_]_≂″_

record [_]_≂″_ (i : Size) (ms ns : Colist ℕ ∞) : Type where
  coinductive
  field
    force : {j : Size< i} → [ j ] ms ≂ ns

open [_]_≂″_ public

-- [_]_≂′_ and [_]_≂″_ are pointwise logically equivalent.

≂′⇔≂″ : ∀ {i ms ns} → [ i ] ms ≂′ ns ⇔ [ i ] ms ≂″ ns
≂′⇔≂″ = record
  { to   = λ { p .force → (λ hyp → proj₁ p hyp .force)
                        , (λ hyp → proj₂ p hyp .force)
             }
  ; from = λ p → (λ { hyp .force → proj₁ (p .force) hyp })
               , (λ { hyp .force → proj₂ (p .force) hyp })
  }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
{-# OPTIONS --without-K #-}

open import Base

module Algebra.FreeGroupAsReducedWords {i} (A : Set i) (eq : has-dec-eq A) where

A-is-set : is-set A
A-is-set = dec-eq-is-set eq

data word : Set i where
  ε : word
  _∷_ : A → word → word
  _′∷_ : A → word → word

is-reduced : word → Set i
is-reduced ε = unit
is-reduced (x ∷ ε) = unit
is-reduced (x ∷ (y ∷ w)) = is-reduced (y ∷ w)
is-reduced (x ∷ (y ′∷ w)) = (x ≢ y) × is-reduced (y ′∷ w)
is-reduced (x ′∷ ε) = unit
is-reduced (x ′∷ (y ∷ w)) = (x ≢ y) × is-reduced (y ∷ w)
is-reduced (x ′∷ (y ′∷ w)) = is-reduced (y ′∷ w)

is-reduced-is-prop : (w : word) → is-prop (is-reduced w)
is-reduced-is-prop ε = unit-is-prop
is-reduced-is-prop (x ∷ ε) = unit-is-prop
is-reduced-is-prop (x ∷ (y ∷ w)) = is-reduced-is-prop (y ∷ w)
is-reduced-is-prop (x ∷ (y ′∷ w)) =
  ×-is-truncated _ (Π-is-truncated _ (λ _ → λ ())) (is-reduced-is-prop (y ′∷ w))
is-reduced-is-prop (x ′∷ ε) = unit-is-prop
is-reduced-is-prop (x ′∷ (y ∷ w)) =
  ×-is-truncated _ (Π-is-truncated _ (λ _ → λ ())) (is-reduced-is-prop (y ∷ w))
is-reduced-is-prop (x ′∷ (y ′∷ w)) = is-reduced-is-prop (y ′∷ w)

reduced-word : Set i
reduced-word = Σ word is-reduced

word-total-path : {x y : A} (p : x ≡ y) {v w : word} (q : v ≡ w)
  → (x ∷ v ≡ y ∷ w)
word-total-path refl refl = refl

word'-total-path : {x y : A} (p : x ≡ y) {v w : word} (q : v ≡ w)
  → (x ′∷ v ≡ y ′∷ w)
word'-total-path refl refl = refl

-- The following six functions prove things like if [x ∷ v ≡ y ∷ w],
-- then [x ≡ y].
-- This is not as easy as it sounds, you cannot directly induct on the equality
-- (because [x ∷ v] is not a general element of type word), so you have to
-- extract the head, but it’s not always possible…

word-comp-path-type : (v w : word) → Set i
word-comp-path-type ε ε = unit
word-comp-path-type ε (y ∷ w) = ⊥
word-comp-path-type ε (y ′∷ w) = ⊥
word-comp-path-type (x ∷ v) ε = ⊥
word-comp-path-type (x ∷ v) (y ∷ w) = (x ≡ y) × (v ≡ w)
word-comp-path-type (x ∷ v) (y ′∷ w) = ⊥
word-comp-path-type (x ′∷ v) ε = ⊥
word-comp-path-type (x ′∷ v) (y ∷ w) = ⊥
word-comp-path-type (x ′∷ v) (y ′∷ w) = (x ≡ y) × (v ≡ w)

word-comp-path : {v w : word} (p : v ≡ w) → word-comp-path-type v w
word-comp-path {v = ε}      refl = tt
word-comp-path {v = x  ∷ v} refl = (refl , refl)
word-comp-path {v = x ′∷ v} refl = (refl , refl)

word-base-path : {x y : A} {v w : word} (p : x ∷ v ≡ y ∷ w) → x ≡ y
word-base-path p = π₁ (word-comp-path p)

word-fiber-path : {x y : A} {v w : word} (p : x ∷ v ≡ y ∷ w) → v ≡ w
word-fiber-path p = π₂ (word-comp-path p)

word'-base-path : {x y : A} {v w : word} (p : x ′∷ v ≡ y ′∷ w) → x ≡ y
word'-base-path p = π₁ (word-comp-path p)

word'-fiber-path : {x y : A} {v w : word} (p : x ′∷ v ≡ y ′∷ w) → v ≡ w
word'-fiber-path p = π₂ (word-comp-path p)

-- This one goes to Set and is used to prove that the constructors of [word] are
-- disjoint
word-cst-dis : (v w : word) → Set
word-cst-dis ε ε = unit
word-cst-dis ε (y ∷ w) = ⊥
word-cst-dis ε (y ′∷ w) = ⊥
word-cst-dis (x ∷ v) ε = ⊥
word-cst-dis (x ∷ v) (y ∷ w) = unit
word-cst-dis (x ∷ v) (y ′∷ w) = ⊥
word-cst-dis (x ′∷ v) ε = ⊥
word-cst-dis (x ′∷ v) (y ∷ w) = ⊥
word-cst-dis (x ′∷ v) (y ′∷ w) = unit

word-has-dec-eq : has-dec-eq word
word-has-dec-eq ε ε = inl refl
word-has-dec-eq ε (x ∷ w) = inr (λ p → transport (word-cst-dis ε) p tt)
word-has-dec-eq ε (x ′∷ w) = inr (λ p → transport (word-cst-dis ε) p tt)
word-has-dec-eq (x ∷ v) ε = inr (λ p → transport (word-cst-dis (x ∷ v)) p tt)
word-has-dec-eq (x ∷ v) (y ∷ w) with (eq x y)
word-has-dec-eq (x ∷ v) (y ∷ w) | inl x≡y with (word-has-dec-eq v w)
word-has-dec-eq (x ∷ v) (y ∷ w) | inl x≡y | inl v≡w =
  inl (word-total-path x≡y v≡w)
word-has-dec-eq (x ∷ v) (y ∷ w) | inl x≡y | inr v≢w =
  inr (λ p → v≢w (word-fiber-path p))
word-has-dec-eq (x ∷ v) (y ∷ w) | inr x≢y = inr (λ p → x≢y (word-base-path p))
word-has-dec-eq (x ∷ v) (y ′∷ w) =
  inr (λ p → transport (word-cst-dis (x ∷ v)) p tt)
word-has-dec-eq (x ′∷ v) ε = inr (λ p → transport (word-cst-dis (x ′∷ v)) p tt)
word-has-dec-eq (x ′∷ v) (y ∷ w) =
  inr (λ p → transport (word-cst-dis (x ′∷ v)) p tt)
word-has-dec-eq (x ′∷ v) (y ′∷ w) with (eq x y)
word-has-dec-eq (x ′∷ v) (y ′∷ w) | inl x≡y with (word-has-dec-eq v w)
word-has-dec-eq (x ′∷ v) (y ′∷ w) | inl x≡y | inl v≡w =
  inl (word'-total-path x≡y v≡w)
word-has-dec-eq (x ′∷ v) (y ′∷ w) | inl x≡y | inr v≢w =
  inr (λ p → v≢w (word'-fiber-path p))
word-has-dec-eq (x ′∷ v) (y ′∷ w) | inr x≢y =
  inr (λ p → x≢y (word'-base-path p))

word-is-set : is-set word
word-is-set = dec-eq-is-set word-has-dec-eq

abstract
  reduced-is-set : is-set reduced-word
  reduced-is-set =
    subtype-truncated-S-is-truncated-S _ word-is-set is-reduced-is-prop

tail-is-reduced : (x : A) (w : word) (r : is-reduced (x ∷ w)) → is-reduced w
tail-is-reduced x ε red = tt
tail-is-reduced x (y ∷ w) red = red
tail-is-reduced x (y ′∷ w) red = π₂ red

tail'-is-reduced : (x : A) (w : word) (r : is-reduced (x ′∷ w)) → is-reduced w
tail'-is-reduced x ε red = tt
tail'-is-reduced x (y ∷ w) red = π₂ red
tail'-is-reduced x (y ′∷ w) red = red

import Algebra.FreeGroup as F
open F A
import Algebra.FreeGroupProps as Fp
open Fp A

reduced-to-freegroup : reduced-word → freegroup
reduced-to-freegroup (ε , _) = e
reduced-to-freegroup ((x ∷ w) , r) =
  x · reduced-to-freegroup (w , tail-is-reduced x w r)
reduced-to-freegroup ((x ′∷ w) , r) =
  x ⁻¹· reduced-to-freegroup (w , tail'-is-reduced x w r)

mul-reduce : A → reduced-word → reduced-word
mul-reduce x (ε , red) = ((x ∷ ε) , tt)
mul-reduce x ((y ∷ w) , red) = ((x ∷ (y ∷ w)) , red)
mul-reduce x ((y ′∷ w) , red) with (eq x y)
mul-reduce x ((y ′∷ w) , red) | inl equal = (w , tail'-is-reduced y w red)
mul-reduce x ((y ′∷ w) , red) | inr different =
  ((x ∷ (y ′∷ w)) , (different , red))

mul'-reduce : A → reduced-word → reduced-word
mul'-reduce x (ε , red) = ((x ′∷ ε) , tt)
mul'-reduce x ((y ∷ w) , red) with (eq x y)
mul'-reduce x ((y ∷ w) , red) | inl equal = (w , tail-is-reduced y w red)
mul'-reduce x ((y ∷ w) , red) | inr different =
  ((x ′∷ (y ∷ w)) , (different , red))
mul'-reduce x ((y ′∷ w) , red) = (x ′∷ (y ′∷ w)) , red

abstract
  mul-mul'-reduce : (x : A) (w : reduced-word)
    → mul-reduce x (mul'-reduce x w) ≡ w
  mul-mul'-reduce x (ε , red) with (eq x x)
  mul-mul'-reduce x (ε , red) | inl obvious = refl
  mul-mul'-reduce x (ε , red) | inr absurd = abort-nondep (absurd refl)
  mul-mul'-reduce x ((y ∷ w) , red) with (eq x y)
  mul-mul'-reduce x ((y ∷ ε) , red) | inl equal = ap _ equal
  mul-mul'-reduce x ((y ∷ (z ∷ w)) , red) | inl equal = ap _ equal
  mul-mul'-reduce x ((y ∷ (z ′∷ w)) , red) | inl equal with (eq x z)
  mul-mul'-reduce x ((y ∷ (z ′∷ w)) , red) | inl equal | inl absurd =
    abort-nondep (π₁ red (! equal ∘ absurd))
  mul-mul'-reduce x ((y ∷ (z ′∷ w)) , red) | inl equal | inr obvious =
    Σ-eq (ap _ equal) (π₁ (is-reduced-is-prop (y ∷ (z ′∷ w)) _ _))
  mul-mul'-reduce x ((y ∷ w) , red) | inr different with (eq x x)
  mul-mul'-reduce x ((y ∷ w) , red) | inr different | inl obvious = refl
  mul-mul'-reduce x ((y ∷ w) , red) | inr different | inr absurd =
    abort-nondep (absurd refl)
  mul-mul'-reduce x ((y ′∷ w) , red) with (eq x x)
  mul-mul'-reduce x ((y ′∷ w) , red) | inl obvious = refl
  mul-mul'-reduce x ((y ′∷ w) , red) | inr absurd =
    abort-nondep (absurd refl)

abstract
  mul'-mul-reduce : (x : A) (w : reduced-word)
    → mul'-reduce x (mul-reduce x w) ≡ w
  mul'-mul-reduce x (ε , red) with (eq x x)
  mul'-mul-reduce x (ε , red) | inl obvious = refl
  mul'-mul-reduce x (ε , red) | inr absurd = abort-nondep (absurd refl)
  mul'-mul-reduce x ((y ′∷ w) , red) with (eq x y)
  mul'-mul-reduce x ((y ′∷ ε) , red) | inl equal = ap _ equal
  mul'-mul-reduce x ((y ′∷ (z ′∷ w)) , red) | inl equal = ap _ equal
  mul'-mul-reduce x ((y ′∷ (z ∷ w)) , red) | inl equal with (eq x z)
  mul'-mul-reduce x ((y ′∷ (z ∷ w)) , red) | inl equal | inl absurd =
    abort-nondep (π₁ red (! equal ∘ absurd))
  mul'-mul-reduce x ((y ′∷ (z ∷ w)) , red) | inl equal | inr obvious =
    Σ-eq (ap _ equal) (π₁ (is-reduced-is-prop (y ′∷ (z ∷ w)) _ _))
  mul'-mul-reduce x ((y ′∷ w) , red) | inr different with (eq x x)
  mul'-mul-reduce x ((y ′∷ w) , red) | inr different | inl obvious = refl
  mul'-mul-reduce x ((y ′∷ w) , red) | inr different | inr absurd =
    abort-nondep (absurd refl)
  mul'-mul-reduce x ((y ∷ w) , red) with (eq x x)
  mul'-mul-reduce x ((y ∷ w) , red) | inl obvious = refl
  mul'-mul-reduce x ((y ∷ w) , red) | inr absurd =
    abort-nondep (absurd refl)

freegroup-to-reduced : freegroup → reduced-word
freegroup-to-reduced = freegroup-rec-nondep reduced-word
  (ε , tt)
  mul-reduce
  mul'-reduce
  mul-mul'-reduce
  mul'-mul-reduce
  reduced-is-set

abstract
  mul-reduce-reduced : (x : A) (w : word) (red : is-reduced (x ∷ w))
    → mul-reduce x (w , tail-is-reduced x w red) ≡ ((x ∷ w) , red)
  mul-reduce-reduced x ε red = refl
  mul-reduce-reduced x (y ∷ w) red = refl
  mul-reduce-reduced x (y ′∷ w) red with (eq x y)
  mul-reduce-reduced x (y ′∷ w) red | inl absurd = abort-nondep (π₁ red absurd)
  mul-reduce-reduced x (y ′∷ w) red | inr obvious =
    Σ-eq refl (π₁ (is-reduced-is-prop (x ∷ (y ′∷ w)) _ _))

abstract
  mul'-reduce-reduced : (x : A) (w : word) (red : is-reduced (x ′∷ w))
    → mul'-reduce x (w , tail'-is-reduced x w red) ≡ ((x ′∷ w) , red)
  mul'-reduce-reduced x ε red = refl
  mul'-reduce-reduced x (y ∷ w) red with (eq x y)
  mul'-reduce-reduced x (y ∷ w) red | inl absurd = abort-nondep (π₁ red absurd)
  mul'-reduce-reduced x (y ∷ w) red | inr obvious =
    Σ-eq refl (π₁ (is-reduced-is-prop (x ′∷ (y ∷ w)) _ _))
  mul'-reduce-reduced x (y ′∷ w) red = refl

inv₁ : (w : reduced-word) → freegroup-to-reduced (reduced-to-freegroup w) ≡ w
inv₁ (ε , red) = refl
inv₁ ((x ∷ w) , red) = ap (mul-reduce x) (inv₁ (w , tail-is-reduced x w red))
                       ∘ mul-reduce-reduced x w red
inv₁ ((x ′∷ w) , red) =
  ap (mul'-reduce x) (inv₁ (w , tail'-is-reduced x w red))
  ∘ mul'-reduce-reduced x w red

reduced-to-freegroup-mul-reduce : (x : A) (v : reduced-word)
  → reduced-to-freegroup (mul-reduce x v) ≡ x · (reduced-to-freegroup v)
reduced-to-freegroup-mul-reduce x (ε , red) = refl
reduced-to-freegroup-mul-reduce x ((y ∷ v) , red) = refl
reduced-to-freegroup-mul-reduce x ((y ′∷ v) , red) with (eq x y)
reduced-to-freegroup-mul-reduce x ((.x ′∷ v) , red) | inl refl =
  ! (right-inverse-· x (reduced-to-freegroup (v , tail'-is-reduced x v red)))
reduced-to-freegroup-mul-reduce x ((y ′∷ v) , red) | inr different = refl

reduced-to-freegroup-mul'-reduce : (x : A) (v : reduced-word)
  → reduced-to-freegroup (mul'-reduce x v) ≡ x ⁻¹· (reduced-to-freegroup v)
reduced-to-freegroup-mul'-reduce x (ε , red) = refl
reduced-to-freegroup-mul'-reduce x ((y ∷ v) , red) with (eq x y)
reduced-to-freegroup-mul'-reduce x ((.x ∷ v) , red) | inl refl =
  ! (left-inverse-· x (reduced-to-freegroup (v , tail-is-reduced x v red)))
reduced-to-freegroup-mul'-reduce x ((y ∷ v) , red) | inr different = refl
reduced-to-freegroup-mul'-reduce x ((y ′∷ v) , red) = refl

inv₂ : (a : freegroup) → reduced-to-freegroup (freegroup-to-reduced a) ≡ a
inv₂ = freegroup-rec _
  refl
  (λ x u p → reduced-to-freegroup-mul-reduce x (freegroup-to-reduced u)
             ∘ ap (λ t → x · t) {y = u} p)
  (λ x u p → reduced-to-freegroup-mul'-reduce x (freegroup-to-reduced u)
             ∘ ap (λ t → x ⁻¹· t) {y = u} p)
  (λ x u t → π₁ (freegroup-is-set _ _ _ _))
  (λ x u t → π₁ (freegroup-is-set _ _ _ _))
  (λ u → truncated-is-truncated-S _ (freegroup-is-set _ _))

freegroup-equiv-reduced : freegroup ≃ reduced-word
freegroup-equiv-reduced =
  (freegroup-to-reduced , iso-is-eq _ reduced-to-freegroup inv₁ inv₂)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

module Filter where

open import Nat

data Bool : Set where
  false : Bool
  true  : Bool

infixr 40 _::_

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

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
filter p (x :: xs) | true  = x :: filter p xs
filter p (x :: xs) | false = filter p xs

infix 20 _⊆_

data _⊆_ {A : Set} : List A -> List A -> Set where
  stop : [] ⊆ []
  drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
  keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys

subset : {A : Set}(p : A -> Bool)(xs : List A) -> filter p xs ⊆ xs
subset p []        = stop
subset p (x :: xs) with p x
... | true = keep (subset p xs)
... | false = drop (subset p xs)

{-
subset p (x :: xs) with p x
subset p (x :: xs) | true  = keep (subset p xs)
subset p (x :: xs) | false = drop (subset p xs)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module local where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

infixr 15 _::_

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

reverse : {A : Set} -> List A -> List A
reverse {A} xs = rev xs nil
  where
    rev : List A -> List A -> List A
    rev  nil      ys = ys
    rev (x :: xs) ys = rev xs (x :: ys)

postulate
  xs : List Nat

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-

This file contains:
- Rijke finiteness is closed under forming Σ-type.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinType.Sigma where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.HITs.SetTruncation as Set
open import Cubical.HITs.SetTruncation.Fibers

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Data.FinSet
open import Cubical.Data.FinSet.DecidablePredicate
open import Cubical.Data.FinSet.Constructors
open import Cubical.Data.FinSet.Quotients
open import Cubical.Data.FinType

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidablePropositions
  hiding (DecProp) renaming (DecProp' to DecProp)

private
  variable
    ℓ ℓ' : Level

module _
  (X : Type ℓ )
  (Y : Type ℓ') (h : isFinType 1 Y)
  (f : X → Y)
  (q : (y : Y) → isFinType 0 (fiber f y)) where

  private
    ∥f∥₂ : ∥ X ∥₂ → ∥ Y ∥₂
    ∥f∥₂ = Set.map f

  module _ (y : Y) where

    isDecPropFiberRel : (x x' : ∥ fiber f y ∥₂) → isDecProp (fiberRel f y x x')
    isDecPropFiberRel x x' =
      isDecPropRespectEquiv (fiberRel1≃2 f y x x')
        (isDecProp∃ (_ , h .snd y y) (λ _ → _ , isDecProp≡ (_ , q y) _ _))

    isFinSetFiber∥∥₂' : isFinSet (fiber ∥f∥₂ ∣ y ∣₂)
    isFinSetFiber∥∥₂' =
      EquivPresIsFinSet (∥fiber∥₂/R≃fiber∥∥₂ f y)
        (isFinSetQuot (_ , q y) (fiberRel f y) (isEquivRelFiberRel f y) isDecPropFiberRel)

  isFinSetFiber∥∥₂ : (y : ∥ Y ∥₂) → isFinSet (fiber ∥f∥₂ y)
  isFinSetFiber∥∥₂ = Set.elim (λ _ → isProp→isSet isPropIsFinSet) isFinSetFiber∥∥₂'

  isFinType0Total : isFinType 0 X
  isFinType0Total = isFinSetTotal ∥ X ∥₂ (∥ Y ∥₂ , h .fst) ∥f∥₂ isFinSetFiber∥∥₂

module _
  (X : FinType ℓ 1)
  (Y : X .fst → FinType ℓ' 0) where

  isFinType0Σ : isFinType 0 (Σ (X .fst) (λ x → Y x .fst))
  isFinType0Σ =
    isFinType0Total (Σ (X .fst) (λ x → Y x .fst)) (X .fst) (X .snd) fst
      (λ x → EquivPresIsFinType 0 (fiberProjEquiv _ _ x) (Y x .snd))

-- the main result

isFinTypeΣ : {n : ℕ}
  (X : FinType ℓ (1 + n))
  (Y : X .fst → FinType ℓ' n)
  → isFinType n (Σ (X .fst) (λ x → Y x .fst))
isFinTypeΣ {n = 0} = isFinType0Σ
isFinTypeΣ {n = suc n} X Y .fst =
  isFinType0Σ (_ , isFinTypeSuc→isFinType1 {n = suc n} (X .snd))
    (λ x → _ , isFinType→isFinType0 {n = suc n} (Y x .snd))
isFinTypeΣ {n = suc n} X Y .snd a b =
  EquivPresIsFinType n (ΣPathTransport≃PathΣ a b)
    (isFinTypeΣ {n = n} (_ , X .snd .snd _ _) (λ _ → _ , Y _ .snd .snd _ _))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------------
-- Comparing styles for equational reasoning
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.Common.FOL.Relation.Binary.PreorderReasoning.Comparison where

infix  7 _≡_
infixl 9  _+_

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

trans : {A : Set}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

postulate
  ℕ               : Set
  zero            : ℕ
  _+_             : ℕ → ℕ → ℕ
  +-comm          : (m n : ℕ) → m + n ≡ n + m
  +-rightIdentity : (n : ℕ) → n + zero ≡ n

module Thesis where
  -- From Ulf's thesis (p. 112).

  infix  7 _≃_
  infix  6 chain>_
  infixl 5 _===_by_
  infix  4 _qed

  data _≃_ (x y : ℕ) : Set where
    prf : x ≡ y → x ≃ y

  chain>_ : (x : ℕ) → x ≃ x
  chain> x = prf refl

  _===_by_ : {x y : ℕ} → x ≃ y → (z : ℕ) → y ≡ z → x ≃ z
  prf p === z by q = prf (trans {_} {_} {_} p q)

  _qed : {x y : ℕ} → x ≃ y → x ≡ y
  prf p qed = p

  -- Example.
  +-leftIdentity : (n : ℕ) → zero + n ≡ n
  +-leftIdentity n =
    chain> zero + n
       === n + zero by +-comm zero n
       === n        by +-rightIdentity n
    qed

module SL where
  -- Adapted from the Agda standard library 0.8.1 (see
  -- Relation/Binary/PreorderReasoning.agda).

  infix  7 _≃_
  infix  4 begin_
  infixr 5 _≡⟨_⟩_
  infix  6 _∎

  data _≃_ (x y : ℕ) : Set where
    prf : x ≡ y → x ≃ y

  begin_ : {x y : ℕ} → x ≃ y → x ≡ y
  begin prf x≡y = x≡y

  _≡⟨_⟩_ : (x : ℕ){y z : ℕ} → x ≡ y → y ≃ z → x ≃ z
  _ ≡⟨ x≡y ⟩ prf y≡z = prf (trans x≡y y≡z)

  _∎ : (x : ℕ) → x ≃ x
  _∎ _ = prf refl

  -- Example.
  +-leftIdentity : (n : ℕ) → zero + n ≡ n
  +-leftIdentity n =
    begin
      zero + n ≡⟨ +-comm zero n ⟩
      n + zero ≡⟨ +-rightIdentity n ⟩
      n
    ∎

module NonWrapper where
  -- A set of combinators without request a wrapper data type (Mu,
  -- S.-C., Ko, H.-S. and Jansson, P. (2009)).

  infixr 5 _≡⟨_⟩_
  infix  6 _∎

  _≡⟨_⟩_ : (x : ℕ){y z : ℕ} → x ≡ y → y ≡ z → x ≡ z
  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

  _∎ : (x : ℕ) → x ≡ x
  _∎ _ = refl

  -- Example.
  +-leftIdentity : (n : ℕ) → zero + n ≡ n
  +-leftIdentity n = zero + n ≡⟨ +-comm zero n ⟩
                     n + zero ≡⟨ +-rightIdentity n ⟩
                     n        ∎

------------------------------------------------------------------------------
-- References
--
-- Mu, S.-C., Ko, H.-S. and Jansson, P. (2009). Algebra of programming
-- in Agda: Dependent types for relational program derivation. Journal
-- of Functional Programming 19.5, pp. 545–579.


text:
module _ where

data N : Set where
  zero : N
  suc  : N → N

record P : Set where
  constructor p
  field fst : N
        snd : N

open P

-- f = λ z → z   internally
f : P → P
f z = p (fst z) (snd z)

-- This should also be λ z → z, but was not due to #2157.
g : P → P
g (p x y) = p x y

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --without-K #-}
module JVM.Types where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Product
open import Data.List
open import Data.String

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Nullary

-- Primitive types
data Ty : Set where
  boolean                   : Ty
  byte short int long char  : Ty
  ref                       : String → Ty
  array                     : Ty → Ty

Integer = ref "java/lang/Integer"
Boolean = ref "java/lang/Boolean"

data Ret : Set where
  ty   : Ty → Ret
  void : Ret      -- clearly void is not a type... right? (Spec accurate)

IsIntegral : Ty → Set
IsIntegral boolean = ⊤ -- int instructions compatible with boolean
IsIntegral byte    = ⊤
IsIntegral short   = ⊤
IsIntegral int     = ⊤
IsIntegral long    = ⊤
IsIntegral char    = ⊤
IsIntegral _       = ⊥

StackTy  = List Ty
LocalsTy = List Ty
Labels   = List StackTy

_:?:_ : Ret → StackTy → StackTy
ty a :?: ψ = a ∷ ψ
void :?: ψ = ψ

record Fun : Set where
  constructor _/_:⟨_⟩_
  field
    cls     : String
    name    : String
    sf_args : List Ty
    sf_ret  : Ret

record Fld : Set where
  constructor _/_∶_
  field
    fld_cls  : String
    fld_name : String
    fld_ty   : Ty

data Constant : Set where
  class     : String → Constant
  fieldref  : Fld → Constant
  staticref : Fld → Constant -- in the actual constant pool static fields are fields
  virtual   : Fun → Constant
  staticfun : Fun → Constant

Constantpool = List Constant
FrameTy      = LocalsTy

variable
  𝑪                : Constantpool
  𝑹₁ 𝑹₂ 𝑹₃ 𝑹₄ 𝑹  : LocalsTy
  𝑭₁ 𝑭₂ 𝑭₃ 𝑭₄ 𝑭  : FrameTy
  𝑎 𝑏              : Fld
  𝑐 𝑛 𝑚           : String
  𝑓 𝑔              : Fun
  a b c r s t      : Ty
  as bs cs         : List Ty
  ψ₁ ψ₂ ψ₃ ψ      : StackTy  -- stack typings