{-# OPTIONS --type-in-type #-}

-- Proving induction principles via free theorems from parametricity.
-- The --type-in-type is so that Church-encoded types are still
-- Sets. That may not be necessary, but it avoids things like
-- needing equality and whatnot at multiple levels, and lets one
-- eliminate over the encoded types (which seems handy for the
-- less trivial types).

module ParamInduction where

open import Relation.Binary.PropositionalEquality

const : ∀{A : Set} {B : Set}  (x : A)  B  A
const x _ = x

_⇔_ : Set  Set  Set
A  B = A  B  Set

infixl 0 _$_
_$_ : ∀{A : Set} {B : A  Set}  ((x : A)  B x)  (x : A)  B x
f $ x = f x

-- Extensionality of functions is something we'll also be needing.
postulate
  ext : {A : Set} {B : A  Set} (f g : (x : A)  B x)
       (∀ x  f x  g x)  f  g


-- The empty type is the set that entails any other set.
 : Set
 = (R : Set)  R

postulate
  -- ∀ f. f b = b, total functions must be strict
  free-⊥ : {R S : Set} (bot : ) (f : R  S)  f (bot R)  bot S

  pm-⊥ : (A B : Set) (R : A  B) (b : )  R (b A) (b B)

-- We don't even need parametricity for the induction principle!
⊥-induction : {P :   Set}  (b : )  P b
⊥-induction {P} b = b (P b)


-- The unit type is the type of the identity function, as it is
-- the only function with that type.
 : Set
 = (R : Set)  R  R

postulate
  pm-⊤ : (A B : Set) (R : A  B) (u : ) (x : A) (y : B)
        R x y  R (u A x) (u B y)

-- ∀ f. f ∘ id = id ∘ f
free-⊤ : {R S : Set} (u : ) (f : R  S)   x  f (u R x)  u S (f x)
free-⊤ {R} {S} u f x = pm-⊤ R S  x y  f x  y) u x (f x) refl

id : 
id R x = x

lemma₀ : (u : )  id  u
lemma₀ u = ext id u λ R  ext (id R) (u R) λ x  free-⊤ u (const x) x

lemma₁ : (u : )  id  u
lemma₁ u = ext id u λ R  ext (id R) (u R) λ x  
           pm-⊤ R R  _ y  x  y) u x x refl

⊤-induction : {P :   Set}  P id   u  P u
⊤-induction {P} Pid u rewrite lemma₀ u = Pid


-- Standard representation of pairs
_×_ : Set  Set  Set
A × B = (R : Set)  (A  B  R)  R

postulate
  -- Yikes!
  pm-× : ∀{A B} C D 
        (R₁ : A  A) (R₂ : B  B) (R₃ : C  D) 
        (p : A × B)
        (k₀ : A  B  C) (k₁ : A  B  D)
        (∀ x₀ x₁ y₀ y₁  R₁ x₀ x₁  R₂ y₀ y₁  R₃ (k₀ x₀ y₀) (k₁ x₁ y₁))
        R₃ (p C k₀) (p D k₁)

-- Bam!
free-× : ∀{A B R S}
        (f : A  A) (g : B  B)
        (k₀ : A  B  R) (k₁ : A  B  S)
        (h : R  S)
        (p : A × B)
        (∀ x y  h (k₀ x y)  k₁ (f x) (g y))
        h (p R k₀)  p S k₁
free-× {A} {B} {R} {S} f g k₀ k₁ h p pf =
  pm-× R S  x₀ x₁  f x₀  x₁)
            y₀ y₁  g y₀  y₁) 
            x y  h x  y)
           p k₀ k₁ λ x₀ x₁ y₀ y₁ fx₀≡x₁ gy₀≡y₁ 
           subst  x  h (k₀ x₀ y₀)  k₁ x y₁) fx₀≡x₁
           (subst  y  h (k₀ x₀ y₀)  k₁ (f x₀) y) gy₀≡y₁ (pf x₀ y₀))

_,_ : {A B : Set}  A  B  A × B
(x , y) R k = k x y

fst : ∀{A B}  A × B  A
fst {A} pair = pair A  x _  x)

snd : ∀{A B}  A × B  B
snd {B = B} pair = pair B  _ y  y)

