Martin Escardo, Chuangjie Xu, 2012.

As a simple application of coinduction and corecursion, one can show
that the the inclusion map incl : ℕ∞ → ₂ℕ is part of a retraction.

This exercise is artificial: a direct construction and proof of the
retraction would be shorter and perhaps clearer. However, it does
illustrate how co-recursion and co-induction can be used.

Recall that a retraction is a pair of maps r : X → Y and s : Y → X
such that r ∘ s : Y → Y is the identity, where r is called the
retraction and s the section. In this case, it follows that 
s ∘ r : X → X is idempotent, and s is an injection and r is a
surjection. When such maps exists one says that Y is a retract of X.

The idea of the construction of the retraction is that we "read"
digits from α until we find a zero or forever, and count how long
this took.


module CoNaturalsExercise where

open import Cantor
open import Two
open import GenericConvergentSequence
open import SetsAndFunctions
open import Naturals
open import CoNaturals
open import Equality
open import CurryHoward
open import Extensionality
open import Sequence

incl-is-a-section :  \(retr : ₂ℕ  ℕ∞)  retr  incl  id
incl-is-a-section  = ∃-intro retr (extensionality lemma)
  f-retr :   ₂ℕ   + ₂ℕ
  f-retr  α = in₀ *
  f-retr  α = in₁ α 

  p-retr : ₂ℕ   + ₂ℕ
  p-retr α = f-retr(hd α)(tl α)

  retr : ₂ℕ  ℕ∞
  retr = ℕ∞-corec p-retr

  retr-spec : P  retr  (①+ retr)  p-retr
  retr-spec = ∃-elim(homomorphism-existence p-retr)

  retr-spec₀ : ∀(α : ₂ℕ)  hd α    retr α  Zero
  retr-spec₀ α r = alg-morphism-Zero p-retr retr retr-spec α * lemma
    lemma : p-retr α  in₀ *
    lemma = cong  b  f-retr b (tl α)) r

  retr-spec₁ : ∀(α : ₂ℕ)  hd α    retr α  Succ(retr(tl α))
  retr-spec₁ α r = alg-morphism-Succ p-retr retr retr-spec α (tl α) lemma
    lemma : p-retr α  in₁(tl α)
    lemma = cong  b  f-retr b (tl α)) r

  R : ℕ∞  ℕ∞  Prp
  R u v =  \w  retr(incl w)  u  w  v 

  r :  u  R (retr(incl u)) u
  r u = (u , refl , refl)

  R-positivity :  u v  R u v  positivity u  positivity v
  R-positivity u v (w , c , d) = 
   two-equality-cases lemma₀ lemma₁ 
    lemma₀ : positivity w    positivity u  positivity v
    lemma₀ r = cong positivity claim₃
      claim₀ : retr(incl w)  Zero
      claim₀ = retr-spec₀(incl w) r
      claim₁ : v  Zero
      claim₁ = trans (sym d) (isZero-equal-Zero r)
      claim₂ : retr(incl w)  v
      claim₂ = trans claim₀ (sym claim₁)
      claim₃ : u  v
      claim₃ = trans (sym c) claim₂

    lemma₁ : positivity w    positivity u  positivity v
    lemma₁ r = trans claim₂ (sym claim₄)
      claim₀ : positivity(retr(incl w))   
      claim₀ = cong positivity (retr-spec₁(incl w) r)
      claim₁ : positivity(retr(incl w))  positivity u 
      claim₁ = cong positivity c
      claim₂ : positivity u  
      claim₂ = trans (sym claim₁) claim₀
      claim₃ : positivity w  positivity v
      claim₃ = cong positivity d
      claim₄ : positivity v  
      claim₄ = trans (sym claim₃) r

  R-Pred :  u v  R u v  R(Pred u)(Pred v)
  R-Pred u v (w , c , d) = (Pred w , lemma₀ , lemma₁)
    lemma₀ : retr(incl(Pred w))  Pred u
    lemma₀ = trans claim claim₀
     claim₀ : Pred(retr(incl w))  Pred u
     claim₀ = cong Pred c
     claim :  retr(incl(Pred w))  Pred(retr(incl w))
     claim = two-equality-cases claim₁ claim₂
       claim₁ : isZero w  retr(incl(Pred w))  Pred(retr(incl w))
       claim₁ r = Lemma[x≡z→y≡z→x≡y] c₃ c₅
         c₀ : w  Zero
         c₀ = isZero-equal-Zero r
         c₁ : Pred w  Zero
         c₁ = cong Pred c₀
         c₂ : incl (Pred w) 0  
         c₂ = cong (hd  incl) c₁
         c₃ : retr(incl (Pred w))  Zero
         c₃ = retr-spec₀(incl (Pred w)) c₂
         c₄ : retr(incl w)  Zero
         c₄ = retr-spec₀(incl w) r
         c₅ : Pred(retr(incl w))  Zero
         c₅ = cong Pred c₄
       claim₂ : positive w  retr(incl(Pred w))  Pred(retr(incl w))
       claim₂ r = Lemma[x≡z→y≡z→x≡y] c₃ c₁
         c₀ : retr(incl w)  Succ(retr(tl(incl w)))
         c₀ = retr-spec₁ (incl w) r
         c₁ : Pred(retr(incl w))  retr(tl(incl w))
         c₁ = trans (cong Pred c₀) Pred-Succ-u-is-u
         c₃ : retr(incl(Pred w))  retr(tl(incl w))
         c₃ = refl

    lemma₁ : Pred w  Pred v
    lemma₁ = cong Pred d

  R-bisimulation : ℕ∞-bisimulation R
  R-bisimulation u v r = ∧-intro (R-positivity u v r) (R-Pred u v r)

  lemma :  u  retr(incl u)  u
  lemma u = ℕ∞-coinduction R R-bisimulation (retr(incl u)) u (r u)