[Agda] A different implementation of --without-K

[Jesper Cockx]

I skipped some code in my previous mail, here is the complete version for
those who are interested:

{-# OPTIONS --without-K --new-without-K #-}
-- Both flags are enabled for extra safety

module FinWithoutK where

open import Data.Empty
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

J : {A : Set} {x : A} (P : (y : A) → x ≡ y → Set) →
    P x refl → {y : A} → (q : x ≡ y) → P y q
J P p refl = p

K : {A : Set} (x : A) → Set₁
K {A} x = (P : x ≡ x → Set) → P refl → (q : x ≡ x) → P q

proof-irrelevance : {A : Set} {x y : A} {e₀ : x ≡ y} → {{k : K x}} →
                    (P : x ≡ y → Set) → P e₀ → (e : x ≡ y) → P e
proof-irrelevance {e₀ = refl} {{k}} P p e = k P p e

add-suc : {m n : ℕ} → m ≡ n → suc m ≡ suc n
add-suc refl = refl

drop-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
drop-suc refl = refl

add-drop-lemma : {m n : ℕ} (q : suc m ≡ suc n) → add-suc (drop-suc q) ≡ q
add-drop-lemma refl = refl

K-for-ℕ : {n : ℕ} → (P : n ≡ n → Set) → P refl → (q : n ≡ n) → P q
K-for-ℕ {zero} P p refl = p
K-for-ℕ {suc n} P p q = J (λ q _ → P q) aux (add-drop-lemma q)
  where
    aux : P (add-suc (drop-suc q))
    aux = K-for-ℕ {n} (λ q → P (add-suc q)) p (drop-suc q)

data Fin : ℕ → Set where
  fz : {n : ℕ} → Fin (suc n)
  fs : {n : ℕ} → Fin n → Fin (suc n)

NoConfusion : {n : ℕ} (x : Fin n) {m : ℕ} (y : Fin m) → Set
NoConfusion (fz {n})   (fz {m})   = n ≡ m
NoConfusion fz         (fs y)     = ⊥
NoConfusion (fs x)     fz         = ⊥
NoConfusion (fs {n} x) (fs {m} y) = Σ[ e ∈ n ≡ m ] subst Fin e x ≡ y

noConfusion : {n : ℕ} {x : Fin n} {m : ℕ} {y : Fin m} →
              (e : n ≡ m) → subst Fin e x ≡ y →
              NoConfusion x y
noConfusion {x = fz}   refl refl = refl
noConfusion {x = fs x} refl refl = refl , refl

drop-fs : ∀ {o} (x y : Fin o) → fs x ≡ fs y → x ≡ y
drop-fs x y q = proof-irrelevance {e₀ = e} (λ p → subst Fin p x ≡ y) x'≡y
refl
  where
    e = proj₁ (noConfusion refl q)
    x'≡y = proj₂ (noConfusion refl q)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131122/11c4037b/attachment.html