0 | module Decidable.Equality.Core
 1 |
 2 | import Control.Function
 3 | import Data.Maybe
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------------------------------------
 8 | -- Decidable equality
 9 | --------------------------------------------------------------------------------
10 |
11 | ||| Decision procedures for propositional equality
12 | public export
13 | interface DecEq t where
14 |   ||| Decide whether two elements of `t` are propositionally equal
15 |   decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
16 |
17 | %inline
18 | public export
19 | maybeEq : DecEq t => (x1, x2 : t) -> Maybe (x1 = x2)
20 | maybeEq x1 x2 = decToMaybe (decEq x1 x2)
21 |
22 | --------------------------------------------------------------------------------
23 | -- Utility lemmas
24 | --------------------------------------------------------------------------------
25 |
26 | ||| The negation of equality is symmetric (follows from symmetry of equality)
27 | export
28 | negEqSym : Not (a = b) -> Not (b = a)
29 | negEqSym p h = p (sym h)
30 |
31 | ||| Everything is decidably equal to itself
32 | export
33 | decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
34 | decEqSelfIsYes with (decEq x x)
35 |   decEqSelfIsYes | Yes Refl = Refl
36 |   decEqSelfIsYes | No contra = absurd $ contra Refl
37 |
38 | ||| If you have a proof of inequality, you're sure that `decEq` would give a `No`.
39 | export
40 | decEqContraIsNo : DecEq a => {x, y : a} -> Not (x = y) -> (p ** decEq x y = No p)
41 | decEqContraIsNo uxy with (decEq x y)
42 |   decEqContraIsNo uxy | Yes xy = absurd $ uxy xy
43 |   decEqContraIsNo _   | No uxy = (uxy ** Refl)
44 |
45 | public export
46 | decEqCong : (0 _ : Injective f) => Dec (x = y) -> Dec (f x = f y)
47 | decEqCong $ Yes prf   = Yes $ cong f prf
48 | decEqCong $ No contra = No $ \c => contra $ inj f c
49 |
50 | public export
51 | decEqInj : (0 _ : Injective f) => Dec (f x = f y) -> Dec (x = y)
52 | decEqInj $ Yes prf   = Yes $ inj f prf
53 | decEqInj $ No contra = No $ \c => contra $ cong f c
54 |
55 | public export
56 | decEqCong2 : (0 _ : Biinjective f) => Dec (x = y) -> Lazy (Dec (v = w)) -> Dec (f x v = f y w)
57 | decEqCong2 (Yes Refl)  s = decEqCong s @{FromBiinjectiveL}
58 | decEqCong2 (No contra) _ = No $ \c => let (Refl, Refl) = biinj f c in contra Refl
59 |