Create a gist now

Instantly share code, notes, and snippets.

How does local completeness generalize to eliminators?
How does local completeness ( 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.
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