×-lemma₀ : ∀{A B}  (p : A × B)  p (A × B) _,_  p
×-lemma₀ {A} {B} p = ext q     p     λ R  
                     ext (q R) (p R) λ k 
                     free-× (id A) (id B) _,_ k  q  q R k) p  _ _  refl)
 where
 q : A × B
 q = p (A × B) _,_

×-lemma₁ : ∀{A B R}  (p : A × B) (k : A  B  R)
          k (fst p) (snd p)  p R k
×-lemma₁ {A} {B} {R} p k = subst  q  k (fst q) (snd q)  p R k) (×-lemma₀ p)
                           (free-× (id A) (id B) _,_ k  q  k (fst q) (snd q))
                                 p  x y  refl))


×-η : ∀{A B}  (p : A × B)  (fst p , snd p)  p
×-η {A} {B} p = ext (fst p , snd p) p  R 
                ext ((fst p , snd p) R) (p R)  k 
                ×-lemma₁ p k))


×-induction : ∀{A B} {P : A × B  Set}
             ((x : A)  (y : B)  P (x , y))
             (p : A × B)  P p
×-induction {A} {B} {P} f p rewrite sym (×-η p) = f (fst p) (snd p)




Σ : (A : Set) (P : A  Set)  Set
Σ A P = (R : Set)  ((x : A)  P x  R)  R

postulate
  pm-Σ : ∀{A P} C D
        (R₁ : A  A) (R₂ :  x₀ x₁  R₁ x₀ x₁  P x₀  P x₁) (R₃ : C  D)
        (p : Σ A P)
        (k₀ : (x : A)  P x  C) (k₁ : (x : A)  P x  D)
        (∀ x₀ x₁  (r : R₁ x₀ x₁)  (w₀ : P x₀) (w₁ : P x₁)
                   R₂ x₀ x₁ r w₀ w₁  R₃ (k₀ x₀ w₀) (k₁ x₁ w₁))
        R₃ (p C k₀) (p D k₁)

_⟩_ : ∀{A P}  (x : A)  P x  Σ A P
(x  w) R k = k x w

Σ-prelemma : ∀{A P R}
            (k : (x : A)  P x  R)
            (x₀ x₁ : A) (eq : x₀  x₁)
            (w₀ : P x₀) (w₁ : P x₁)
            w₀  subst P (sym eq) w₁
            k x₀ w₀  k x₁ w₁
Σ-prelemma k x₀ .x₀ refl .w₁ w₁ refl = refl
           
Σ-lemma₀ : ∀{A P}  (p : Σ A P)  p (Σ A P) _⟩_  p
Σ-lemma₀ {A} {P} p = ext q     p     λ R 
                     ext (q R) (p R) λ k 
                     pm-Σ (Σ A P) R _≡_
                           x₀ x₁ x₀≡x₁ w₀ w₁  w₀  subst P (sym x₀≡x₁) w₁)
                           q e  q R k  e) p _⟩_ k
                          (Σ-prelemma k)
 where
 q : Σ A P
 q = p (Σ A P) _⟩_

module Σ₁ (A : Set) (P : A  Set) where
  Q : Σ A P  Set
  Q q = Σ A λ x  Σ (P x) λ w  q  x  w

  R₁ : A  A  Set
  R₁ = _≡_

  R₂ : (x₀ x₁ : A)  R₁ x₀ x₁  P x₀  P x₁  Set
  R₂ x₀ x₁ r w₀ w₁ = 

  R₃ : Σ A P  Σ A P  Set
  R₃ _ = Q

Σ-lemma₁ : ∀{A P}  (p : Σ A P)  Σ A λ x  Σ (P x) λ w  p  x  w
Σ-lemma₁ {A} {P} p = subst Q (Σ-lemma₀ p)
                     (pm-Σ (Σ A P) (Σ A P) R₁ R₂ R₃ p _⟩_ _⟩_
                        x₀ x₁ _ w₀ w₁ _  x₁  (w₁  refl)))
 where
 open Σ₁ A P

uncurry : ∀{A : Set} {P : A  Set} {C : Σ A P  Set}
         (f : (x : A)  (w : P x)  C (x  w))
         (p : Σ A P)  C p
uncurry {A} {P} {C} f p = Σ-lemma₁ p (C p) λ x sg 
                          sg (C p) λ w p≡x⟩w 
                          subst C (sym p≡x⟩w) (f x w)

