on package:gdp

Apply an implication to a predicate in the implicit context. The (a ~~ n) parameter is not actually used; it's type is used to help select a specific fact from the context. @ -- A safe head function, using an implicitly-passed safety proof. head :: Fact (IsCons xs) => ([a] ~~ xs) -> a head xs = Prelude.head (the xs)

• - Reverse, and a lemma. reverse :: ([a] ~~ xs) -> ([a] ~~ Reverse xs) revConsLemma :: Proof (IsCons xs) -> Proof (IsCons (Reverse xs))
• - Implement a safe last function. last :: Fact (IsCons xs) => ([a] ~~ xs) -> a last xs = note (revConsLemma on xs) $ head (reverse xs)

Extract the ghost proof from a value.

Proof by contradiction: this proof technique allows you to prove P by showing that, from "Not P", you can prove a falsehood. Proof by contradiction is not a theorem of constructive logic, so it requires the Classical constraint. But note that the similar technique of proof by contrapositive (not-introduction) is valid in constructive logic! For comparison, the two types are:

contradiction  :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p
introNot       ::              (Proof      p  -> Proof FALSE) -> Proof (Not p)

The derivation of proof by contradiction from the law of the excluded middle goes like this: first, use the law of the excluded middle to prove p || Not p. Then use or-elimination to prove p for each alternative. The first alternative is immediate; for the second alternative, use the provided implication to get a proof of falsehood, from which the desired conclusion is derived.

contradiction impl = elimOr id (absurd . impl) lem

Prove a contradiction from P and "not P".

contradicts' is contradicts with the arguments flipped. It is useful when you want to partially apply contradicts to a negation.

contrapositive is an alias for introNot, with a somewhat more suggestive name. Not-introduction corresponds to the proof technique "proof by contrapositive".

Prove "not P" by demonstrating that, from the assumption P, you can derive a false conclusion.

modusPonens is just elimImpl with the arguments flipped. In this form, it is useful for partially applying an implication.

The Law of Noncontradiction: for any proposition P, "P and not-P" is false.

Apply a derivation to the right side of a conjunction.

Apply a derivation to the right side of a disjunction.

A name for referring to the result of a cons operation.

Construct a list from an element and another list.

Axiom: The result of cons x y satisfies IsCons.

Axiom: The head of cons x y is x.

Induction principle: If a predicate P is true for the empty list, and P is true for a list whenever it is true for the tail of the list, then P is true.

Axiom: The tail of cons x y is y.