Pages

Saturday, February 21, 2015

Learning set theory through Coq (part 3)

This post covers through page 34 (through definition 2.8).

Relations

A binary relation describes a property that pairs of elements could possess. In set theory the binary relation is expressed as a set of ordered pairs. If the pair meets the criteria defined by the relation, it is in the set. For example, this relation describes pairs of natural numbers where the pair adds up to 10: $\{(n,m) \in \mathbb{N \times N} : n + m = 10 \}$. The advantage of defining a relation this way is that all of the usual set operators, such as $\cup$, work well between relations.

Relations in Coq are a mess. There are 4 different names for binary homogeneous relations in different modules. A binary homogeneous relation takes exactly 2 operands (similar to an ordered pair), and each of those operands have the same type. There is a fifth relation-like type in Coq, predicate, which supports an arbitrary number of operands, and they can be heterogeneous. The problem with predicate is that almost none of the functions in the module can use it. Furthermore the convenience notations to define a specific predicate are locally defined in Coq.Classes.RelationClasses; they are not available outside of the module.

TypeNameModule
binary homogeneous relationRelation Coq.Sets.Relations_1
binary homogeneous relationRel Coq.Sets.Partial_Order
binary homogeneous relationrelation Coq.Relations.Relation_Definitions
binary homogeneous relationbinary_relation Coq.Classes.RelationClasses
heterogenous relationpredicate Coq.Classes.RelationClasses


Similar to Ensemble, relations in Coq are functions that return a Prop, and that Prop describes whether the pair meets the criteria of the relation. The problem is that the relation is not defined as an Ensemble of a pair. Instead it is a function that takes takes two arguments, that is, forall T : Type, T -> T -> Prop. Describing that with Ensemble, the definition becomes T -> Ensemble(T), that is a function that returns an ensemble. Note this is not implicitly convertible with either Ensemble (T * T) (ensemble of a pairs) or Ensemble (T -> T) (ensemble of functions that take a T and return a T). Translating that function-style representation back to set theory, the previous example of pairs of numbers that add to 10 would look like, $\{(n,M) \in \mathbb{N} \times \mathcal{P}(\mathbb{N}) : \forall m \in \mathbb{N}, n + m = 10 \iff m \in M \}$. The disadvantage of this representation is that the regular set operations aren't useful on it. The advantage of this representation in Coq is that the relations behave like normal curried functions.
The prod_curry function can convert Coq's function-style relation to a pair-style relation, specifically an Ensemble (T * T). In reverse, a pair-style relation can be converted to function-style relation with prod_uncurry. Note that prod_curry and prod_uncurry seem to be reversed relative to Haskell's curry and uncurry functions. prod_uncurry actually curries a function, and prod_curry actually uncurries a function.

It is possible to manipulate relations by uncurrying them and using the Ensemble operations (like Union), then currying the result to convert it back to a function-style relation. Additionally, Coq has functions that work directly with relations. My goal for this series of posts was to stick with the Coq.Sets.* modules, but it turns out that Coq.Sets.Relations_1 is practically unusable due to all the missing manipulations for relations. Instead in this series of posts I will use Coq.Classes.RelationClasses for relations and continue to use Coq.Sets for Ensembles.

Cartesian product

The Cartesian product generates a relation from two sets. The relation contains every possible combination of an element from the left set with an element from the right set. There is some ambiguity as to how to translate to type theory, because the two input sets could be represented as Types or as Ensembles.

Since this post relies on homogeneous relations, that strongly limits what the Cartesian product can do for joining two types together; those types must be the same! Instead I decided to write a custom Cartesian product function (cartesian_product) that joins two Ensembles together, where both Ensembles use the same carrier type. However as the notations table describes, a type can be joined with itself to form a relation using true_predicate.

Definition translations

For the following table, let:
$\begin{aligned} X, Y &\subset T \\ U, V &\subset T \times T \\ x &\in X \end{aligned} $
Assume those variables are defined with the following Coq types:
Variable T : Type.
Variable X Y : Ensemble T.
Variable x : T.
Variable U V : binary_relation T.
Set theory notationDescriptionCoq syntaxModule
$U=V$ $U$ equals $V$ relation_equivalence U V Coq.Classes.RelationClasses
predicate_equivalence U V Coq.Classes.RelationClasses
same_relation T U V Coq.Relations.Relation_Definitions
same_relation T U V Coq.Sets.Relations_1
$U \subset V$ $U$ is a subset of $V$ subrelation U V Coq.Classes.RelationClasses
predicate_implication U V Coq.Classes.RelationClasses
inclusion T U V Coq.Relations.Relation_Definitions
contains T U V Coq.Sets.Relations_1
$U^{-1}$ inverse of $U$ inverse U Coq.Classes.RelationClasses
transp T U Coq.Relations.Relation_Operators
$U^c$ complement of $U$ complement U Coq.Classes.RelationClasses
Complement T U Coq.Sets.Relation_1_Facts
$U \cup V$ union of $U$ and $V$ relation_disjunction U V Coq.Classes.RelationClasses
predicate_union U V Coq.Classes.RelationClasses
union T U V Coq.Relations.Relation_Definitions
$U \cap V$ intersection of $U$ and $V$ predicate_intersection U V Coq.Classes.RelationClasses
relation_conjunction U V Coq.Classes.RelationClasses
$T \times T$ full relation of $T$ true_predicate : binary_relation T Coq.Classes.RelationClasses
$\emptyset$ empty set for $T$ false_predicate : binary_relation T Coq.Classes.RelationClasses
$X \times Y$ Cartesian product of $X$ and $Y$ cartesian_product X Y *sets_part3
$U \times V$ Cartesian product of $U$ and $V$ RelProd U V Coq.Classes.RelationPairs
$U - V$ $U$ minus $V$ relation_minus U V *sets_part3
$V \circ U$ composition of $V$ and $U$ (Note that $U$ is evaluated first, then $V$) relation_composition V U *sets_part3
$U[X]$ image of $X$ under relation $U$ relation_image U X *sets_part3
$U\{x\}$ image of $x$ under relation $U$ U x
$U \langle X \rangle$ relation_for_all U X *sets_part3
$U|X$ restriction of $U$ to $X$ relation_restriction U X *sets_part3
$\triangle$ diagonal of $T$ @eq T
$(X, U)$ relational space (X,U)
choice function choice Coq.Logic.ClassicalChoice

