Module Playground. Inductive nat : Type := | O : nat | S : nat -> nat. (** The clauses of this definition can be read: - [O] is a natural number (note that this is the letter "[O]," not the numeral "[0]"). - [S] is a "constructor" that takes a natural number and yields another one -- that is, if [n] is a natural number, then [S n] is too. Let's look at this in a little more detail. Every inductively defined set ([day], [nat], [bool], etc.) is actually a set of _expressions_. The definition of [nat] says how expressions in the set [nat] can be constructed: - the expression [O] belongs to the set [nat]; - if [n] is an expression belonging to the set [nat], then [S n] is also an expression belonging to the set [nat]; and - expressions formed in these two ways are the only ones belonging to the set [nat]. The same rules apply for our definitions of [day] and [bool]. The annotations we used for their constructors are analogous to the one for the [O] constructor, and indicate that each of those constructors doesn't take any arguments. *) (** These three conditions are the precise force of the [Inductive] declaration. They imply that the expression [O], the expression [S O], the expression [S (S O)], the expression [S (S (S O))], and so on all belong to the set [nat], while other expressions like [true], [andb true false], and [S (S false)] do not. We can write simple functions that pattern match on natural numbers just as we did above -- for example, the predecessor function: *) Definition pred (n : nat) : nat := match n with | O => O | S n' => n' end. (** The second branch can be read: "if [n] has the form [S n'] for some [n'], then return [n']." *) End Playground. Definition minustwo (n : nat) : nat := match n with | O => O | S O => O | S (S n') => n' end. Check minustwo. (** The Check command asks Coq to print the type of an expression. *) (** Because natural numbers are such a pervasive form of data, Coq provides a tiny bit of built-in magic for parsing and printing them: ordinary arabic numerals can be used as an alternative to the "unary" notation defined by the constructors [S] and [O]. Coq prints numbers in arabic form by default: *) Check (S (S (S (S O)))). Eval simpl in (minustwo 4). Compute (minustwo 5). (** The constructor [S] has the type [nat -> nat], just like the functions [minustwo] and [pred]: *) Check S. Check pred. Check minustwo. (** All the above three can be applied to a number to yield a number. However, there is a fundamental difference: functions like [pred] and [minustwo] come with _computation rules_ -- e.g., the definition of [pred] says that [pred 2] can be simplified to [1] -- while the definition of [S] has no such behavior attached. Although it is like a function in the sense that it can be applied to an argument, it does not _do_ anything at all! It is just a way of writing down numbers. (Think about standard decimal numerals: the numeral [1] is not a computation; it's a piece of data. When we write [111] to mean the number one hundred and eleven, we are using [1] three times, to write down a concrete representation of a number.) *) Module Playground2. (** recursive functions *) Fixpoint plus (n : nat) (m : nat) : nat := match n with | O => m | S n' => S (plus n' m) end. Check (plus 3). Check plus 3 5. Compute (plus 3 5). Compute (plus (S (S (S O))) (S (S O))). (** The simplification that Coq performs to reach this conclusion can be visualized as follows: *) (* [plus (S (S (S O))) (S (S O))] ==> [S (plus (S (S O)) (S (S O)))] by the second clause of the [match] ==> [S (S (plus (S O) (S (S O))))] by the second clause of the [match] ==> [S (S (S (plus O (S (S O)))))] by the second clause of the [match] ==> [S (S (S (S (S O))))] by the first clause of the [match] *) (** As a notational convenience, if two or more arguments have the same type, they can be written together. In the following definition, [(n m : nat)] means just the same as if we had written [(n : nat) (m : nat)]. *) Fixpoint mult (n m : nat) : nat := match n with | O => O | S n' => plus m (mult n' m) end. Lemma test_mult1: (mult 3 3) = 9. Proof. reflexivity. Qed. (** A tactic (e.g. [reflexivity]) is a command that is used between Proof and Qed to guide the process of checking some claim we are making. We use [reflexivity] to check that both sides of the equality contain identical values. *) (** You can match two expressions at once by putting a comma between them: *) Fixpoint minus (n m : nat) : nat := match n, m with | O , _ => O | S _ , O => n | S n', S m' => minus n' m' end. (** The _ in the first line is a _wildcard pattern_. Writing _ in a pattern is the same as writing some variable that doesn't get used on the right-hand side. This avoids the need to invent a bogus variable name. *) Lemma plus_S: forall m n, plus m (S n) = S (plus m n). Proof. induction m. - auto. - intro n. simpl. rewrite -> IHm. reflexivity. Qed. (** There are several ways to state that a number [n] is even. - You may define a recursive function [evenb : nat -> bool]. - Or, you may write inductively defined propositions. (We will discuss propositions in detail later. ) We say n is even if we can establish its evenness from the following rules: + Rule [even_O]: The number [O] is even. + Rule [even_S]: If [n] is even, then [S (S n)] is even. We translate this definition into a formal Coq definition using an [Inductive] declaration, where each constructor corresponds to an inference rule. *) Inductive even : nat -> Prop := | even_O: even O | even_S: forall n, even n -> even (S (S n)). (** This definition is different in one crucial respect from previous uses of [Inductive]: the thing we are defining is not a [Type], but rather a function from [nat] to [Prop] — that is, a property of numbers. *) (** We can think of the definition of [even] as defining a Coq property [even] : nat → Prop, together with primitive theorems [even_O] and [even_S]. Such "constructor theorems" have the same status as proven theorems. In particular, we can use Coq's [apply] tactic with the rule names to prove [even] for a number. *) Lemma even_4 : even 4. Proof. apply even_S. apply even_S. apply even_O. Qed. Lemma mult_2_even: forall n, even (mult 2 n). Proof. induction n. - simpl. apply even_O. - simpl. simpl in IHn. assert (plus n (S (plus n 0)) = S ((plus n (plus n 0)))). apply plus_S. (* [plus_S] is a lemma we just proved. *) rewrite -> H. apply even_S. exact IHn. Qed. (** [lia] is a tactic for solving goals in linear integer arithmetic, i.e. for proving formulas made of equations and inequalities over the type [nat] of natural numbers or the type [Z] of binary-encoded integers. *) Require Import Psatz. Lemma mult_2_ge_self: forall n, 2 * n >= n. Proof. intro n. lia. Qed. Lemma plus_commut: forall m n, plus m n = plus n m. Proof. intros m n. admit. Admitted. End Playground2. Module NatList. (* ###################################################### *) (** * Lists of Numbers *) (** Generalizing the definition of pairs a little, we can describe the type of _lists_ of numbers like this: "A list is either the empty list or else a pair of a number and another list." *) Inductive natlist : Type := | nil : natlist | cons : nat -> natlist -> natlist. (** For example, here is a three-element list: *) Definition mylist := cons 1 (cons 2 (cons 3 nil)). (** *** *) (** As with pairs, it is more convenient to write lists in familiar programming notation. The following two declarations allow us to use [::] as an infix [cons] operator and square brackets as an "outfix" notation for constructing lists. *) Notation "x :: l" := (cons x l) (at level 60, right associativity). Notation "[ ]" := nil. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). (** It is not necessary to fully understand these declarations, but in case you are interested, here is roughly what's going on. The [right associativity] annotation tells Coq how to parenthesize expressions involving several uses of [::] so that, for example, the next three declarations mean exactly the same thing: *) Definition mylist1 := 1 :: (2 :: (3 :: nil)). Definition mylist2 := 1 :: 2 :: 3 :: nil. Definition mylist3 := [1;2;3]. (** The [at level 60] part tells Coq how to parenthesize expressions that involve both [::] and some other infix operator. For example, since we defined [+] as infix notation for the [plus] function at level 50, Notation "x + y" := (plus x y) (at level 50, left associativity). The [+] operator will bind tighter than [::], so [1 + 2 :: [3]] will be parsed, as we'd expect, as [(1 + 2) :: [3]] rather than [1 + (2 :: [3])]. (By the way, it's worth noting in passing that expressions like "[1 + 2 :: [3]]" can be a little confusing when you read them in a .v file. The inner brackets, around 3, indicate a list, but the outer brackets, which are invisible in the HTML rendering, are there to instruct the "coqdoc" tool that the bracketed part should be displayed as Coq code rather than running text.) The second and third [Notation] declarations above introduce the standard square-bracket notation for lists; the right-hand side of the third one illustrates Coq's syntax for declaring n-ary notations and translating them to nested sequences of binary constructors. *) (** *** Repeat *) (** A number of functions are useful for manipulating lists. For example, the [repeat] function takes a number [n] and a [count] and returns a list of length [count] where every element is [n]. *) Fixpoint repeat (n count : nat) : natlist := match count with | O => nil | S count' => n :: (repeat n count') end. (** *** Length *) (** The [length] function calculates the length of a list. *) Fixpoint length (l : natlist) : nat := match l with | nil => O | h :: t => S (length t) end. (** *** Append *) (** The [app] ("append") function concatenates two lists. *) Fixpoint app (l1 l2 : natlist) : natlist := match l1 with | nil => l2 | h :: t => h :: (app t l2) end. Lemma app_prop: forall l1 l2, length (app l1 l2) = length l1 + length l2. Admitted. (** Actually, [app] will be used a lot in some parts of what follows, so it is convenient to have an infix operator for it. *) Notation "x ++ y" := (app x y) (right associativity, at level 60). Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5]. Proof. simpl. reflexivity. Qed. Example test_app2: nil ++ [4;5] = [4;5]. Proof. reflexivity. Qed. Example test_app3: [1;2;3] ++ nil = [1;2;3]. Proof. reflexivity. Qed. (** Here are two smaller examples of programming with lists. The [hd] function returns the first element (the "head") of the list, while [tl] returns everything but the first element (the "tail"). Of course, the empty list has no first element, so we must pass a default value to be returned in that case. *) (** *** Head (with default) and Tail *) Definition hd (default:nat) (l:natlist) : nat := match l with | nil => default | h :: t => h end. Definition tl (l:natlist) : natlist := match l with | nil => nil | h :: t => t end. Example test_hd1: hd 0 [1;2;3] = 1. Proof. reflexivity. Qed. Example test_hd2: hd 0 [] = 0. Proof. reflexivity. Qed. Example test_tl: tl [1;2;3] = [2;3]. Proof. reflexivity. Qed. (** *** Reversing a list *) (** For a slightly more involved example of an inductive proof over lists, suppose we define a "cons on the right" function [snoc] like this... *) Fixpoint snoc (l:natlist) (v:nat) : natlist := match l with | nil => [v] | h :: t => h :: (snoc t v) end. (** ... and use it to define a list-reversing function [rev] like this: *) Fixpoint rev (l:natlist) : natlist := match l with | nil => nil | h :: t => snoc (rev t) h end. Example test_rev1: rev [1;2;3] = [3;2;1]. Proof. reflexivity. Qed. Example test_rev2: rev nil = nil. Proof. reflexivity. Qed. Fixpoint map (f: nat -> nat) (l: natlist) : natlist := match l with | nil => nil | h :: t => f h :: (map f t) end. Compute map (fun n => n*n) [1;2;3]. End NatList. Module LOGIC. Check True. Check False. Check true. Check false. Check bool. Check Set. Check Prop. (** Here is an example of a provable proposition: *) Check (3 = 3). Check (5 = 3). (* ===> Prop *) (** Here is an example of an unprovable proposition: *) Check (forall (n:nat), n = 2). (* ===> Prop *) (* ########################################################### *) (** * Conjunction (Logical "and") *) Print and. (* ===> Inductive and (P Q : Prop) : Prop := conj : P -> Q -> (and P Q). *) (** The logical conjunction of propositions [P] and [Q] can be represented using an [Inductive] definition with one constructor. The intuition behind this definition is simple: to construct evidence for [and P Q], we must provide evidence for [P] and evidence for [Q]. More precisely: - [conj p q] can be taken as evidence for [and P Q] if [p] is evidence for [P] and [q] is evidence for [Q]; and - this is the _only_ way to give evidence for [and P Q] -- that is, if someone gives us evidence for [and P Q], we know it must have the form [conj p q], where [p] is evidence for [P] and [q] is evidence for [Q]. Since we'll be using conjunction a lot, let's introduce a more familiar-looking infix notation for it. *) Locate "/\". (* ===> Notation "P /\ Q" := (and P Q) : type_scope. *) (** The [type_scope] annotation tells Coq that this notation will be appearing in propositions, not values. *) (** Consider the "type" of the constructor [conj]: *) Check conj. (* ===> forall P Q : Prop, P -> Q -> P /\ Q *) (** Notice that it takes 4 inputs -- namely the propositions [P] and [Q] and evidence for [P] and [Q] -- and returns as output the evidence of [P /\ Q]. *) (** ** "Introducing" conjunctions *) (** Besides the elegance of building everything up from a tiny foundation, what's nice about defining conjunction this way is that we can prove statements involving conjunction using the tactics that we already know. For example, if the goal statement is a conjuction, we can prove it by applying the single constructor [conj], which (as can be seen from the type of [conj]) solves the current goal and leaves the two parts of the conjunction as subgoals to be proved separately. *) Theorem and_example : (0 = 0) /\ (4 = mult 2 2). Proof. apply conj. - reflexivity. - reflexivity. Qed. (** Just for convenience, we use the tactic [split] as a shorthand for [apply conj]. *) Theorem and_example' : (0 = 0) /\ (4 = mult 2 2). Proof. split. - reflexivity. - reflexivity. Qed. Theorem and_commut : forall P Q : Prop, P /\ Q -> Q /\ P. Proof. intros P Q H. destruct H as [HP HQ]. split. - apply HQ. - apply HP. Qed. (** [destruct] is a tactic to perform case analysis on a term. If we have a term of some type but we don't know what the term actually is, we can use [destruct] to examine all the possible options. It generates subgoals for each possible constructor that could have been used to construct the term. Then we prove the goal for each possibility. *) Print and_commut. (* ###################################################### *) (** * Iff *) (** The handy "if and only if" connective is just the conjunction of two implications. *) (** Definition iff (P Q : Prop) := (P -> Q) /\ (Q -> P). *) Print iff. Locate "<->". (** Notation "P <-> Q" := (iff P Q) (at level 95, no associativity) : type_scope. *) Theorem iff_implies : forall P Q : Prop, (P <-> Q) -> P -> Q. Proof. intros P Q H. destruct H as [HAB HBA]. apply HAB. Qed. (* ############################################################ *) (** * Disjunction (Logical "or") *) Print or. Locate "\/". (** Disjunction ("logical or") can also be defined as an inductive proposition. Inductive or (P Q : Prop) : Prop := | or_introl : P -> or P Q | or_intror : Q -> or P Q. Notation "P \/ Q" := (or P Q) : type_scope. *) (** Consider the "type" of the constructor [or_introl]: *) Check or_introl. (* ===> forall P Q : Prop, P -> P \/ Q *) (** It takes 3 inputs, namely the propositions [P], [Q] and evidence of [P], and returns, as output, the evidence of [P \/ Q]. Next, look at the type of [or_intror]: *) Check or_intror. (* ===> forall P Q : Prop, Q -> P \/ Q *) (** *** *) (** Since [P \/ Q] has two constructors, doing [destruct] on a hypothesis of type [P \/ Q] yields two subgoals. *) Theorem or_commut : forall P Q : Prop, P \/ Q -> Q \/ P. Proof. intros P Q H. destruct H as [HP | HQ]. - apply or_intror. apply HP. - apply or_introl. apply HQ. Qed. Print or_commut. (** From here on, we'll use the shorthand tactics [left] and [right] in place of [apply or_introl] and [apply or_intror]. *) Theorem or_commut' : forall P Q : Prop, P \/ Q -> Q \/ P. Proof. intros P Q H. destruct H as [HP | HQ]. - right. apply HP. - left. apply HQ. Qed. (* ################################################### *) (** * Falsehood *) Print False. (** Logical falsehood can be represented in Coq as an inductively defined proposition with _no constructors_. Inductive False : Prop := . Intuition: [False] is a proposition for which there is no way to give evidence. *) (** Since [False] has no constructors, inverting an assumption of type [False] always yields zero subgoals, allowing us to immediately prove any goal. *) Theorem False_implies_nonsense : False -> 2 + 2 = 5. Proof. intros contra. inversion contra. Qed. (** The [inversion] tactic discovers necessary conditions for a hypothesis to be true. It breaks [contra] into each of its possible cases, and yields a subgoal for each case. As [contra] is evidence for [False], it has _no_ possible cases, hence, there are no possible subgoals and the proof is done. *) (** *** *) (** Conversely, the only way to prove [False] is if there is already something nonsensical or contradictory in the context: *) Theorem nonsense_implies_False : 2 + 2 = 5 -> False. Proof. intros contra. inversion contra. Qed. (** Actually, since the proof of [False_implies_nonsense] doesn't actually have anything to do with the specific nonsensical thing being proved; it can easily be generalized to work for an arbitrary [P]: *) Theorem ex_falso_quodlibet : forall (P:Prop), False -> P. Proof. intros P contra. inversion contra. Qed. Definition False': Prop := forall P: Prop, P. Lemma false_equiv: False <-> False'. Proof. split. - apply ex_falso_quodlibet. (* Apply the lemma we just proved.*) - intro H. unfold False' in H. apply H. Qed. (** The [unfold] tactic replaces a definition with its body. *) Print True. (* ===> Inductive True : Prop := I : True. [True] is a proposition that is trivially true. *) Lemma true_prop: forall P: Prop, P -> True. Proof. intros P HP. apply I. Qed. (** Unlike False, which is used extensively, True is used quite rarely, since it is trivial (and therefore uninteresting) to prove as a goal, and it carries no useful information as a hypothesis. *) (* #################################################### *) (** * Negation *) Print not. (** The logical complement of a proposition [P] is written [not P] or, for shorthand, [~P]: Definition not (P:Prop) := P -> False. The intuition is that, if [P] is not true, then anything at all (even [False]) follows from assuming [P]. *) Locate "~". (* ===> Notation "~ x" := (not x) : type_scope. *) Check not. (* ===> Prop -> Prop *) (** It takes a little practice to get used to working with negation in Coq. Even though you can see perfectly well why something is true, it can be a little hard at first to get things into the right configuration so that Coq can see it! Here are proofs of a few familiar facts about negation to get you warmed up. *) Theorem not_False : ~ False. Proof. unfold not. intros H. inversion H. Qed. (** *** *) Theorem contradiction_implies_anything : forall P Q : Prop, (P /\ ~P) -> Q. Proof. intros P Q H. destruct H as [HP HNA]. unfold not in HNA. apply HNA in HP. inversion HP. Qed. Theorem double_neg : forall P : Prop, P -> ~~P. Proof. intros P H. unfold not. intros G. apply G. apply H. Qed. (** *** Constructive logic *) (** Note that some theorems that are true in classical logic are _not_ provable in Coq's (constructive) logic. E.g., let's look at how this proof gets stuck... *) Theorem classic_double_neg : forall P : Prop, ~~P -> P. Proof. intros P H. unfold not in H. (* But now what? *) Abort. (* ########################################################## *) (** ** Inequality *) Locate "<>". (* ===> Notation "x <> y" := (~ (x = y)) : type_scope. *) (** Saying [x <> y] is just the same as saying [~(x = y)]. *) (** Since inequality involves a negation, it again requires a little practice to be able to work with it fluently. Here is one very useful trick. If you are trying to prove a goal that is nonsensical (e.g., the goal state is [false = true]), apply the lemma [ex_falso_quodlibet] to change the goal to [False]. This makes it easier to use assumptions of the form [~P] that are available in the context -- in particular, assumptions of the form [x<>y]. *) Theorem not_false_then_true : forall b : bool, b <> false -> b = true. Proof. intros b H. destruct b. - reflexivity. - unfold not in H. apply ex_falso_quodlibet. apply H. reflexivity. Qed. Lemma mp: forall P Q: Prop, (P -> Q) -> P -> Q. Proof. intros P Q impl HP. apply impl. exact HP. Qed. Check mp. Print mp. End LOGIC.