idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-01 16:12:26 +03:00
Code Issues Projects Releases Wiki Activity

Simplify Equality

Browse Source
This commit is contained in:
Nick Drozd 2020-06-29 20:18:40 -05:00 committed by G. Allais
parent 48fe4382eb
commit 7d1ee9dd08
3 changed files with 51 additions and 108 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
libs/base/Data/List.idr
View File

@ -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)

116
libs/base/Decidable/Equality.idr
View File

@ -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

6
libs/contrib/Data/List/Equalities.idr
View File

@ -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} ->