Extensions to Coq library: sets_part3.v


Exercises

Require Import sets_part3.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Classes.RelationClasses.

Section Lemma_1_38.

Variable T : Type.

Variable U V X Y : Ensemble T.

Lemma Lemma_1_38_i_a :
    relation_equivalence (cartesian_product (Empty_set T) V)
    (cartesian_product U (Empty_set T)).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_i_b :
    relation_equivalence (cartesian_product U (Empty_set T))
    (false_predicate:binary_relation T).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_ii :
    relation_equivalence
    (relation_conjunction (cartesian_product U V) (cartesian_product X Y))
    (cartesian_product (Intersection _ U X) (Intersection _ V Y)).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_iii :
    relation_equivalence
    (cartesian_product X (Union _ V Y))
    (relation_disjunction (cartesian_product X V) (cartesian_product X Y)).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_iv :
    relation_equivalence
    (cartesian_product X (Setminus _ Y V))
    (relation_minus (cartesian_product X Y) (cartesian_product X V)).
Proof.
  admit.
Qed.

End Lemma_1_38.

Section Lemma_1_39.

Variable T : Type.

Variable U : Ensemble T.
Variable V : Ensemble T.
Variable X : Ensemble T.
Variable Y : Ensemble T.

Hypothesis HXInU : Included _ X U.
Hypothesis HYInV : Included _ Y V.

(* This half of Lemma 1.39 can be proven using intuistionistic logic. *)

Lemma Lemma_1_39_constructive :
    subrelation
    (relation_disjunction
      (cartesian_product (Complement _ X) (Complement _ Y))
      (relation_disjunction
        (cartesian_product (Complement _ X) Y)
        (cartesian_product X (Complement _ Y))))
    (complement (cartesian_product X Y)).
Proof.
  admit.
Qed.

(* The other part of Lemma 1.39 requires the excluded middle. *)
Hypothesis classic : forall P:Prop, P \/ ~ P.

Lemma Lemma_1_39 :
    relation_equivalence
    (complement (cartesian_product X Y))
    (relation_disjunction
      (cartesian_product (Complement _ X) (Complement _ Y))
      (relation_disjunction
        (cartesian_product (Complement _ X) Y)
        (cartesian_product X (Complement _ Y)))).
Proof.
  admit.
Qed.

End Lemma_1_39.

Section Lemma_2_6.

Variable T : Type.

Variable X Y Z S : Ensemble T.

Variable U U' V V' W : binary_relation T.

Hypothesis HUSubXY : subrelation U (cartesian_product X Y).
Hypothesis HU'SubU : subrelation U' U.

Hypothesis HVSubYZ : subrelation V (cartesian_product Y Z).
Hypothesis HV'SubV : subrelation V' V.

Hypothesis HWSubZS : subrelation W (cartesian_product Z S).

