Last active

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist

How does local completeness generalize to eliminators?

View LocalProps.agda
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
{-
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
Something went wrong with that request. Please try again.