Commit 91879f03 authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent ef9b7f72
> module Fun.Operations
> %default total
> %access public export
> %auto_implicits on
> |||
> pair : (a -> b, a -> c) -> a -> (b, c)
> pair (f, g) x = (f x, g x)
> |||
> cross : (a -> c) -> (b -> d) -> (a, b) -> (c, d)
> cross f g (x, y) = (f x, g y)
> |||
> modifyFun : {a : Type} -> {b : Type} -> (Eq a) =>
> (a -> b) -> a -> b -> (a -> b)
> modifyFun f a b a' = if a' == a then b else f a'
> module Fun.Properties
> import Syntax.PreorderReasoning
> import Fun.Operations
> import Fun.Predicates
> import Pair.Properties
> import Finite.Predicates
> %default total
> %access public export
> %auto_implicits on
Lambda conversions
> etaLemma : {A, B : Type} -> (f : A -> B) -> (\ a => f a) = f
> etaLemma f = Refl
Functionality, injectivity, surjectivity, etc.
> ||| Functionality of dependent functions
> functionality : {A : Type} -> {B : A -> Type} ->
> {f : (a : A) -> B a} -> {g : (a : A) -> B a} ->
> f = g -> (a : A) -> f a = g a
> functionality Refl x = Refl
> ||| Injectivity (one direction)
> Injective1 : {A, B : Type} -> (f : A -> B) -> Type
> Injective1 {A} f = (a1 : A) -> (a2 : A) -> f a1 = f a2 -> a1 = a2
> ||| Injectivity (the other direction)
> Injective2 : {A, B : Type} -> (f : A -> B) -> Type
> Injective2 {A} f = (a1 : A) -> (a2 : A) -> Not (a1 = a2) -> Not (f a1 = f a2)
> ||| Non injectivity, constructive
> NonInjective : {A, B : Type} -> (f : A -> B) -> Type
> NonInjective f = Exists (\ a1 => Exists (\ a2 => (Not (a1 = a2) , f a1 = f a2)))
> ||| Surjectivity
> Surjective : {A, B : Type} -> (f : A -> B) -> Type
> Surjective {B} f = (b : B) -> Exists (\ a => f a = b)
> ||| Non surjectivity, constructive
> NonSurjective : {A, B : Type} -> (f : A -> B) -> Type
> NonSurjective {A} f = Exists (\ b => (a : A) -> Not (f a = b))
Relationships of injectivity notions
> ||| Injective1 implies Injective2
> injectiveLemma : {A, B : Type} -> (f : A -> B) -> Injective1 f -> Injective2 f
> injectiveLemma f i1f a1 a2 contra = contra . (i1f a1 a2)
> %freeze injectiveLemma -- frozen
Properties of constructive proofs
> ||| NonInjective => Not Injective
> nonInjectiveNotInjective : {A, B : Type} -> (f : A -> B) -> NonInjective f -> Not (Injective1 f)
> nonInjectiveNotInjective f (Evidence a1 (Evidence a2 (na1eqa2 , fa1eqfa2))) =
> \ injectivef => na1eqa2 (injectivef a1 a2 fa1eqfa2)
> %freeze nonInjectiveNotInjective -- frozen
> ||| NonSurjective => Not Surjective
> nonSurjectiveNotSurjective : {A, B : Type} -> (f : A -> B) -> NonSurjective f -> Not (Surjective f)
> nonSurjectiveNotSurjective f (Evidence b faanfab) =
> \ surjectivef => let a = (getWitness (surjectivef b)) in (faanfab a) (getProof (surjectivef b))
> %freeze nonSurjectiveNotSurjective -- frozen
Properties of cross
> |||
> crossAnyIdFstLemma : fst ((cross f Prelude.Basics.id) (a,b)) = f a
> crossAnyIdFstLemma {a} {b} {f} = Refl
> |||
> crossAnyIdFstLemma' : fst ((cross f Prelude.Basics.id) ab) = f (fst ab)
> crossAnyIdFstLemma' {ab} {f} =
> ( fst ((cross f Prelude.Basics.id) ab) )
> ={ cong {f = \ ZUZU => fst ((cross f Prelude.Basics.id) ZUZU)} (pairLemma ab) }=
> ( fst ((cross f Prelude.Basics.id) (fst ab, snd ab)) )
> ={ Refl }=
> ( fst (f (fst ab), id (snd ab)) )
> ={ Refl }=
> ( f (fst ab) )
> QED
> |||
> crossAnyIdSndLemma : snd ((cross f Prelude.Basics.id) (a,b)) = b
> crossAnyIdSndLemma {a} {b} {f} = Refl
> |||
> crossAnyIdSndLemma' : snd ((cross f Prelude.Basics.id) ab) = snd ab
> crossAnyIdSndLemma' {ab} {f} =
> ( snd ((cross f Prelude.Basics.id) ab) )
> ={ cong {f = \ ZUZU => snd ((cross f Prelude.Basics.id) ZUZU)} (pairLemma ab) }=
> ( snd ((cross f Prelude.Basics.id) (fst ab, snd ab)) )
> ={ Refl }=
> ( snd (f (fst ab), id (snd ab)) )
> ={ Refl }=
> ( snd (f (fst ab), snd ab) )
> ={ Refl }=
> ( snd ab )
> QED
> |||
> crossIdAnyFstLemma : fst ((cross Prelude.Basics.id f) (a,b)) = a
> crossIdAnyFstLemma {a} {b} {f} = Refl
* Properties of extensional equality
> eqImpliesExtEq : {A, B : Type} -> (f, g : A -> B) ->
> f = g -> ExtEq f g
> eqImpliesExtEq f f Refl = \ x => Refl
> {-
> finiteDecidableExtEq : {A, B : Type} ->
> (f : A -> B) -> (g : A -> B) ->
> Finite A -> DecEq B -> Dec (ExtEq f g)
> -}
> {-
> ---}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment