Propositions and Proofs

The source code for this module: PartI/Proofs.ard
The source code for the exercises: PartI/ProofsEx.ard

In this module we explain how to formulate and prove propositions in Arend. We show how to express various logical connectives and demonstrate that they satisfy the required properties.

Curry-Howard correspondence

Arend is based on a variant of Martin-Löf’s type theory. Such theories do not have a separate logical language to express propositions and their proofs. Instead, they use the Curry-Howard correspondence to encode propositions as types. The false proposition corresponds to the empty type and the true proposition corresponds to the unit type. Different elements of a type can be thought of as different ways to prove their corresponding proposition. For example, the type of natural numbers corresponds to the proposition that natural numbers exist and every element of this type witnesses a proof of this proposition.

Remark: This correspondence will be refined in Part II of this tutorial, where we will argue that not every type should be thought of as a proposition.

In order to illustrate the correspondence between the empty type Empty and the logical False, we can prove that False implies everything by constructing an element of any type from an element in Empty:

\func absurd {A : \Type} (e : Empty) : A
-- There are no patterns since Empty does not have constructors.

-- This can be expressed more explicitly by means of the absurd patterns.
-- This pattern indicates that the data type of the corresponding variable does not have constructors.
-- If such a pattern is used, the right hand side of the clause can (and should) be omitted.
\func absurd' {A : \Type} (e : Empty) : A \elim e
  | () -- absurd pattern

Of course, we can also prove that Unit corresponds to the logical True simply by constructing an element of this type:

\func Unit-isTrue : Unit => unit

To formulate more complicated propositions, we need to define various logical connectives such as conjunction &&, disjunction ||, implication ->, and negation Not. Let us begin with the implication. If P -> Q is true, then the truth of P implies the truth of Q. Thus, we can think of a proof of P -> Q as a function that transforms a proof of P into a proof of Q. That is, the type corresponding to the implications is the type of functions P -> Q!

We already can prove various propositional tautologies. For example, the identity function proves that P -> P holds for every proposition P. The constant function \lam x y => x proves P -> Q -> P. The composition function \lam g f x => g (f x) proves (Q -> S) -> (P -> Q) -> P -> S.

Exercise 1: Prove that (P -> Q -> R) -> (P -> Q) -> P -> R.

Exercise 2: Prove that ((P -> Q -> R) -> P) -> (P -> R) -> R.

Since P && Q is true if and only if P and Q are true, we can say that a proof of P && Q is just a pair consisting of a proof of P and a proof of Q. That is, the type corresponding to P && Q is simply the type of pairs:

\func \infixr 3 && (P Q : \Type) => \Sigma P Q

It is easy to prove conjunction axioms:

-- This function proves that P -> Q -> (P && Q)
\func &&-intro {P Q : \Type} (p : P) (q : Q) : \Sigma P Q => (p, q)

-- This function proves that (P && Q) -> P
\func &&-elim1 {P Q : \Type} (t : \Sigma P Q) : P => t.1

-- This function proves that (P && Q) -> Q
\func &&-elim2 {P Q : \Type} (t : \Sigma P Q) : Q => t.2

Exercise 3: Prove that ((P && Q) -> R) -> P -> Q -> R.

Exercise 4: Prove that (P -> Q -> R) -> (P && Q) -> R.

A proof of P || Q is either a proof of P or a proof of Q. The type corresponding to this principle is the sum type:

\data \infixr 2 || (P Q : \Type)
  | inl P
  | inr Q

It is easy to prove disjunction axioms:

-- This function proves that P -> (P || Q)
\func ||-intro1 {P Q : \Type} (p : P) : P || Q => inl p

-- This function proves that Q -> (P || Q)
\func ||-intro2 {P Q : \Type} (q : Q) : P || Q => inr q

-- This function proves that (P -> R) -> (Q -> R) -> (P || Q) -> R
\func ||-elim {P Q R : \Type} (l : P -> R) (r : Q -> R) (x : P || Q) : R \elim x
  | inl p => l p
  | inr q => r q

Exercise 5: Prove that (P -> R) -> (Q -> R) -> P || Q -> R.

Exercise 6: Prove that ((P || Q) -> (P && Q)) -> ((P -> Q) && (Q -> P)).

The negation Not P can be defined in terms of the implication as P -> Empty.

Remark: The logic of Arend is intuitionistic. This means that the law of excluded middle, the double negation elimination, and other classically valid principles are not provable in Arend. In particular, it is not true that the conjunction P && Q can be expressed as Not (Not P || Not Q). Similarly, the disjunction P || Q cannot be expressed as Not (Not P && Not Q) and the implication P -> Q cannot be expressed as Not P || Q.

