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