Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid
Last active December 15, 2015 03:09
Show Gist options
  • Save larrytheliquid/5192580 to your computer and use it in GitHub Desktop.
Save larrytheliquid/5192580 to your computer and use it in GitHub Desktop.
How does local completeness generalize to eliminators?
{-
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.
-}
open import Data.Nat
open import Relation.Binary.PropositionalEquality
module LocalProps where
caseℕ : ∀{ℓ} (P : ℕ → Set ℓ)
(pz : P zero)
(ps : (n : ℕ) {- → P n -} → P (suc n))
→ (n : ℕ) → P n
caseℕ P pz ps zero = pz
caseℕ P pz ps (suc n) = ps n {- (caseℕ P pz ps n) -}
completeness : (n : ℕ) → caseℕ (λ m → ℕ) zero (λ m → suc m) n ≡ n
completeness zero = refl
completeness (suc n) = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment