module IID-Proof-Setup where

open import LF
open import Identity
open import IID
open import IIDr
open import DefinitionalEquality

OPg : Set -> Set1
OPg I = OP I I

-- Encoding indexed inductive types as non-indexed types.
ε : {I : Set}(γ : OPg I) -> OPr I
ε (ι i)     j = σ (i == j) (\_ -> ι ★)
ε (σ A γ)   j = σ A (\a -> ε (γ a) j)
ε (δ H i γ) j = δ H i (ε γ j)

-- Adds a reflexivity proof.
g→rArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (a : Args γ U) ->
	      rArgs (ε γ) U (index γ U a)
g→rArgs (ι e)     U a	  = < refl | ★ >
g→rArgs (σ A γ)   U < a | b > = < a | g→rArgs (γ a) U b >
g→rArgs (δ H i γ) U < g | b > = < g | g→rArgs γ U b >

-- Strips the equality proof.
r→gArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (i : I)(a : rArgs (ε γ) U i) ->
	      Args γ U
r→gArgs (ι i)     U j _	    = ★
r→gArgs (σ A γ)   U j < a | b > = < a | r→gArgs (γ a) U j b >
r→gArgs (δ H i γ) U j < g | b > = < g | r→gArgs γ U j b >

-- Converting an rArgs to a gArgs and back is (provably, not definitionally)
-- the identity.
r←→gArgs-subst :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (C : (i : I) -> rArgs (ε γ) U i -> Set)
  (i : I)(a : rArgs (ε γ) U i) ->
  (C (index γ U (r→gArgs γ U i a))
     (g→rArgs γ U (r→gArgs γ U i a))
  ) -> C i a

r←→gArgs-subst {I} (ι i) U C j < p | ★ > m =
  elim== i (\k q -> C k < q | ★ >) m j p

r←→gArgs-subst (σ A γ)   U C j < a | b > m = 
  r←→gArgs-subst (γ a) U (\i c -> C i < a | c >) j b m

r←→gArgs-subst (δ H i γ) U C j < g | b > m =
  r←→gArgs-subst γ U (\i c -> C i < g | c >) j b m

-- r←→gArgs-subst eliminates the identity proof stored in the rArgs. If this proof is
-- by reflexivity r←→gArgs-subst is a definitional identity. This is the case
-- when a = g→rArgs a'
r←→gArgs-subst-identity :
  {I  : Set}(γ : OPg I)(U : I -> Set)
  (C  : (i : I) -> rArgs (ε γ) U i -> Set)
  (a' : Args γ U) ->
  let a = g→rArgs γ U a'
      i = index γ U a' in
  (h : C (index γ U (r→gArgs γ U i a))
	 (g→rArgs γ U (r→gArgs γ U i a))
  ) -> r←→gArgs-subst γ U C i a h ≡ h
r←→gArgs-subst-identity (ι i)	  U C _		h = refl-≡
r←→gArgs-subst-identity (σ A γ)	  U C < a | b > h = r←→gArgs-subst-identity (γ a) U C' b h
  where C' = \i c -> C i < a | c >
r←→gArgs-subst-identity (δ H i γ) U C < g | b > h = r←→gArgs-subst-identity γ U C' b h
  where C' = \i c -> C i < g | c >

-- Going the other way around is definitionally the identity.
g←→rArgs-identity :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (a : Args γ U) ->
  r→gArgs γ U (index γ U a) (g→rArgs γ U a) ≡ a
g←→rArgs-identity (ι i)	    U ★		= refl-≡
g←→rArgs-identity (σ A γ)   U < a | b > = cong-≡ (\ ∙ -> < a | ∙ >) (g←→rArgs-identity (γ a) U b)
g←→rArgs-identity (δ H i γ) U < g | b > = cong-≡ (\ ∙ -> < g | ∙ >) (g←→rArgs-identity γ U b)

-- Corresponding conversion functions for assumptions to inductive occurrences.
-- Basically an identity function.
g→rIndArg : {I : Set}(γ : OPg I)(U : I -> Set)
        (i : I)(a : rArgs (ε γ) U i) ->
        IndArg γ U (r→gArgs γ U i a) -> IndArg (ε γ i) U a
g→rIndArg (ι j)	    U i < h | ★ > ()
g→rIndArg (σ A γ)   U i < a | b > v       = g→rIndArg (γ a) U i b v
g→rIndArg (δ A j γ) U i < g | b > (inl a) = inl a
g→rIndArg (δ A j γ) U i < g | b > (inr v) = inr (g→rIndArg γ U i b v)

-- Basically we can substitute general inductive occurences for the encoded
-- restricted inductive occurrences.
g→rIndArg-subst :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i)
    (v : IndArg γ U (r→gArgs γ U i a)) ->
    C (IndIndex (ε γ i) U a (g→rIndArg γ U i a v))
      (Ind	(ε γ i) U a (g→rIndArg γ U i a v)) ->
    C (IndIndex γ U (r→gArgs γ U i a) v)
      (Ind	γ U (r→gArgs γ U i a) v)
g→rIndArg-subst (ι j)	  U C i < p | _ > ()	  h
g→rIndArg-subst (σ A γ)	  U C i < a | b > v	  h = g→rIndArg-subst (γ a) U C i b v h
g→rIndArg-subst (δ A j γ) U C i < g | b > (inl a) h = h
g→rIndArg-subst (δ A j γ) U C i < g | b > (inr v) h = g→rIndArg-subst γ U C i b v h

-- g→rIndArg-subst is purely book-keeping. On the object level it's definitional identity.
g→rIndArg-subst-identity :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i)
    (v : IndArg γ U (r→gArgs γ U i a))
    (h : C (IndIndex (ε γ i) U a (g→rIndArg γ U i a v))
	   (Ind	(ε γ i) U a (g→rIndArg γ U i a v))
    ) -> g→rIndArg-subst γ U C i a v h ≡ h
g→rIndArg-subst-identity (ι j)	   U C i < p | _ > ()	   h
g→rIndArg-subst-identity (σ A γ)   U C i < a | b > v	   h =
  g→rIndArg-subst-identity (γ a) U C i b v h
g→rIndArg-subst-identity (δ A j γ) U C i < g | b > (inl a) h = refl-≡
g→rIndArg-subst-identity (δ A j γ) U C i < g | b > (inr v) h =
  g→rIndArg-subst-identity γ U C i b v h

-- And finally conversion of induction hypotheses. This goes the other direction.
r→gIndHyp :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i) ->
    IndHyp (ε γ i) U C a -> IndHyp γ U C (r→gArgs γ U i a)
r→gIndHyp γ U C i a h v = g→rIndArg-subst γ U C i a v (h (g→rIndArg γ U i a v))