Skip to content

@larrytheliquid /LocalProps.agda
Last active

Embed URL


Subversion checkout URL

You can clone with
Download ZIP
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
Something went wrong with that request. Please try again.