@@ -12,6 +12,7 @@ import Prelude.Maybe
12-- Utility lemmas
12-- Utility lemmas
13--------------------------------------------------------------------------------
13--------------------------------------------------------------------------------
15+||| The negation of equality is symmetric (follows from symmetry of equality)
15total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
16total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)
16negEqSym p h = p (sym h)
17negEqSym p h = p (sym h)
@@ -20,7 +21,9 @@ negEqSym p h = p (sym h)
20-- Decidable equality
21-- Decidable equality
21--------------------------------------------------------------------------------
22--------------------------------------------------------------------------------
24+||| Decision procedures for propositional equality
23class DecEq t where
25class DecEq t where
26+ ||| Decide whether two elements of `t` are propositionally equal
24 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
27 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
26--------------------------------------------------------------------------------
29--------------------------------------------------------------------------------
@@ -33,7 +36,6 @@ instance DecEq () where
33--------------------------------------------------------------------------------
36--------------------------------------------------------------------------------
34-- Booleans
37-- Booleans
35--------------------------------------------------------------------------------
38--------------------------------------------------------------------------------
37total trueNotFalse : True = False -> _|_
39total trueNotFalse : True = False -> _|_
38trueNotFalse refl impossible
40trueNotFalse refl impossible
@@ -122,13 +124,13 @@ lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
122lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
124lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
124instance (DecEq a, DecEq b) => DecEq (a, b) where
126instance (DecEq a, DecEq b) => DecEq (a, b) where
125− decEq (a, b) (a', b') with (decEq a a')
127+ decEq (a, b) (a', b') with (decEq a a')
126− decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
128+ decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
127− decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
129+ 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)
130+ 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')
131+ 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)
132+ 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)
133+ decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
134--------------------------------------------------------------------------------
136--------------------------------------------------------------------------------