public
Last active

How does local completeness generalize to eliminators?

  • Download Gist
LocalProps.agda
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

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.