Even and Odd data types

Definition of the mutually recursive data types Even and Odd.

module even-odd where

open import map
open import phantomNat using (phantomZero[] ; phantomSuc[_] ; ⊢phantomZero ; ⊢phantomSuc)
open import Data.List using (_∷_ ; [] ; [_] )
open import Data.Vec renaming (_∷_ to _¦_ ; [] to [||] ; [_] to [|_|])
open import Data.Unit renaming (tt to ∗)
open import Data.Product using (_,_)

α β : mix-var
α = tvar 
β = tvar 

Γα Γβ : context {mix-var}
Γα = ⟦ [| α |] ⟧
Γβ = ⟦ [| β |] ⟧

We define now the data types Even and Odd as they usually appear in the literature. Even has two constructors, one proving that phantomZero is even, and one producing a proof that phantomSuc n is even from a proof that n is odd. Odd has a unique constructor producing a proof that phantomSuc n is odd from a proof that n is even.

Even-id Odd-id : id-TC-var
Even-id = 
Odd-id = 

Even-name Odd-name : TC-var 
Even-name = TC Even-id 
Odd-name = TC Odd-id 

even-zero-id even-suc-id odd-suc-id : id-data-constructor
even-zero-id = 
even-suc-id = 
odd-suc-id = 

even-zero even-suc odd-suc : data-constructor 
even-zero = even-zero-id ∷ [] ⇒ᵀ [| phantomZero[] |]
even-suc = even-suc-id ∷ [ appᵀ Odd-name [ [| varᵀ α |] ] ] ⇒ᵀ [| phantomSuc[ varᵀ α ] |]
odd-suc = odd-suc-id ∷ [ appᵀ Even-name [ [| varᵀ β |] ] ] ⇒ᵀ [| phantomSuc[ varᵀ β ] |]

Even Odd : user-defined 
Even = dataᵀ Even-name whereᵀ (even-zero ∷ even-suc ∷ [])
Odd = dataᵀ Odd-name whereᵀ [ odd-suc ]

Even[_] = λ n → data-typeᵀ Even [ [| n |] ]
Odd[_] = λ n → data-typeᵀ Odd [ [| n |] ]
even-zero[] = dc even-zero [||]
even-suc[_] = λ x → dc even-suc [| x |]
odd-suc[_] = λ x → dc odd-suc [| x |]

Here are the justifications for Odd and Even. Notice the need for Odd-name in the TC context of the justification of even-suc, and, conversely, the need for Even-name in the TC context of the justification of odd-suc. This is where the mutual recursive definition manifests.

⊢even-zero : ∅ ∥ ∅ ⊢ᶜ even-zero
⊢even-zero = dcᵀ-intro {G = Even-name} ∗ (⊢phantomZero , ∗)

⊢even-suc : Γα ∥ (∅ , (_ , Odd-name)) ⊢ᶜ even-suc
⊢even-suc = dcᵀ-intro {G = Even-name} (app-intro (var-intro ∋-last , ∗) (∋-rec ∋-last) , ∗) (⊢phantomSuc (var-intro ∋-last , ∗) , ∗)

⊢odd-suc : Γβ ∥ (∅ , (_ , Even-name)) ⊢ᶜ odd-suc
⊢odd-suc = dcᵀ-intro {G = Odd-name} ((app-intro (var-intro ∋-last , ∗) (∋-rec ∋-last) , ∗)) (⊢phantomSuc (var-intro ∋-last , ∗)  , ∗)
 
⊢Even : ∀ {Γ χ φ} → _ → Γ ∥ χ ⊢ Even[ φ ]
⊢Even ⊢φ =
  data-intro {Γcs = ∅ ∷ Γα ∷ []} {χcs = ∅ ∷ (∅ , (_ , Odd-name)) ∷ []}
  (⊢even-zero , ⊢even-suc , ∗) (⊢φ , ∗)

⊢Odd : ∀ {Γ χ φ} → _ → Γ ∥ χ ⊢ Odd[ φ ]
⊢Odd ⊢φ =
  data-intro {Γcs = Γβ ∷ []} {χcs = (∅ , (_ , Even-name)) ∷ []}
  (⊢odd-suc , ∗) (⊢φ , ∗)

By comparison with calls to adm on terms of non-mutually-recursive data types, a call to adm on a term in Even or in Odd will need to carry a non-empty stack of already-encountered data types. Indeed, if the call is made with an empty stack on a term of the form even-suc p, the algorithm will fail to recognize Odd at the known data type when examining the type of p. For that reason, we define the following ready-to-use stack:

Even∷Odd∷[] =
  (
    arity _
    def Even
    ctx (∅ ∷ Γα ∷ []) ∥ (∅ ∷ (∅ , (_ , Odd-name)) ∷ [])
    der (⊢even-zero , ⊢even-suc , ∗)
  ) ∷ (
    arity _
    def Odd
    ctx (Γβ ∷ []) ∥ ((∅ , (_ , Even-name)) ∷ [])
    der (⊢odd-suc , ∗)
  ) ∷ []