module Chapter7.Derivable.Equality where
open import Level
open import Function
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.Maybe
open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint
open import Chapter7.Derivable
infix 12 _`+_
data EqDesc : Desc zero → Set₁ where
`1 : EqDesc `1
`var : EqDesc `var
_`×_ : ∀{Dl Dr} → (l : EqDesc Dl)(r : EqDesc Dr) → EqDesc (Dl `× Dr)
_`+_ : ∀{Dl Dr} → (l : EqDesc Dl)(r : EqDesc Dr) → EqDesc (Dl `+ Dr)
`Σ : ∀{D : Bool → Desc zero}
(T : (b : Bool) → EqDesc (D b)) → EqDesc (`Σ Bool D)
equalityCompat : (D : Desc zero) → SemiDec (EqDesc D)
equalityCompat `1 = just `1
equalityCompat `var = just `var
equalityCompat (x `× y) with equalityCompat x | equalityCompat y
... | just ex | just ey = just (ex `× ey)
... | just p | nothing = nothing
... | nothing | t₂ = nothing
equalityCompat (x `+ y) with equalityCompat x | equalityCompat y
... | just ex | just ey = just (ex `+ ey)
... | just p | nothing = nothing
... | nothing | t₂ = nothing
equalityCompat (`Σ S T) = nothing
equalityCompat (`Π S T) = nothing
private
out : {D : Desc zero} → μ D → ⟦ D ⟧ (μ D)
out ⟨ xs ⟩ = xs
module H (D : Desc zero)(q : EqDesc D) where
uninj₁ : ∀{A B : Set}{x y : A} → inj₁ {_}{_}{_}{B} x ≡ inj₁ y → x ≡ y
uninj₁ refl = refl
uninj₂ : ∀{A B : Set}{x y : B} → inj₂ {_}{_}{A} x ≡ inj₂ y → x ≡ y
uninj₂ refl = refl
unpair₁ : ∀{A : Set}{B : A → Set}{x y : A}{p : B x}{q : B y} → (x , p) ≡ (y , q) → x ≡ y
unpair₁ refl = refl
unpair₂ : ∀{A : Set}{B : A → Set}{x : A}{p q : B x} → _,_ {_}{_}{_}{B} x p ≡ (x , q) → p ≡ q
unpair₂ refl = refl
help : (R : Desc zero) → EqDesc R → (x y : ⟦ R ⟧ (μ D)) → Dec (x ≡ y)
help `1 `1 (lift tt) (lift tt) = yes refl
help `var `var ⟨ xs ⟩ ⟨ ys ⟩ with help D q xs ys
help `var `var ⟨ .ys ⟩ ⟨ ys ⟩ | yes refl = yes refl
help `var `var ⟨ xs ⟩ ⟨ ys ⟩ | no ¬p = no (¬p ∘ cong out)
help (R₁ `× R₂) (q₁ `× q₂) (x₁ , x₂) (y₁ , y₂)
with help R₁ q₁ x₁ y₁ | help R₂ q₂ x₂ y₂
help (R₁ `× R₂) (q₁ `× q₂) (.y₁ , .y₂) (y₁ , y₂) | yes refl | yes refl = yes refl
help (R₁ `× R₂) (q₁ `× q₂) (.y₁ , x₂) (y₁ , y₂) | yes refl | no ¬p = no (¬p ∘ cong (λ {(x , y) → y}))
help (R₁ `× R₂) (q₁ `× q₂) (x₁ , x₂) (y₁ , y₂) | no ¬p | t = no (¬p ∘ cong (λ {(x , y) → x}))
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ x₁) (inj₁ x₂)
with help R₁ q₁ x₁ x₂
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ .x₂) (inj₁ x₂) | yes refl = yes refl
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ x) (inj₁ y) | no ¬p = no (¬p ∘ uninj₁)
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ x) (inj₂ y)
with help R₂ q₂ x y
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ .y₁) (inj₂ y₁) | yes refl = yes refl
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ x) (inj₂ y) | no ¬p = no (¬p ∘ uninj₂)
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₁ x₁) (inj₂ y₁) = no (λ ())
help (R₁ `+ R₂) (q₁ `+ q₂) (inj₂ y₁) (inj₁ x₁) = no (λ ())
help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (b₂ , ts₂) with b₁ ≟ b₂
help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (.b₁ , ts₂) | yes refl with help (T b₁) (TEq b₁) ts₁ ts₂
help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (.b₁ , .ts₁) | yes refl | yes refl = yes refl
help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (.b₁ , ts₂) | yes refl | no ¬p = no (¬p ∘ unpair₂)
help (`Σ .Bool T) (`Σ TEq) (b₁ , ts₁) (b₂ , ts₂) | no ¬p = no (¬p ∘ unpair₁)
help (`Π S T) () x₁ y₁
equalityDerive : {D : Desc zero} → EqDesc D → (x y : μ D) → Dec (x ≡ y)
equalityDerive {D} q ⟨ x ⟩ ⟨ y ⟩ with H.help D q D q x y
equalityDerive q ⟨ .y ⟩ ⟨ y ⟩ | yes refl = yes refl
equalityDerive q ⟨ x ⟩ ⟨ y ⟩ | no ¬p = no (¬p ∘ cong out)
Equality : Derive (λ D → (x y : μ D) → Dec (x ≡ y))
Equality = record { subUniverse = EqDesc
; belongTo = equalityCompat
; derive = equalityDerive }