@@ -12,6 +12,7 @@ import Prelude.Maybe
1212-- Utility lemmas
1313--------------------------------------------------------------------------------
1414
15+||| The negation of equality is symmetric (follows from symmetry of equality)
1516total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
1617negEqSym p h = p (sym h)
1718
@@ -20,7 +21,9 @@ negEqSym p h = p (sym h)
2021-- Decidable equality
2122--------------------------------------------------------------------------------
2223
24+||| Decision procedures for propositional equality
2325class DecEq t where
26+ ||| Decide whether two elements of `t` are propositionally equal
2427 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
2528
2629--------------------------------------------------------------------------------
@@ -33,7 +36,6 @@ instance DecEq () where
3336--------------------------------------------------------------------------------
3437-- Booleans
3538--------------------------------------------------------------------------------
36−
3739total trueNotFalse : True = False -> _|_
3840trueNotFalse refl impossible
3941
@@ -122,13 +124,13 @@ lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
122124lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
123125
124126instance (DecEq a, DecEq b) => DecEq (a, b) where
125− decEq (a, b) (a', b') with (decEq a a')
126− decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
127− decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
128− decEq (a, b) (a, b') | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)
129− decEq (a, b) (a', b') | (No p) with (decEq b b')
130− decEq (a, b) (a', b) | (No p) | (Yes refl) = No (\eq => lemma_fst_neq_snd_eq p refl eq)
131− decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
127+ decEq (a, b) (a', b') with (decEq a a')
128+ decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
129+ decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
130+ decEq (a, b) (a, b') | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)
131+ decEq (a, b) (a', b') | (No p) with (decEq b b')
132+ decEq (a, b) (a', b) | (No p) | (Yes refl) = No (\eq => lemma_fst_neq_snd_eq p refl eq)
133+ decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
132134
133135
134136--------------------------------------------------------------------------------