RefinementProofs

This library allows for stronger and more refined types in Elm for both library writer and end users.

Definition

type Proven a p

A value "a" that is proven to hold the property "b"

Logic operator types

type And p1 p2

Both "p1" and "p2" holds

type Or p1 p2

"p1" or "p2" holds

type Not p

A negation of a proof

type alias XOr p1 p2 =

Or (And p1 (Not p2)) (And (Not p1) p2)

Exlusive or

type Implies p1 p2

Implies that if "p1" holds than "p2" holds

Basic function

axiom : p -> a -> Proven a p

Used by library writers to create axioms with non-exported constructors. Remember, the library/module constructors must not be exported!

or : p1 -> p2 -> Or p1 p2

Used by library writers to create build a Or proof

and : p1 -> p2 -> And p1 p2

Used by library writers to create build a And proof

not : p1 -> Not p1

Used by library writers to create build a Not proof

Logic operators

introOrR : Proven a p1 -> Proven a (Or p1 p2)

If a is proven to hold property p1 then classic logic gives that a holds either p1 or p2

introOrL : Proven a p1 -> Proven a (Or p2 p1)

Same as introOrR but introduces the p2 on the other side

makeOr :

(a -> Maybe (Proven a b))

-> (a -> Maybe (Proven a c))

-> a

-> Maybe (Proven a (Or b c))

A convience method to check two proofs for Or

makeAnd :

(a -> Maybe (Proven a b))

-> (a -> Maybe (Proven a c))

-> a

-> Maybe (Proven a (And b c))

A convience method to check two proofs at once for And

inverse : p1 -> (a -> Maybe (Proven a p1)) -> a -> Maybe (Proven a (Not p1))

Used by library writers to show that when p1 does not hold for a then Not p1 holds.

elimAndL : Proven a (And b c) -> Proven a b

Remove the left hand side of an And proof

elimAndR : Proven a (And b c) -> Proven a c

Remove the right hand side of an And proof

exorcise : Proven a b -> a

Extract the actual value and remove the proof. This is always safe and a library writer should always expect and allow its users to do this.

modusPonens : Implies p1 p2 -> Proven a p1 -> Proven a p2

If a library implies that when p1 holds the p2 holds then you have proven p2 by prove p1

since : Implies p1 p2 -> Proven a p1 -> Proven a p2

Synonym for "modus ponens". If a library implies that when p1 holds the p2 holds then you have proven p2 by prove p1

modusTollens : Implies p1 p2 -> Proven a (Not p1) -> Proven a (Not p2)

If a library implies that when p1 holds the p2 holds then you have proven (Not p2) by prove (Not p1)

sinceNot : Implies p1 p2 -> Proven a (Not p1) -> Proven a (Not p2)

Synonym for "modus tollens". If a library implies that when p1 holds the p2 holds then you have proven (Not p2) by prove (Not p1)

imply : p1 -> p2 -> Implies p1 p2

Used by library writers to imply proof relations

absurd : a

Used by library writers to carefully ignore "impossible" states. Note use this with extreme care since this will cause a runtime exception if ever evaluated! Remember that Elm is an eager language and not lazy.

mtonnberg/refinement-proofs/2.0.0

RefinementProofs

Definition

Logic operator types

Basic function

Logic operators

Modules