From 7d1ee9dd080daeeeef20ba3fbf11f404e8bb34ed Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Mon, 29 Jun 2020 20:18:40 -0500 Subject: [PATCH] Simplify Equality --- libs/base/Data/List.idr | 37 ++------ libs/base/Decidable/Equality.idr | 116 ++++++++++---------------- libs/contrib/Data/List/Equalities.idr | 6 -- 3 files changed, 51 insertions(+), 108 deletions(-) diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index 0025929b4..5b9840a30 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -1,7 +1,5 @@ module Data.List -import Decidable.Equality - public export isNil : List a -> Bool isNil [] = True @@ -597,6 +595,12 @@ export Uninhabited (Prelude.(::) x xs = []) where uninhabited Refl impossible +||| (::) is injective +export +consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} -> + x :: xs = y :: ys -> (x = y, xs = ys) +consInjective Refl = (Refl, Refl) + ||| The empty list is a right identity for append. export appendNilRightNeutral : (l : List a) -> @@ -631,32 +635,3 @@ revAppend (v :: vs) ns rewrite sym (revAppend vs ns) in rewrite appendAssociative (reverse ns) (reverse vs) [v] in Refl - -public export -lemma_val_not_nil : {x : t} -> {xs : List t} -> ((x :: xs) = Prelude.Nil {a = t} -> Void) -lemma_val_not_nil Refl impossible - -public export -lemma_x_eq_xs_neq : {x : t} -> {xs : List t} -> {y : t} -> {ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void) -lemma_x_eq_xs_neq Refl p Refl = p Refl - -public export -lemma_x_neq_xs_eq : {x : t} -> {xs : List t} -> {y : t} -> {ys : List t} -> (x = y -> Void) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> Void) -lemma_x_neq_xs_eq p Refl Refl = p Refl - -public export -lemma_x_neq_xs_neq : {x : t} -> {xs : List t} -> {y : t} -> {ys : List t} -> (x = y -> Void) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void) -lemma_x_neq_xs_neq p p' Refl = p Refl - -public export -implementation DecEq a => DecEq (List a) where - decEq [] [] = Yes Refl - decEq (x :: xs) [] = No lemma_val_not_nil - decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil) - decEq (x :: xs) (y :: ys) with (decEq x y) - decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys) - decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl - decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq) - decEq (x :: xs) (y :: ys) | No p with (decEq xs ys) - decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq) - decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq) diff --git a/libs/base/Decidable/Equality.idr b/libs/base/Decidable/Equality.idr index 137291197..9d2b67ea9 100644 --- a/libs/base/Decidable/Equality.idr +++ b/libs/base/Decidable/Equality.idr @@ -2,6 +2,7 @@ module Decidable.Equality import Data.Maybe import Data.Nat +import Data.List %default total @@ -36,34 +37,29 @@ decEqSelfIsYes {x} with (decEq x x) -------------------------------------------------------------------------------- export -implementation DecEq () where +DecEq () where decEq () () = Yes Refl -------------------------------------------------------------------------------- -- Booleans -------------------------------------------------------------------------------- -trueNotFalse : True = False -> Void -trueNotFalse Refl impossible export -implementation DecEq Bool where +DecEq Bool where decEq True True = Yes Refl decEq False False = Yes Refl - decEq True False = No trueNotFalse - decEq False True = No (negEqSym trueNotFalse) + decEq False True = No absurd + decEq True False = No absurd -------------------------------------------------------------------------------- -- Nat -------------------------------------------------------------------------------- -ZnotS : Z = S n -> Void -ZnotS Refl impossible - export -implementation DecEq Nat where +DecEq Nat where decEq Z Z = Yes Refl - decEq Z (S _) = No ZnotS - decEq (S _) Z = No (negEqSym ZnotS) + decEq Z (S _) = No absurd + decEq (S _) Z = No absurd decEq (S n) (S m) with (decEq n m) decEq (S n) (S m) | Yes p = Yes $ cong S p decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h @@ -72,18 +68,49 @@ implementation DecEq Nat where -- Maybe -------------------------------------------------------------------------------- -nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void -nothingNotJust Refl impossible - export -implementation (DecEq t) => DecEq (Maybe t) where +DecEq t => DecEq (Maybe t) where decEq Nothing Nothing = Yes Refl + decEq Nothing (Just _) = No absurd + decEq (Just _) Nothing = No absurd decEq (Just x') (Just y') with (decEq x' y') decEq (Just x') (Just y') | Yes p = Yes $ cong Just p decEq (Just x') (Just y') | No p = No $ \h : Just x' = Just y' => p $ justInjective h - decEq Nothing (Just _) = No nothingNotJust - decEq (Just _) Nothing = No (negEqSym nothingNotJust) + +-------------------------------------------------------------------------------- +-- Tuple +-------------------------------------------------------------------------------- + +pairInjective : (a, b) = (c, d) -> (a = c, b = d) +pairInjective Refl = (Refl, Refl) + +export +(DecEq a, DecEq b) => DecEq (a, b) where + decEq (a, b) (a', b') with (decEq a a') + decEq (a, b) (a', b') | (No contra) = + No $ contra . fst . pairInjective + decEq (a, b) (a, b') | (Yes Refl) with (decEq b b') + decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl + decEq (a, b) (a, b') | (Yes Refl) | (No contra) = + No $ contra . snd . pairInjective + +-------------------------------------------------------------------------------- +-- List +-------------------------------------------------------------------------------- + +export +DecEq a => DecEq (List a) where + decEq [] [] = Yes Refl + decEq (x :: xs) [] = No absurd + decEq [] (x :: xs) = No absurd + decEq (x :: xs) (y :: ys) with (decEq x y) + decEq (x :: xs) (y :: ys) | No contra = + No $ contra . fst . consInjective + decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys) + decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl + decEq (x :: xs) (x :: ys) | (Yes Refl) | (No contra) = + No $ contra . snd . consInjective -- TODO: Other prelude data types @@ -93,59 +120,6 @@ implementation (DecEq t) => DecEq (Maybe t) where -- A postulate would be better, but erasure analysis may think they're needed -- for computation in a higher order setting. --------------------------------------------------------------------------------- --- Tuple --------------------------------------------------------------------------------- - -lemma_both_neq : (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void) -lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl - -lemma_snd_neq : (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void) -lemma_snd_neq Refl p Refl = p Refl - -lemma_fst_neq_snd_eq : (x = x' -> Void) -> - (y = y') -> - ((x, y) = (x', y) -> Void) -lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl - -export -implementation (DecEq a, DecEq b) => DecEq (a, b) where - decEq (a, b) (a', b') with (decEq a a') - decEq (a, b) (a, b') | (Yes Refl) with (decEq b b') - decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl - decEq (a, b) (a, b') | (Yes Refl) | (No p) = No (\eq => lemma_snd_neq Refl p eq) - decEq (a, b) (a', b') | (No p) with (decEq b b') - decEq (a, b) (a', b) | (No p) | (Yes Refl) = No (\eq => lemma_fst_neq_snd_eq p Refl eq) - decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq) - --------------------------------------------------------------------------------- --- List --------------------------------------------------------------------------------- - -lemma_val_not_nil : (the (List _) (x :: xs) = Prelude.Nil {a = t} -> Void) -lemma_val_not_nil Refl impossible - -lemma_x_eq_xs_neq : (x = y) -> (xs = ys -> Void) -> (the (List _) (x :: xs) = (y :: ys) -> Void) -lemma_x_eq_xs_neq Refl p Refl = p Refl - -lemma_x_neq_xs_eq : (x = y -> Void) -> (xs = ys) -> (the (List _) (x :: xs) = (y :: ys) -> Void) -lemma_x_neq_xs_eq p Refl Refl = p Refl - -lemma_x_neq_xs_neq : (x = y -> Void) -> (xs = ys -> Void) -> (the (List _) (x :: xs) = (y :: ys) -> Void) -lemma_x_neq_xs_neq p p' Refl = p Refl - -implementation DecEq a => DecEq (List a) where - decEq [] [] = Yes Refl - decEq (x :: xs) [] = No lemma_val_not_nil - decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil) - decEq (x :: xs) (y :: ys) with (decEq x y) - decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys) - decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl - decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq) - decEq (x :: xs) (y :: ys) | No p with (decEq xs ys) - decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq) - decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq) - -------------------------------------------------------------------------------- -- Int diff --git a/libs/contrib/Data/List/Equalities.idr b/libs/contrib/Data/List/Equalities.idr index 31eb62579..4a8d196cd 100644 --- a/libs/contrib/Data/List/Equalities.idr +++ b/libs/contrib/Data/List/Equalities.idr @@ -16,12 +16,6 @@ SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (xs `snoc` x) SnocNonEmpty [] _ = IsNonEmpty SnocNonEmpty (_::_) _ = IsNonEmpty -||| (::) is injective -export -consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} -> - (x :: xs) = (y :: ys) -> (x = y, xs = ys) -consInjective Refl = (Refl, Refl) - ||| Two lists are equal, if their heads are equal and their tails are equal. export consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->