-- If we try to make π₀ use uncurry, then the P (π₀ (x ⟩ w)) result
-- type of the lambda expression in π₁ will be a mess, and we'll need
-- to *prove* that it's equal to P x (substitution with equality
-- postulates is the main culprit, I think). The standard Church-encoding
-- definition normalizes π₀ (x ⟩ w) to x, which is much easier.
π₀ : ∀{A P}  Σ A P  A
π₀ {A} p = p A  x _  x)

π₁ : ∀{A P}  (p : Σ A P)  P (π₀ p)
π₁ {A} {P} p = uncurry {C = λ q  P (π₀ q)}  x w  w) p




_⊎_ : Set  Set  Set
A  B = (R : Set)  (A  R)  (B  R)  R

postulate
  -- Yikes again
  pm-⊎ : ∀{A B} C D
        (R₁ : A  A) (R₂ : B  B) (R₃ : C  D)
        (s : A  B)
        (l₀ : A  C) (r₀ : B  C)
        (l₁ : A  D) (r₁ : B  D)
        (∀ x₀ x₁  R₁ x₀ x₁  R₃ (l₀ x₀) (l₁ x₁))
        (∀ y₀ y₁  R₂ y₀ y₁  R₃ (r₀ y₀) (r₁ y₁))
        R₃ (s C l₀ r₀) (s D l₁ r₁)

free-⊎ : {A B R S : Set}
        (f : A  A)  (g : B  B)
        (h : R  S)
        (l₀ : A  R)  (r₀ : B  R)
        (l₁ : A  S)  (r₁ : B  S)
        (s : A  B)
        (∀ x  h (l₀ x)  l₁ (f x))
        (∀ y  h (r₀ y)  r₁ (g y))
        h (s R l₀ r₀)  s S l₁ r₁
free-⊎ {A} {B} {R} {S} f g h l₀ r₀ l₁ r₁ s pfl pfr =
  pm-⊎ R S  x₀ x₁  f x₀  x₁)
            y₀ y₁  g y₀  y₁)
            x y  h x  y)
           s l₀ r₀ l₁ r₁
            x₀ x₁ fx₀≡x₁  subst  x  h (l₀ x₀)  l₁ x) fx₀≡x₁ (pfl x₀))
            y₀ y₁ gy₀≡y₁  subst  y  h (r₀ y₀)  r₁ y) gy₀≡y₁ (pfr y₀))

inl : ∀{A B}  A  A  B
inl x R f _ = f x

inr : ∀{A B}  B  A  B
inr y R _ g = g y


-- A simpler disjunction first
Bool : Set
Bool = (R : Set)  R  R  R

true : Bool
true _ t _ = t

false : Bool
false _ _ f = f

postulate
  pm-B :  A B  (R : A  B)  (b : Bool)  (x₀ y₀ : A) (x₁ y₁ : B)
                R x₀ x₁  R y₀ y₁  R (b A x₀ y₀) (b B x₁ y₁)

free-B : ∀{R S}  (f : R  S)  (x y : R)
        (b : Bool)  f (b R x y)  b S (f x) (f y)
free-B {R} {S} f x y b =
  pm-B R S  x y  f x  y) b x y (f x) (f y) refl refl

B-lemma₀ : (b : Bool)  b Bool true false  b
B-lemma₀ b = ext c       b       λ R 
             ext (c R)   (b R)   λ t 
             ext (c R t) (b R t) λ f 
             free-B  d  d R t f) true false b
 where
 c : Bool
 c = b Bool true false

B-lemma₁ : ∀{A}  (x : A)  (b : Bool)  x  b A x x
B-lemma₁ {A} x b = free-B (const x) x x b

-- This needs the full parametricity theorem, not just the free theorem,
-- as far as I can tell.
B-lemma₂ : ∀{A}  (x y : A)  (b : Bool)  (b A x y  x)  (b A x y  y)
B-lemma₂ {A} x y b = pm-B A A R b x y x y (inl refl) (inr refl)
 where
 R : A  A  Set
 R _ e = (e  x)  (e  y)

B-lemma₃ : (b : Bool)  (b  true)  (b  false)
B-lemma₃ b rewrite sym (B-lemma₀ b) = B-lemma₂ true false b

B-induction : ∀{P : Bool  Set}  P true  P false   b  P b
B-induction {P} Pt Pf b = B-lemma₃ b (P b)
                           b≡t  subst P (sym b≡t) Pt) 
                           b≡f  subst P (sym b≡f) Pf)







