larrytheliquid

{-
How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) generalize to eliminators?

Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.

Caveats:
1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
-}

larrytheliquid

open import Data.Bool
open import Data.Nat
module HypotheticalFunMatching where

{-
Imagine that the expressions in the pattern positions are first evaluated to values/neutrals.
So for example, "not" really becomes elimBool and "_+_" becomes two nested elimℕ's.

A wildcard match is always necessary because there are infinitely many intentionally different
functions.

larrytheliquid

λ A m n →
  ind
  (`Arg (Tag ("nil" ∷ "cons" ∷ []))
   (λ t →
      case
      (λ _ →
         Desc
         (μ
          (`Arg (Tag ("zero" ∷ "suc" ∷ []))
           (λ t₁ → case (λ _ → Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))

larrytheliquid

open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
  renaming ( _≟_ to _≟B_ )
open import Data.Nat using ( ℕ ; zero ; suc )
    renaming ( _≟_ to _≟ℕ_ )
open import Data.Product using ( Σ ; _,_ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

larrytheliquid

{-# OPTIONS --copatterns #-}
module CoList where

{- High-level intuition:

codata CoList (A : Set) : Set where
  nil : CoList A
  cons : A → CoList A → CoList A

append : ∀{A} → CoList A → CoList A → CoList A

larrytheliquid

open import Data.Unit
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) (O : I → Set) : Set₁ where
  `ι : (i : I) (o : O i) → Desc I O
  `δ : (A : Set) (i : A → I) (D : (o : (a : A) → O (i a)) → Desc I O) → Desc I O
  `σ : (A : Set) (D : A → Desc I O) → Desc I O

larrytheliquid

open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where

{-
This odd approach gives you 2 choices when defining an indexed type:
1. Use a McBride-Dagand encoding so your datatype 
   "need not store its indices".

larrytheliquid

open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) : Set₁ where
  `ι : I → Desc I

larrytheliquid

open import Data.Nat
open import Data.Fin renaming ( zero to here ; suc to there )
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where

mutual
 data Vec₁ (A : Set) : ℕ → Set where
   nil₁ : Vec₁ A zero
   cons₁ : {n : ℕ} → A → (xs : Vec₁ A n) → toℕ (Vec₂ xs) ≡ n → Vec₁ A (suc n)

larrytheliquid

open import Data.Nat
open import Data.Product
open import Data.String
open import Relation.Binary.PropositionalEquality
module _ where

mutual
  data Vec₁ (A : Set) : Set where
    nil : Vec₁ A
    cons : (n : ℕ) → A → (xs : Vec₁ A) → Vec₂ xs ≡ n → Vec₁ A