-- IIRDg is expressible in IIRDr + Identity
module Proof where

import LF
import IIRD
import IIRDr
import DefinitionalEquality
import Identity
import Proof.Setup
import Logic.ChainReasoning1 as Chain
import Logic.ChainReasoning0 as Chain₀

open LF
open IIRD
open IIRDr
open DefinitionalEquality
open Identity
open Proof.Setup

-- We can then define general IIRDs using the ε function from Proof.Setup.
Ug : {I : Set}{D : I -> Set1} -> OPg I D -> I -> Set
Ug γ = Ur (ε γ)

Tg : {I : Set}{D : I -> Set1}(γ : OPg I D)(i : I) -> Ug γ i -> D i
Tg γ = Tr (ε γ)

introg : {I : Set}{D : I -> Set1}(γ : OPg I D)(a : Gu γ (Ug γ) (Tg γ)) ->
         Ug γ (Gi γ (Ug γ) (Tg γ) a)
introg γ a = intror (G→H γ (Ug γ) (Tg γ) a)

-- TODO: is this the best way of writing the type (just copied and pasted from
-- normalised goal type in Tg-equality)
Tg-eq : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
        (a : Gu γ U T) ->
        Kt (ε γ (π₀' (Kt γ U T a))) U T (G→H γ U T a) ≡₁ π₁' (Kt γ U T a)
Tg-eq {I}{D} (ι < i | e >') U T ★         = reduction==₁ (\z _ -> D z) e
Tg-eq        (σ A γ)        U T < a | b > = Tg-eq (γ a) U T b
Tg-eq        (δ A i γ)      U T < g | b > = Tg-eq (γ (T « i × g »)) U T b

Tg-equality : {I : Set}{D : I -> Set1}(γ : OPg I D)(a : Gu γ (Ug γ) (Tg γ)) ->
              Tg γ (Gi γ (Ug γ) (Tg γ) a) (introg γ a) ≡₁ Gt γ (Ug γ) (Tg γ) a
Tg-equality γ a = Tg-eq γ (Ug γ) (Tg γ) a

Rg : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1)
     (h : (a : Gu γ (Ug γ) (Tg γ)) -> KIH γ (Ug γ) (Tg γ) F a -> F (Gi γ (Ug γ) (Tg γ) a) (introg γ a))
     (i : I)(u : Ug γ i) -> F i u
Rg {I}{D} γ F h = Rr (ε γ) F \i a ih ->
                    G→H∘H→G-subst γ U T
                                  (\i a -> F i (intror a))
                                  i a (lem1 i a ih)
  where
    U = Ug γ
    T = Tg γ
    lem1 : (i : I)(a : Hu (ε γ) U T i) ->
           KIH (ε γ i) U T F a ->
           F (Gi γ U T (H→G γ U T i a))
             (intror (G→H γ U T (H→G γ U T i a)))
    lem1 i a ih = h (H→G γ U T i a) (\v -> εIArg-subst γ U T F i a v (ih (εIArg γ U T i a v)))

module Chain-≡ = Chain _≡₁_ (\x -> refl-≡₁ {_}{x}) trans-≡₁
open Chain-≡

module Chain-≡₀ = Chain₀ _≡_ (\x -> refl-≡ {_}{x}) trans-≡
open Chain-≡₀ renaming (chain>_ to chain>₀_ _===_ to _===₀_ _by_ to _by₀_)

Rg-eq : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
        (F : (i : I) -> U i -> Set1)(intro : (a : Gu γ U T) -> U (Gi γ U T a))
        (g : (i : I)(u : U i) -> F i u)
        (h : (a : Gu γ U T) -> KIH γ U T F a -> F (Gi γ U T a) (intro a))
        (a : Gu γ U T) ->
        let i  = Gi γ U T a
            a' = G→H γ U T a
        in h (H→G γ U T i a') (\v -> εIArg-subst γ U T F i a' v (Kmap (ε γ i) U T F g a' (εIArg γ U T i a' v)))
           ≡₁ h a (Kmap γ U T F g a)
Rg-eq {I}{D} γ U T F intro g h a = app-≡₁
  (cong-≡₁⁰ h (H→G∘G→H-identity γ U T a))
  (η-≡₁⁰ \x y p ->
    chain>  εIArg-subst γ U T F i a' x (Kmap (ε γ i) U T F g a' (εIArg γ U T i a' x))
        === Kmap (ε γ i) U T F g a' (εIArg γ U T i a' x)
              by εIArg-identity γ U T F a x (Kmap (ε γ i) U T F g a' (εIArg γ U T i a' x))
        === Kmap γ U T F g a y
              by app-≡₁⁰
                  (cong-≡₁⁰ g
                    (chain>₀ KIArg→I (ε γ i) U T a' (εIArg γ U T i a' x)
                        ===₀ KIArg→I γ U T (H→G γ U T i a') x   by₀  εIArg→I-identity γ U T i a' x
                        ===₀ KIArg→I γ U T a y                  by₀
                                app-≡₀ (cong-≡' (KIArg→I γ U T)
                                                (H→G∘G→H-identity γ U T a)
                                       ) p
                    )
                  )
                  (chain>₀ KIArg→U (ε γ i) U T a' (εIArg γ U T i a' x)
                      ===₀ KIArg→U γ U T (H→G γ U T i a') x   by₀  εIArg→U-identity γ U T i a' x
                      ===₀ KIArg→U γ U T a y                  by₀
                              app-≡₀ (cong-≡' (KIArg→U γ U T)
                                              (H→G∘G→H-identity γ U T a)
                                     ) p
                  )
  )
  where
    i  = Gi γ U T a
    a' = G→H γ U T a

Rg-equality : {I : Set}{D : I -> Set1}(γ : OPg I D)(F : (i : I) -> Ug γ i -> Set1)
              (h : (a : Gu γ (Ug γ) (Tg γ)) -> KIH γ (Ug γ) (Tg γ) F a -> F (Gi γ (Ug γ) (Tg γ) a) (introg γ a))
              (a : Gu γ (Ug γ) (Tg γ)) ->
              Rg γ F h (Gi γ (Ug γ) (Tg γ) a) (introg γ a)
              ≡₁ h a (Kmap γ (Ug γ) (Tg γ) F (Rg γ F h) a)
Rg-equality {I}{D} γ F h a =
  chain> Rg γ F h (Gi γ U T a) (introg γ a)
--      === h'' i a' ih    by  refl-≡₁
--      === G→H∘H→G-subst γ U T F' i a' (h' i a' ih)
--                         by  refl-≡₁
     === h' i a' ih     by G→H∘H→G-identity γ U T F' a (h' i a' ih)
--      === h (H→G γ U T i a') (\v -> εIArg-subst γ U T F i a' v (ih (εIArg γ U T i a' v)))
--                         by refl-≡₁
     === h a (Kmap γ U T F (Rg γ F h) a)      by  Rg-eq γ U T F (introg γ) (Rg γ F h) h a
  where
    U  = Ug γ
    T  = Tg γ
    F' = \i a -> F i (intror a)
    i  = Gi γ U T a
    a' = G→H γ U T a
    h' : (i : I)(a : Hu (ε γ) U T i) -> KIH (ε γ i) U T F a -> F _ _
    h' = \i a ih -> h (H→G γ U T i a) \v ->
                  εIArg-subst γ U T F i a v
                      (ih (εIArg γ U T i a v))
--     h'' = \i a ih -> G→H∘H→G-subst γ U T F' i a (h' i a ih)
    ih  = Kmap (ε γ i) U T F (Rg γ F h) a'