Lemma Lemma_2_6_i :
    relation_equivalence (inverse (relation_composition V U))
      (relation_composition (inverse U) (inverse V)).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_ii :
    relation_equivalence (relation_composition (relation_composition W V) U)
      (relation_composition W (relation_composition V U)).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_iii :
    subrelation (inverse U') (inverse U).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_iv :
    subrelation (relation_composition V' U)
      (relation_composition V U).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_v :
    subrelation (relation_composition V U')
      (relation_composition V U).
Proof.
  admit.
Qed.

End Lemma_2_6.

Section Lemma_2_7.

Variable T : Type.

Variable X Y Z A : Ensemble T.

Variable U V : binary_relation T.

Hypothesis HUSubXY : subrelation U (cartesian_product X Y).

Hypothesis HVSubYZ : subrelation V (cartesian_product Y Z).

Hypothesis HASubX : Included _ A X.

Lemma Lemma_2_7 :
    relation_image (relation_composition V U) A =
    relation_image V (relation_image U A).
Proof.
  admit.
Qed.

End Lemma_2_7.

Solutions: sets_part3_exercises.v

Sunday, February 1, 2015

Learning set theory through Coq (part 2)

This post covers through page 22 (through lemma 1.36).

Power set

In set theory, one use of the power set is used to describe functions take subsets as input parameters or return subsets. For example $f : \mathcal{P}(U) \rightarrow U$ means that function $f$ takes a subset of $U$ and returns an element of $U$. In Coq, this kind of usage of the power set maps to describing the type of the input parameter: Ensemble U.

The rest of the time in set theory, the power set operator is used to build systems (sets of sets) where set operations are performed on the system. For example $Y \subset X \implies Y \in \mathcal{P}(X)$. This type of power set usage maps to Power_set _ X.

Ordered pairs

Set theory defines an ordered pair as a system, specifically $(x,y) = \big\{\{x,y\}, \{x\}\big\}$. However Coq defines an ordered pair using an inductive type without going through the set/Ensemble abstraction.

Coq's ordered pairs have most of the same properties as in set theory, except direct set operations are not allowed. For example, $(1,2) \cup (3,4)$ is defined (but avoided) in set theory, while it is disallowed by Coq's type checker.

Definition translations

For the following table, let $(x~y~z) : U$, $X \subset U$, and $A=(x,y)$.
Set theory notationPronunciationCoq syntax
$\mathcal{P}(U)$ power set of $U$
(as a Type)
Ensemble U
$\mathcal{P}(X)$ power set of $X$
(as an Ensemble)
Power_set U X
$\mathcal{P}(X)$ power set of $X$
(as an Ensemble)
Power_set U X
$\{x\}$ singleton of $x$
1-tuple of $x$
Singleton U x
$\{x, y\}$ unordered pair of $x$ and $y$
unordered 2-tuple of $x$ and $y$
Couple U x y
$\{x, y, z\}$ unordered triple of $x$, $y$, and $z$
unordered triplet of $x$, $y$, and $z$
unordered 3-tuple of $x$, $y$, and $z$
Triple U x y z
$(x, y)$ ordered pair of $x$ and $y$
ordered 2-tuple of $x$ and $y$
(x, y)
$A_l$ left coordinate of $A$ fst A
$A_r$ right coordinate of $A$ snd A

Exercises

(* Include the extended definitions from the previous post.
   Make sure you downloaded and compiled them. *)
Require Import sets_part1.

(* The exercise in lemma 1.31 does not translate to Coq. *)

Section Lemma_1_34.

Variable U : Type.

Definition US := Ensemble U.

Variable AS BS : Ensemble US.

(* The book's definition of a big intersection requires that the system is
   inhabited. So the exercise says AS and BS are inhabited so that the big
   intersection is defined for them.

   However the Coq definition given in part1 does not require the system to
   be inhabited. For completeness, these hypotheses are included. Uncomment
   them if you choose. They are not necessary to solve the exercises.
*)
(*
Hypothesis AS_inhabited : Inhabited US AS.
Hypothesis BS_inhabited : Inhabited US BS.
*)

Lemma Lemma_1_34_i : Intersection U (Big_union AS) (Big_union BS) =
    Big_union (
      fun x => exists A B,
        x = (Intersection U A B) /\
          In US AS A /\
          In US BS B
    ).
Proof.
  admit.
Qed.

(* Using intuitionistic logic, it is possible to prove that
   ((Big_intersection AS) union (Big_intersection BS)) is a subset of
   (Big_intersection {A union B | A in AS /\ B in BS}), but proving the converse
   requires classical logic.
*)
Lemma Lemma_1_34_ii_constructive :
    Included U (Union U (Big_intersection AS) (Big_intersection BS))
    (Big_intersection (
      fun x => exists A B,
        x = (Union U A B) /\
          In US AS A /\
          In US BS B
    )).
Proof.
  admit.
Qed.

(* The excluded middle is necessary to prove the other case. I found these
   two forms of the excluded middle helpful, but
   Coq.Logic.Classical_Pred_Type could be included instead. *)
Hypothesis not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.

Hypothesis classic : forall P:Prop, P \/ ~ P.

Lemma Lemma_1_34_ii : Union U (Big_intersection AS) (Big_intersection BS) =
    Big_intersection (
      fun x => exists A B,
        x = (Union U A B) /\
          In US AS A /\
          In US BS B
    ).
Proof.
  admit.
Qed.

End Lemma_1_34.

Section Lemma_1_35.

Variable X : Type.

Definition PX := Ensemble X.

Variable AS : Ensemble PX.

(*
Hypothesis AS_inhabited : Inhabited US AS.
*)

Lemma Lemma_1_35_i_constructive : Included X (Big_union (
    fun AC => exists A, In PX AS A /\ AC = Complement X A))
    (Complement X (Big_intersection AS)).
Proof.
  admit.
Qed.


(* The excluded middle is necessary to prove the other case. I found this
   form of the excluded middle helpful, but
   Coq.Logic.Classical_Pred_Type could be included instead. *)
Hypothesis not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.

Lemma Lemma_1_35_i : Complement X (Big_intersection AS) = Big_union (
    fun AC => exists A, In PX AS A /\ AC = Complement X A).
Proof.
  admit.
Qed.

(* This lemma can be proved constructively. *)
Lemma Lemma_1_35_ii : Complement X (Big_union AS) = Big_intersection (
    fun AC => exists A, In PX AS A /\ AC = Complement X A).
Proof.
  admit.
Qed.

End Lemma_1_35.

Solutions: sets_part2_exercises.v

Monday, January 26, 2015

Learning set theory through Coq (part 1)

Overview of the series

This is the first in a series of posts about how to use the Coq.Sets.* modules. Specifically this series will focus on translating the notations and concepts from set theory into Coq syntax.

The intended reader is expected to have little preexiting knowledge of set thoery, but is comfortable with Coq syntax knowledge. For learning Coq syntax, here are some excellent books on the subject:
Software Foundations
Interactive Theorem Proving and Program Development
Certified Programming with Dependent Types
Good documentation for Coq's standard library is difficult find. A thorough explanation of a module almost involves a books worth of information for the math behind it. This is a daunting task. Instead trying to write an entire book, I will attempt to bridge between an existing book on set theory and the Coq syntax. This series of posts follows along with Set theory and topology. An introduction to the foundations of analysis. Part I: Sets, relations, numbers by Felix Nagel, which is freely available online.

Each post will translates the concepts from a section of the book. Key concepts that do not translate well will be discussed in detail. However, for most concepts, their notation and translation will simply be listed in a table/cheat sheet.

The set theory book contains some definitions that are lacking in Coq's standard library. For these cases, I will provide a new Coq definition. In the translation table, these definitions are preceded by an asterisk. After the table, the Coq source for those definitions is attached to this post.

The exercises from the book will be translated into Coq syntax. A template Coq source file will be included inline with the post. Where ever the template says 'admit', the reader is expected to fill in this part with the completed proof. The solutions are attached as a .v file to the end of the post. I recommend reviewing the solutions if you are stuck, and even after completing the proof for examples of how to structure proofs.

When an exercise duplicates a theorem already in the standard library, the standard name for the theorem will be listed in the template. Of course the reader should not use that particular theorem to complete the exercise!

This post covers up to page 17 (through lemma 1.21).

Subsets

A subset is defined by examining all of the elements of the parent set, and only keeping the ones that meet the criteria for that subset. That criteria is a proposition (mathematical statement) that is called a predicate.

In type theory, a sigma type is a special kind of pair. The first component of the sigma is a parent type (e.g. the set of natural numbers). The second component is a predicate (e.g. the number is greater than 5) that restricts which instances of the parent type are accepted. Instances of the sigma type contain an instance from the parent type (e.g. 6), along with a proof that the predicate is met (e.g. le_S (le_n 5)) ).

Often a set is translated as a type in type theory -- sets have elements and types have instances. A subset is translated into a sigma type. This blog has some examples of how to use sigma types.

Representing subsets as sigma types breaks in a few cases. One is that instances of the sigma type are different from instances of the parent type. Instances of the sigma type have to be projected to pull out an instance of the parent type.

This type distinction becomes more apparent when subsets of subsets are considered. Let's start with a set called $A$, which is the natural numbers. $B$ is a subset of $A$ that contains only that are greater than 5. From $B$, a more restricted subset is created, called $C$. $C$ contains the natural numbers that are greater than 6.
\[ \begin{aligned}
A&=\mathbb{N} \\
B&=\{a \in A: a \gt 5 \} \\
C&=\{a \in B: a \gt 6 \} \\
\end{aligned} \]

The subset relation is transitive. So all of the elements in $C$ are also in $A$.
\[ \begin{aligned}
B &\subset A \\
C &\subset B \\
C &\subset A
\end{aligned} \]

$C$ could be translated as a sig of $B$. In this case, instances of $C$ are no longer instances of $A$. An alternative is to pair $C$'s predicate with $B$'s predicate using sig2. In this case, an instance of $A$ can be pulled out from an instance of $C$, but $C$ does not directly contain instances of $B$ in it.

Another problem with saying subsets are sigma types is with the power set. Describing every possible sigma type for $A$ is a dependent type. So one cannot write a function that has a single parameter, and that parameter is any possible sigma type for $A$. Instead the function would need two parameters: one for the predicate and one for the sigma type.

To fill these gaps, Coq has another subset-like object called an Ensemble. The Ensemble is really just the predicate for the subset. To write a function that takes an element from an Ensemble, it can be wrapped in a sigma type.

The Coq.Sets library is awkward to use because the parent of the Ensemble needs to be passed everywhere. Ideally it would be an implicit parameter instead, but I didn't write the library...

Set equality

The previous section discussed why sets are represented as Ensembles, which are really a type of function. Coq's default equality is intensional equality, in which two functions are the same if they are judgementally equal (which basically means they have the same definition once the functions they call are inlined).

In ZF set theory, the extensionality axiom (axiom 1.2 in the book) says that two sets are equal if they contain exactly the same elements. This is the same as saying two functions are the same if they always return the same output for the same input. So extensional and intensional equality are different.

Unfortunately Coq.Sets.Ensembles adds the Extensionality_Ensembles axiom, which could escape and apply to more than just Ensembles.

Definition translations

For the following table, let $A, B \subset U$, and let $\mathcal{C}$ be a system of subsets of $U$.
Set theory notationPronunciationCoq syntax
$\{x : U | P(x)\}$ the set of all $x$ from $U$ such that $P$ is true for $x$ fun x : U => P x
(to represent the set as an Ensemble)
{x : U | P x}
(to represent the set as a sig type)
$a \in A$ $a$ is an element of $A$ In U A a
$a \notin A$ $a$ is not an element of $A$ ~ In U A a
$A = B$ $A$ equals $B$ Same_set U A B,
or using the Extensionality_Ensembles axiom, A = B
$A \subset B$ $A$ is a subset of $B$ Included U A B
(Note this only works when (A B : Ensemble U), otherwise use Full_set to convert U into an Ensemble.)
$A \supset B$ $A$ is a superset of $B$, or $A$ contains $B$ Included U B A
(Note this only works when (A B : Ensemble U), otherwise use Full_set to convert U into an Ensemble.)
$A \subsetneq B$ $A$ is a proper subset of $B$ Strict_Included U A B
(Note this only works when (A B : Ensemble U), otherwise use Full_set to convert U into an Ensemble.)
let $A \subset U$ let $A$ be a subset of $U$ Variable A : Ensemble U.
let $A \subset U \wedge A = U$ let $A$ be the full set of $U$ Definition A : Ensemble U := Full_set U
$\emptyset$ empty set Empty_set U
(Note there is a unique empty set for every type U.)
$A \cup B$ union of $A$ and $B$ Union U A B
$A \cap B$ intersection of $A$ and $B$ Intersection U A B
$\bigcup \mathcal{C}$ union of $\mathcal{C}$ *Big_union C
$\bigcap \mathcal{C}$ intersection of $\mathcal{C}$ *Big_intersection C
$A \cap B = \emptyset$ $A$ and $B$ are disjoint Disjoint U A B
$A \setminus B$ difference of $A$ and $B$ Setminus U A B
$A^c$ complement of $A$ in $U$ Complement U A

Other notable definitions: Union_introl, Union_intror, and Intersection_intro.

Notable theorems

For the following table, let $A, B \subset U$.
Set theory notationNameCoq name
$A \cup B = B \cup A$ union commutativity Union_commutative
$A \cap B = B \cap A$ intersection commutativity Intersection_commutative
$A \cup (B \cup C) = (A \cup B) \cup C$ union associativity Union_associative
$A \cap (B \cap C) = (A \cap B) \cap C$ intersection associativity Intersection_associative
$A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$ distributivity Distributivity
$A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$ distributivity Distributivity'

Extensions to Coq library: sets_part1.v


Exercises

Require Import Coq.Sets.Ensembles.

Section Lemma_1_18.

Variable U : Type.

Variable (A B C : Ensemble U).

(* This is the same as Union_commutative *)
Lemma i_a : Union U A B = Union U B A.
Proof.
  admit.
Qed.

(* This is the same as Intersection_commutative *)
Lemma i_b : Intersection U A B = Intersection U B A.
Proof.
  admit.
Qed.

(* This is the same as Union_associative *)
Lemma ii_a : Union U A (Union U B C) = Union U (Union U A B) C.
Proof.
  admit.
Qed.

(* This is the same as Intersection_associative *)
Lemma ii_b : Intersection U A (Intersection U B C) = Intersection U (Intersection U A B) C.
Proof.
  admit.
Qed.

(* This is the same as Distributivity *)
Lemma iii_a :
    Intersection U A (Union U B C) =
    Union U (Intersection U A B) (Intersection U A C).
Proof.
  admit.
Qed.

(* This is the same as Distributivity' *)
Lemma iii_b :
    Union U A (Intersection U B C) =
    Intersection U (Union U A B) (Union U A C).
Proof.
  admit.
Qed.

(* Using intuitionistic logic, it is possible to prove that
   (A intersection B) is a subset of (A \ (A \ B)), but proving the converse
   requires classical logic. *)
Lemma iv_constructive :
    Included U (Intersection U A B) (Setminus U A (Setminus U A B)).
Proof.
  admit.
Qed.

(* Either add this one classical axiom only to this section *)
Hypothesis NNPP : forall p:Prop, ~ ~ p -> p.
(* or uncomment the following line to import all of Classical_Prop for this
   whole module *)
(* Require Import Coq.Logic.Classical_Prop. *)
Lemma iv : Setminus U A (Setminus U A B) = Intersection U A B.
Proof.
  admit.
Qed.

End Lemma_1_18.

Section Lemma_1_19.

Variable X : Type.

Variable (A B : Ensemble X).

(* This half is provable using intuitionistic logic *)
Lemma a_constructive :
    Included X (Union X (Complement X A) (Complement X B))
    (Complement X (Intersection X A B)).
Proof.
  admit.
Qed.

Hypothesis NNPP : forall p:Prop, ~ ~ p -> p.

Lemma a :
    Complement X (Intersection X A B) =
    Union X (Complement X A) (Complement X B).
Proof.
  admit.
Qed.

(* This half is provable using intuitionistic logic *)
Lemma b_constructive :
    Included X (Intersection X (Complement X A) (Complement X B))
    (Complement X (Union X A B)).
Proof.
  admit.
Qed. 

Lemma b :
    Complement X (Union X A B) = 
    Intersection X (Complement X A) (Complement X B).
Proof.
  admit.
Qed.

End Lemma_1_19.

Solutions: sets_part1_exercises.v

Friday, January 23, 2015

Dependent typing from a C++ perspective

Coq has a feature called dependent typing. In Coq, among other things, dependent types are used to represent propositions (mathematical statements) and proofs of those propositions. This post explains how propositions are represented as types in Coq, and what happens if same tricks are applied in C++ (the short answer is that it doesn't work).

Hints to the power of static typing

First let me try to convince you that maybe it is possible to represent proofs using static typing. Unless you have heard of the Curry-Howard correspondence, the idea of representing a proof as a type probably sounds crazy. Proofs can be incredibly complex, and at first glance it doesn't seem like there is enough complexity in a static typing system to represent that.

For a C++ developer, the rules for static typing are complicated, but once they are built into the compiler, it doesn't feel like the compiler is really doing a lot of computation to apply them. It seems like you could almost find an upper bound for the amount of computation the compiler does for any given expression.

Many times I've found quickly found a class I want to use in the Java API docs, but then I spend an hour trying to figure out how to even create an instance of the class. The class I want is built through a static factory method. The factory method wants 2 other classes instantiated first. The constructors for those classes want other objects built first, and so on. This gives a hint at how static typing can get complex.

With Java the complexity is pretty much capped by the number of classes/interfaces in the library. The static typing system gets even more powerful with C++ templates. Now new types can be recursively built, and even used to do things like template metaprogramming.

Informal proof

We'll use an example proof to show how dependent typing works. The statement uses natural numbers, which is an integer greater than or equal to 0 (such as 0, 1, 2, etc). The statement to prove is really simple, it is: $\text{forall } n (\text{where $n$ is a natural number}), 1 \leq n + 1$.

Now let's to prove that statement with a traditional proof using induction (if you don't know what induction is, it will make sense soon). For understandability, this proof is written in a very explicit manner, which unfortunately makes the proof much longer.

Let $n$ be an arbitrary natural number. Either $n = 0$ or $n \geq 1$.
  • Let's take the first case where $n = 0$. This is called the base case. In this case, $1 \leq n + 1$. That simplifies to $1 \leq 0 + 1$, which is trivially true.
  • Next we prove the second case. This is called the inductive step. We prove the second case by proving that the statement is true when $n = n' + 1$, assuming that the statement is already proved for $n'$. Note that $n'$ is just a variable name; it isn't a derivative.

    Again, we are trying to prove $1 \leq n + 1$, which is the same as $1 \leq n' + 1 + 1$. Our assumption says that $1 \leq n' + 1$.

    Trivially, $n' + 1 \leq n' + 1 + 1$.
    So $1 \leq n' + 1 + 1$.
$\blacksquare$

We tend to learn about induction as a set pattern without really learning why it works. The induction proof can be thought of as a set of steps to generate a specific proof for any specific natural number, $n$.
  1. Use the base case to get a proof for when $a = 0$. If $n = 0$, use this proof and stop here.
  2. While $a \lt n$, apply the induction step to get a proof for $a := a + 1$.
Let's say that we want to use the proof for $1 \leq n + 1$, when $n = 3$. First the base case is used to generate a proof for $a = 0$. Next the induction step is run. The induction step uses the proof for $a = 0$ to generate a new proof for $a' = 0$. The induction step is run 2 more times until a proof is generated for $n= 3$.

The induction proof can be thought of as a short program that takes $n$ as an input parameter, then it unrolls the induction steps to generate a proof of the statement for $n$. The program returns that generated proof. Now the proof is starting to sound like a computer program!

Natural numbers

Before jumping into how the proof translates into C++, we need to be more formal about how natural numbers are defined. The unsigned integer types in C++ have an upper bound of $2^64$ or $2^128$ depending on the compiler. In math, the set of natural numbers does not have an upper bound, so we can't use C++'s built-in integer types to represent natural numbers.

Coq uses the Peano construction for natural numbers, so we'll use the same thing in C++. Note Peano is pronounced "pay-a-no" in native Italian but often bastardized to "piano" in English.

With peano numbers, $0$ is axiomatically defined (meaning it exists, but the concept can't be broken down further). Then there is a constructor (for now think function) that adds $1$ to any natural number. So 2 is represented as $0+1+1$.

In C++, those rules can be encoded using template metaprogramming. Of course the downside to using metaprogramming is that the natural numbers can only be defined at compile time.

// A generic base for all natural numbers
struct nat
{
};

// A type representing 0
struct nat_0 : public nat
{
};

// A template that adds 1 to a natural number.
// So 3 is defined as nat_S<nat_S<nat_S<nat_0> > >
template <class Pred>
struct nat_S : public nat
{
};

This post isn't about Coq syntax, but for the sake of completeness, I'll include the equivalent Coq code. The nat_0 function is simply called O and nat_S is called S.
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Pattern matching

In Coq, the S constructor (nat_S in C++) is a function in the sense that you can pass a natural number it a number and the constructor will return that number plus 1. However, the constructor is more than a regular function because pattern matching can be performed on the result. Pattern matching means that you can break apart a natural number to determine if it was constructed by calling 0 or by calling S. If it was constructed with S, you can determine what the parameter was for S.

Fortunately the pattern matching for the constructor maps well to the template structure we used for the C++ definitions. The pattern matching can be performed using template specialization or function overloading. In either case, one can determine whether a natural number was built with nat_0 or nat_S.

Let's use function overloading to define an equality operator for natural numbers.
// The compiler tries first to use this overload because the parameters are
// derived types (nat_0 instead of nat), and this overload does not use
// templates.
constexpr bool operator == (const nat_0 &, const nat_0 &)
{
    return true;
}

// If the first overload fails, the compiler tries this one next, because this
// overload uses a derived types for its parameters (nat_S instead of nat).
template <class Pred1, class Pred2>
constexpr bool operator == (const nat_S<Pred1> &, const nat_S<Pred2> &)
{
    return Pred1() == Pred2();
}

// Finally if nothing else works, the compiler will use this overload. This
// overload is least preferred because the compiler has to cast the parameters
// to the base type.
constexpr bool operator == (const nat &, const nat &)
{
    return false;
}

Coq's standard definition for equality is more complicated than the C++ example. Here is what the simplified example equality function maps to in Coq:
Fixpoint nat_eq (m n: nat) : bool :=
  match m,n with
    | O, O => true
    | S m', S n' => nat_eq m' n'
    | _, _ => false
  end.

As another example of pattern matching, we'll define the pred function. The pred function performs truncated decrement. This means if the input parameter is 1 or larger, the function subtracts 1 from the parameter. Otherwise 0 is returned. Also the pred function an the equality operator from above can be validated against each other.
// The compiler tries this overload first
constexpr nat_0 pred(const nat_0 &n)
{
    return n;
}

// The compiler tries this overload second
template <typename Pred>
constexpr Pred pred(const nat_S<Pred> &n)
{
    return Pred();
}

// Show that pred(0) returns 0
static_assert(pred(nat_0{}) == nat_0{}, "must be equal");
// Show that pred(1) != 1
static_assert(!(pred(nat_S<nat_0>{}) == nat_S<nat_0>{}), "must not be equal");

This time the C++ code was a direct translation of the standard Coq pred function.
Definition pred (n : nat) :=
  match n with
  | 0 => n
  | S p => p
  end.

Less-than-equal binary relation

So far natural numbers, incrementing, and decrementing have been precisely defined. The last definition used by the proof is $\le$. In math, $\le$ is called a binary relation because it describes a property between two operands (that is $m \leq n$).

In the C++ example, the $\leq$ relation is translated into a templated class called le. The two operands to compare are passed to the le class as template parameters.

In C++, <= is an operator that returns a true/false boolean. The le class does something quite different. Instead of returning a bool, the le<m,n> class can only be constructed if the proposition is true, namely m <= n.

Using public functions (constructors or factory method), there are only two ways to construct an instance of le<m,n>. An instance of le<n,n> can be constructed using the le_n() factory method. As the signature implies, this function can only build le<m,n> when m = n.

The other factory method, le_S() basically constructs le<m, n+1>, but it requires an instance of le<m, n>. So for example, le<1, 3> could constructed with these steps:
  1. Create le<1,1> using le_n()
  2. Create le<1,2> using le_S()
  3. Create le<1,3> using le_S()

// Can only instantiate the le class if m is less than or equal to n. m and n
// are peano numbers.
template<class m, class n>
class le
{
private:
    le()
    {
    }

    // There are only 2 ways to externally create the le class. The le_n case
    // covers when n = n.
    template<class o>
    friend le<o, o> le_n();

    // The le_S case lets one prove that n <= m + 1, but only if n <= m.
    template<class o, class p>
    friend le<o, nat_S<p> > le_S(const le<o, p> &);
};

template<class m>
le<m, m> le_n()
{
    return le<m, m>();
}

template<class m, class n>
le<m, nat_S<n> > le_S(const le<m, n> &)
{
    return le<m, nat_S<n> >();
}

If the proposition is false, namely m > n, there simply are no public constructors or factory functions to build le<m,n>.

Let's say m > n. You can still describe the type le<m,n>, but there is simply no way to instantiate it using public constructors or factory methods. A functions could have a parameter of type le<m,n>, but since you can't instantiate le<m,n>, you can't run the function.

Again, here is the equivalent Coq code:
Inductive le (m : nat) : nat -> Prop :=
  | le_n : le m m
  | le_S : forall n : nat, le m n -> le m (S n).

Formal Proof

Now we have the pieces to try implementing the proof in C++. Again the proof statement is $\text{forall } n (\text{where $n$ is a natural number}), 1 \leq n + 1$.

As discussed under the informal proof section, because of the $\text{forall } n$ part of the proposition, this proof can be thought of as a proof generator: a function that takes $n$ as a parameter and returns a proof for that specific $n$.

In C++ we'll call this function le_plus_1. The induction is implemented using pattern matching through function overloading.

Let's start with the base case where $n = 0$. For the base case, the statement simplifies as follows:
\[ \begin{aligned}
  1 &\leq n + 1\\
  1 &\leq 0 + 1\\
  1 &\leq 1\\
\end{aligned} \]
Now the base case can be implemented in C++ as:
le<nat_S<nat_0>, nat_S<nat_0>> le_plus_1(const nat_0 &)
{
    return le_n<int_to_nat<1>::type>();
}
The induction step has to prove $1 \leq (n + 1) + 1$, which translates to instantiating this type: \[
  \text{le<}1, (n + 1) + 1\text{>}\\
  \text{le< nat_S<nat_0>, nat_S<nat_S<$n$>> >}
\] The induction step is given $1 \leq n + 1$ as an assumption. In C++, obtaining the assumption translates into using recursion. So le_plus_1($n+1$) calls le_plus_($n$).
template <typename N>
le<nat_S<nat_0>, nat_S<nat_S<N>> > le_plus_1(const nat_S<N> &n)
{
    return le_S(le_plus_1(pred(n)));
}

In Coq, the proof looks like:
Lemma le_plus_1 : forall n:nat, 1 <= n + 1.
Proof.
  induction n.
  + (* Base case. Prove 1 <= 0 + 1 *)
    exact (le_n 1).
  + (* Induction case. Prove 1 <= S n + 1, given the assumption as IHn *)
    apply le_S.
    exact IHn.
Qed.

How the proof breaks in C++

The le_plus_1 function acts like a proof generator. Given a specific $n$, it returns a proof for that $n$. The problem is that le_plus_1 is written as a template function and template use adhoc polymorphism. That means the C++ compiler does not validate the function until it is instantiated (given specifics value for its template parameters).

So le_plus_1 generates proofs for specific values of n, and the compiler validates those generated proofs. The compiler does not validate that le_plus_1 works forall n. It only validates the specific values of n that the proof is instantiated with.

Hypothetically the base case could be tested and correct, but the induction step could be untested and incorrect. To validate the proof, each branch in the proof needs to be validated with its own test case. Granted that once the correct input values are determined to test the branch, the validation is simple: make sure it compiles.

On the other hand, Coq uses dependent typing instead of adhoc polymorphism. One advantage is that the Coq compiler automatically validates that le_plus_1 works for all values of n, without having to give test cases.

With C++, all template metaprogramming is run at compile time. There is no way to let the user input an integer, then convert that to the proper instance of our nat class. With Coq, new nat can be created at runtime, and they can be passed to functions that use dependent typing.

Monday, January 19, 2015

Enabling math symbols and coq syntax highlighting

This post is about the tools used to produce this blog. The blog is freely hosted at blogger.com. MathJax is installed for printing equations like \[ \cos^2\theta-\sin^2\theta=\cos 2\theta. \]

In addition to mathematical equations, coq source code snippets are posted with SyntaxHighlighter. For example,
Lemma Rgt_0_mult_r2n_compat : forall (x r:R)(n:nat), x > 0 -> Rabs r >= 1 -> x * r ^ (2 *n) >= x.
Proof.
  intros.
  apply Ropp_ge_cancel.
  apply Rle_ge.
  rewrite <- 2?Ropp_mult_distr_l_reverse.
  apply Ropp_gt_lt_contravar in H.
  rewrite Ropp_0 in H.
  now apply Rlt_0_mult_r2n_compat.
Qed.

I started using this blog's MathJax installation directions, but it recommends directly editing the template source. That works, but if the template is ever edited with the GUI editor, the custom changes are lost.

Instead, I added two HTML/JavaScript widgets. The first widget is on the top of the page and gets run before the posts are shown. In order for this widget to have a visible artefact on the page, I had to
  1. leave the widget untitled (it shows up as HTML/JavaScript when the title is blank)
  2. edit the template source to move the widget into the navbar section.

(Click the below image to view it full-size)


Specifically this source code is included in the first widget for MathJax:
<script src='http://cdn.mathjax.org/mathjax/latest/MathJax.js' type='text/javascript'>    
    MathJax.Hub.Config({
        HTML: ["input/TeX","output/HTML-CSS"],
        TeX: { extensions: ["AMSmath.js","AMSsymbols.js"], 
               equationNumbers: { autoNumber: "AMS" } },
        extensions: ["tex2jax.js"],
        jax: ["input/TeX","output/HTML-CSS"],
        tex2jax: { inlineMath: [ ['$','$'], ["\\(","\\)"] ],
                   displayMath: [ ['$$','$$'], ["\\[","\\]"] ],
                   processEscapes: true },
        "HTML-CSS": { availableFonts: ["TeX"],
                      linebreaks: { automatic: true } }
    });
</script>

Beyond using the HTML/JavaScript widget, there is some futher customization for SyntaxHighlighter. Sometimes the blogger website is accessed through HTTPS. The recommended installation suggests using these links:
<link href='http://agorbatchev.typepad.com/pub/sh/3_0_83/styles/shCore.css' rel='stylesheet' type='text/css'/>
<link href='http://agorbatchev.typepad.com/pub/sh/3_0_83/styles/shThemeDefault.css' rel='stylesheet' type='text/css'/>
<script src='http://agorbatchev.typepad.com/pub/sh/3_0_83/scripts/shCore.js' type='text/javascript'/>

Instead I am using the links below, because they still work if http is replaced with https. When the blog is accessed through https, Firefox is implicitly replaces the http with https. Also the source code doesn't stand out enough, so the default style is tweaked slightly to add a border.
<link href='http://alexgorbatchev.com/pub/sh/current/styles/shCore.css' rel='stylesheet' type='text/css'/>
<link href='http://alexgorbatchev.com/pub/sh/current/styles/shThemeDefault.css' rel='stylesheet' type='text/css'/>
<script src='http://alexgorbatchev.com/pub/sh/current/scripts/shCore.js' type='text/javascript'/>

<style>
  .syntaxhighlighter {
    border: 1px solid #DADAD9 !important;
    margin-bottom: 20px !important;
    padding: 1px !important;
  }
</style>

The code to turn on SyntaxHighlighter needs to be separate and after the posts that use the plugin. I included it in a second widget located above the attribution bar. That location is good because it doesn't have visible artefacts and it is after the posts.

SyntaxHighlighter does not have builtin support (called a brush) for Coq's syntax. So in addition to enabling SyntaxHighlighter, a custom brush is defined for Coq that matches coqide's syntax highlighting:
<script language='javascript' type='text/javascript'>
    SyntaxHighlighter.brushes.Coq = function()
    { 
        var definitions = 'Definition Lemma Fixpoint '
                       + 'Variable Lemma Hypothesis';
        var keywords = 'Require Import Proof forall '
                       + 'Qed with as Hint Resolve in '
                       + 'Section Type End Prop';
        this.regexList = [
            { regex:
              /\(\*[\s\S]*?\*\)/gm,
              css: 'comments'
            }, // multiline comments
            { regex: new RegExp(this.getKeywords(keywords), 'gmi'), css: 'keyword' },
            { regex: new RegExp(this.getKeywords(definitions), 'gmi'), css: 'color2' }
        ];
    }; 
    SyntaxHighlighter.brushes.Coq.prototype = new SyntaxHighlighter.Highlighter();  
    SyntaxHighlighter.brushes.Coq.aliases   = ['coq'];

    SyntaxHighlighter.config.bloggerMode = true;
    SyntaxHighlighter.all();
</script>

To insert Coq source code inside of a post, switch to the HTML view for the post editor, then paste something like the following:
<pre class="brush: coq">Lemma Rgt_0_mult_r2n_compat : forall (x r:R)(n:nat), x > 0 -> Rabs r >= 1 -> x * r ^ (2 *n) >= x.
Proof.
  intros.
  apply Ropp_ge_cancel.
  apply Rle_ge.
  rewrite <- 2?Ropp_mult_distr_l_reverse.
  apply Ropp_gt_lt_contravar in H.
  rewrite Ropp_0 in H.
  now apply Rlt_0_mult_r2n_compat.
Qed.
</pre>