Instantly share code, notes, and snippets.

larrytheliquid/LocalProps.agda Last active Dec 15, 2015

What would you like to do?
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
Owner