Exercise 7: Russell’s paradox shows that there is no set of all sets. If such a set exists, then we can form the set B of sets which are not members of themselves. Then B belongs to itself if and only if it is not. This implies a contradiction. Cantor’s theorem states that there is no set X with a surjection from X onto the set of subsets of X. Its proof also constructs a proposition which is true if and only if it is false. Prove that more generally the existence of any such proposition implies a contradiction.

Finally, let us discuss quantifiers. A proof of forall (x : A). P(x) should give us a proof of P(a) for every element a : A. Thus, this proposition corresponds to the type of dependent functions \Pi (x : A) -> P x. A proof of exists (x : A). P(x) consists of an element a : A and a proof of P(a). Thus, this proposition corresponds to the type of dependent pairs \Sigma (x : A) (P x).

Exercise 8: Prove that if, for every x : Nat, P x is true, then there exists x : Nat such that P x is true.

Exercise 9: Prove that if there is no x : Nat such that P x holds, then P 3 is false.

Exercise 10: Prove that if, for every x : Nat, P x implies Q x, then the existence of an element x : Nat for which P x is true implies the existence of an element x : Nat for which Q x is true.

Exercise 11: Prove that if, for every x : Nat, either P x is false or Q x is false, then P 3 implies that Q 3 is false.

Examples of propositions and proofs

Here we will give several simple examples of propositions and proofs, using what we have discussed so far. To express various propositions, we will use the function T that interprets true : Bool as the proposition True (type Unit) and false : Bool as the proposition False (type Empty):

\func T (b : Bool) : \Type
  | true => Unit
  | false => Empty

Now let us prove some statements about the two-element type Bool defined earlier. We formulate some properties of Bool, expressable in terms of equality predicate for Bool:

\func \infix 4 == (x y : Bool) : Bool
  | true, true => true
  | false, false => true
  | _ , _ => false

For example, propositions T (x == x) and T (not (not x) == x) can be proven by case analysis:

\func not-isInvolution (x : Bool) : T (not (not x) == x)
  | true => unit -- if x is true, then T (not (not true) == true) evaluates to Unit
  | false => unit -- if x is false, then T (not (not false) == false) again evaluates to Unit

-- proof of reflexivity of == is analogous 
\func ==-refl (x : Bool) : T (x == x)
  | true => unit
  | false => unit

In both cases in both proofs we simply return unit. Note that we cannot return unit without case analysis since both T (not (not x) == x) and T (x == x) do not evalute to Unit. The following code does not typecheck:

\func not-isInvolution' (x : Bool) : T (not (not x) == x) => unit

It is not possible to prove false statements in this way:

\func not-isIdempotent (x : Bool) : T (not (not x) == not x)
  | true => {?} -- goal expression, an element of Empty is expected
  | false => {?} -- goal expression, an element of Empty is expected

-- we can prove negation of not-isIdempotent
\func not-isIdempotent' (x : Bool) : T (not (not x) == not x) -> Empty
  | true => \lam x => x -- a proof of Empty -> Empty
  | false => \lam x => x -- again a proof of Empty -> Empty

Let us also prove something involving quantification. For example, the statement “for every x : Bool there exists y : Bool such that x == y”:

-- Sigma-types are used to express existential quantification
\func lemma (x : Bool) : \Sigma (y : Bool) (T (x == y)) => (x, ==-refl x)

The following is a proof of rather awkward statement “if every x : Bool equals itself, then true : Bool equals true : Bool”:

\func higherOrderFunc (f : \Pi (x : Bool) -> T (x == x)) : T (true == true) => f true

Identity type

The way how we defined equality == for Bool above is not actually satisfactory. Its definition is specific for Bool, we need to make analogous definitions for all other types and each time prove, say, that it is an equivalence relation.

Instead, we define an identity type for all types at once. Its definition is located in Prelude (type Path and its infix form =). We will not get into details for now, all that we currently need is the proof of reflexivity idp : a = a, which is also defined in Prelude.

Now, all the equalities that we proved for == can similarly be proved for =. For example, the equality not (not x) = x:

\func not-isInvolution'' (x : Bool) : not (not x) = x
  | true => idp
  | false => idp

And as before, we cannot prove false statements:

\func not-isIdempotent'' (x : Bool) : not (not x) = not x
  | true => {?} -- goal expression, non-existing proof of true = false is expected
  | false => {?} -- goal expression, non-existing proof of false = true is expected

Exercise 12: Prove associativity of and and or.

Exercise 13: Prove that 2 * 2 equals to 4.