⊎-lemma₀ : ∀{A B}  (s : A  B)  s (A  B) inl inr  s
⊎-lemma₀ {A} {B} s = ext t s λ R 
                     ext (t R) (s R) λ l 
                     ext (t R l) (s R l) λ r 
                     free-⊎ (id A) (id B)  v  v R l r) inl inr l r s
                             x  refl)  y  refl)
 where
 t : A  B
 t = s (A  B) inl inr

⊎-lemma₁ : ∀{A B C}  (f : A  C) (g : B  C)  (s : A  B)
          (Σ A λ x  s C f g  f x)  (Σ B λ y  s C f g  g y)
⊎-lemma₁ {A} {B} {C} f g s = pm-⊎ C C _≡_ _≡_ R s f g f g
                              x₀ x₁ x₀≡x₁  inl (x₁  refl))
                              y₀ y₁ y₀≡y₁  inr (y₁  refl)) 
 where
 R : C  C  Set
 R _ e = (Σ A λ x  e  f x)  (Σ B λ y  e  g y)

⊎-lemma₂ : ∀{A B}  (s : A  B)
          (Σ A λ x  s  inl x)  (Σ B λ y  s  inr y)
⊎-lemma₂ {A} {B} s rewrite sym (⊎-lemma₀ s) = ⊎-lemma₁ inl inr s


⊎-induction : ∀{A B} {P : A  B  Set}  (∀ x  P (inl x))  (∀ y  P (inr y))
             (s : A  B)  P s
⊎-induction {A} {B} {P} pfl pfr s =
  ⊎-lemma₂ s (P s)
     sg  sg (P s)  x s≡inlx  subst P (sym s≡inlx) (pfl x)))
     sg  sg (P s)  y s≡inry  subst P (sym s≡inry) (pfr y)))




 : Set
 = (R : Set)  R  (R  R)  R

zero : 
zero R z s = z

suc :   
suc n R z s = s (n R z s)

postulate
  pm-ℕ : (A B : Set) (R : A  B) (s₀ : A  A) (s₁ : B  B) (z₀ : A) (z₁ : B) (n : )
        (∀ x₀ x₁  R x₀ x₁  R (s₀ x₀) (s₁ x₁))
        R z₀ z₁  R (n A z₀ s₀) (n B z₁ s₁)

free-ℕ : {R S : Set} (x : R) (f : R  S) (g : R  R) (h : S  S) (n : )
        (∀ x  f (g x)  h (f x))
        f (n R x g)  n S (f x) h
free-ℕ x f g h n pre = pm-ℕ _ _
                             x y  f x  y) g h x (f x) n 
                             x y pf  subst  z  f (g x)  h z) pf (pre x)) refl

ℕ-lemma₀ : (n : )  n  zero suc  n
ℕ-lemma₀ n = ext (n  zero suc)     n       λ R 
             ext (n  zero suc R)   (n R)   λ z 
             ext (n  zero suc R z) (n R z) λ s 
             free-ℕ zero  m  m R z s) suc s n  m  refl)

-- I won't argue that things defined this way are handy to work with
data _+_ (A B : Set) : Set where
  inj₁ : A  A + B
  inj₂ : B  A + B

[_^_] : ∀{A B C}  (A  C)  (B  C)  A + B  C
[ f ^ g ] (inj₁ x) = f x
[ f ^ g ] (inj₂ y) = g y

record Sg (A : Set) (T : A  Set) : Set where
  constructor _,,_
  field
    proj₁ : A
    proj₂ : T proj₁
open Sg

ℕ-lemma₁ : ∀{A : Set} z s  (n : )  (n A z s  z) + (Sg  λ m  n A z s  s (m A z s))
ℕ-lemma₁ {A} z s n = pm-ℕ A A R s s z z n
                        x y  [  y=z  inj₂ (zero ,, cong s y=z))
                                ^  pf  inj₂ (suc (proj₁ pf) ,, cong s (proj₂ pf))) ])
                       (inj₁ refl)
 where
 R : A  A  Set
 R _ e = (e  z) + (Sg  λ m  e  s (m A z s))

{-
induction : {P : ℕ → Set} → P Z → (∀ n → P n → P (S n)) → ∀ n → P n
induction {P} Pz Ps n = {!!}
-}