Quick Reference for Beginners - coq/coq GitHub Wiki
What follows is an informal guide to a shortlist of Coq features, designed to give new users a starting point. Runs as a standalone Coq file, tested on versions 8.6 and 8.9.1. Originally written in July 2019.
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Lists.List.
(*** Concept/Syntax Reference ***)
(***
This is a quick reference for some foundational Coq syntax and proof tactics. It
is by no means complete -- for a complete reference, see the Coq Reference
Manual (https://coq.inria.fr/distrib/current/refman/index.html).
This reference is organized as follows:
Declarations:
Definition
Fixpoint
Lemma
Theorem
Inductive
Inspection:
Search
Check
Print
Miscellaneous:
nat
match
Propositions:
Prop
forall
exists
and (/\)
or (\/)
implies (->)
not (~)
eq (=)
not-eq (<>)
Proofs:
intros
apply
rewrite
reflexivity
cbv
cbn
induction
lia
nia
replace
***)
(*** Declarations ***)
(* Definition :
A [Definition] declares a term, a type, a proposition, or a non-recursive
function. It looks like:
Definition <name> : <type> := <value>.
It's possible to omit the <type> if Coq can infer it from the value, which
looks like:
Definition <name> := <value>.
For functions, the arguments can go before the colon. That is, saying:
Definition <name> : <type1> -> <type2> -> <type3> := fun <argname> <argname> => <body>
...is equivalent to:
Definition <name> (<argname> : <type1>) : <type2> -> <type3> := fun <argname> => <body>
Definition <name> (<argname> : <type1>) (<argname : <type2>) : <type3> := <body>
*)
Module DefinitionExamples.
(* defining numbers *)
Definition x : nat := 5.
Definition y : Z := 5.
Definition z := 5. (* z is a [nat], because that's the default type of numbers *)
(* defining types *)
Definition two_integers : Type := Z * Z. (* represents a pair of integers *)
(* defining functions *)
Definition add2 : nat -> nat := fun x => x + 2.
Definition make_pair : Z -> Z -> two_integers := fun a b => (a,b).
(* The following are both equivalent to [add2] *)
Definition add2' (x : nat) : nat := x + 2.
Definition add2'' (x : nat) := x + 2. (* return type is inferred *)
(* The following are all equivalent to [make_pair] *)
Definition make_pair' (a : Z) : Z -> two_integers := fun b => (a,b).
Definition make_pair'' (a : Z) (b : Z) : two_integers := (a,b).
Definition make_pair''' (a b : Z) : two_integers := (a,b).
(* defining propositions : see the entry on [Prop] *)
Definition nat_pos : Prop := forall x : nat, 0 <= x.
Definition nat_pos' (x : nat) : Prop := 0 <= x. (* equivalent to [nat_pos] *)
(* This [Prop] is false; you wouldn't be able to prove it, but you can state it. *)
Definition nat_neg : Prop := forall x : nat, x < 0.
End DefinitionExamples.
(* Fixpoint :
[Fixpoint] defines a *recursive* function. Syntax is similar to [Definition]:
Fixpoint <name> : <type> := fun <arguments...> => <body>.
Fixpoint <name> (<argname> : <type>) (argname : <type>) ... : <type> := <body>.
However, it is important to note that Coq does not allow the construction of
functions that might not terminate. So, every time you write a [Fixpoint], you
have to make it very clear to Coq that the function will eventually stop. The
simplest way to do this is to have one of the arguments be a natural number
that decreases every time you call the function. You can also use
other inductive structures like lists as the "decreasing" arguments.
These definitions reference [O] and [S], the two constructors of [nat]. See
the entry on [nat] to understand what [O] and [S] mean in detail; the short
version is that O is zero and S is "successor"; any nat is either equal to
O, or equal to the successor of some other nat.
*)
Module FixpointExamples.
(* loop and decrement n until we reach 0 *)
Fixpoint countdown (n : nat) : nat :=
match n with
| O => n
| S x => countdown x (* "x" is the name I chose for n's predecessor; changing
the name won't break anything *)
end.
(* exponentiation *)
Fixpoint power_of (b : nat) (e : nat) : nat :=
match e with
| O => 1 (* return 1 if e = 0 *)
| S n => b * power_of b n (* if e = n + 1 for some n, return b * b^n with a
recursive call *)
end.
(* You can also recurse on lists, using the list constructors [nil] (an empty
list) and [cons] (which makes a list by adding one element to the head of an
existing list). [Fixpoint] can use any inductive data structure, even one
you've defined yourself, as the decreasing argument (see the entry on
[Inductive]) *)
Fixpoint sum (ls : list nat) : nat :=
match ls with
| nil => 0
| cons x ls' => x + sum ls'
end.
(* Fixpoints don't have to be recursive, technically, but there's no reason
not to use [Definition] in that case. *)
Fixpoint identity (x : nat) : nat := x.
End FixpointExamples.
(* Lemma :
[Lemma] is the most common type of proof declaration. The syntax looks like:
Lemma <name> : <proof statement>.
Proof.
<proof body>
Qed.
You can omit writing [Proof] before your proof, but it's convention, and
visually helps separate the proof from the proof statement when the statement
is long and complicated.
The proof statement usually has type [Prop] (it can also have [Set] or [Type],
if you're trying to prove that a type is non-empty, but this is fairly rare in
practical use afaik).
The proof body consists of "proof-mode" statements that construct a reasoning
for why your proof statement is true. If you finish constructing that
reasoning, you can end your proof with [Qed], which defines your lemma and
makes it available to future proofs just like any fact from the standard library.
If you don't finish your proof but want to exit your lemma, you can't use
[Qed]. Instead, you have two options: [Admitted] and [Abort]. Choosing [Abort]
means that the lemma will not be defined, and won't be visible to or usable by
other proofs. Conversely, [Admitted] will let other proofs see and use your
lemma, even though you haven't yet proven it. Naturally, this means it's
important to remember if you're depending on an admitted lemma, because it
means your top-level proof might not be correct. To see the admitted proofs
a lemma or theorem depends on, type [Print Assumptions <lemma/theorem name>].
*)
Module LemmaExamples.
(* [True] has the type [Prop], so it technically counts as a proof statement *)
Lemma simple : True.
Proof.
trivial. (* in this case, we just tell Coq "this proof is easy" *)
Qed.
Lemma nat_nonneg : forall a : nat, 0 <= a.
Proof.
(* see the [intros] and [lia] entries to understand what these do; for our
purposes here, what's important is that they prove the goal so we can end
with [Qed]. *)
intros. lia.
Qed.
(* same statement as [nat_nonneg], just with the [forall] argument pulled
before the colon *)
Lemma nat_nonneg' (a : nat) : 0 <= a.
Proof.
intros. lia.
Qed.
Lemma nat_nonneg_aborted : forall a : nat, 0 <= a.
Proof.
intros.
(* Qed. *) (* uncomment to see that [Qed] before finishing the proof fails *)
Abort.
(* Uncomment to see that Coq doesn't know about the lemma we [Abort]ed *)
(* Check nat_nonneg_aborted. *)
Lemma nat_nonneg_admitted : forall a : nat, 0 <= a.
Proof.
intros.
(* Qed. *) (* uncomment to see that [Qed] before finishing the proof fails *)
Admitted.
Check nat_nonneg_admitted. (* admitted lemma is visible *)
Lemma use_admitted : 0 <= 5.
Proof.
apply nat_nonneg_admitted. (* lemma is usable even though it's unproven *)
Qed. (* we can still end *this* proof with [Qed] *)
(* However, when we [Print Assumptions], we can see the admitted lemma *)
Print Assumptions use_admitted.
End LemmaExamples.
(* Theorem :
[Theorem] is exactly the same as [Lemma] to Coq. Its only purpose is to signal
to humans that a particular proof is more important than the ones marked
[Lemma].
Other synonyms include [Remark], [Fact], [Corollary], and [Proposition]. In my
own work, I use almost exclusively [Lemma] and only occasionally [Theorem] to
mark particularly important top-level proofs. Ultimately, though, this comes
down to individual style. *)
Module TheoremExamples.
(* see Lemma examples *)
End TheoremExamples.
(* Inductive :
Proofs by induction are an extremely powerful tool in mathematical proofs;
[Inductive] is Coq's built-in machinery for inductive reasoning. Its syntax
looks like:
Inductive <name> [<arguments>] : <type> :=
| <constructor>
| <constructor>
| <constructor>
...
| <constructor>
.
The first example of an inductive is the [nat] type of natural
numbers. If you [Print nat], you'll see the definition of the type,
which looks like this:
Inductive nat : Set :=
| O : nat
| S : nat -> nat
.
This means that you can make a natural number in two ways. The first way is
to make zero (with the constructor [O]). The second way is to add one to an
existing natural number, creating that number's "successor", using the [S]
constructor. Because [S] requires a [nat] to create a [nat], its type is
[nat -> nat]. Natural numbers are defined as everything that can be created
by some combination of these two constructors. And whenever you have a natural
number in context, you can use a [match] to split into the two cases -- either
you have zero, or you have the successor of another number.
An [Inductive] defines a [Set], [Prop], or [Type]. That means you can have
inductive datatypes using [Type] (like [nat] or [list] from the standard
library), and also inductive proof statements. For instance, if you're proving
something about a state machine, you might want a proof statement that says
"this state is reachable". Using an [Inductive], you can define "reachable" by
saying "it's either equal to the initial state (base case) or it's one state
transition away from another reachable state".
*)
Module InductiveExamples.
(* inductive type of binary trees; this says essentially that a binary tree can
either be a leaf, or can be constructed from two existing binary trees (the
left and right children. *)
Inductive tree : Type :=
| Leaf : tree
| Parent : tree -> tree -> tree
.
(* Now, we can use the constructors of [tree] *)
Check Parent.
(* This tree looks like:
x
/ \
x x
/ \
x x
*)
Definition small_tree : tree :=
Parent (Parent Leaf Leaf) Leaf.
(* we can also split into cases when we write functions about trees *)
Definition is_leaf (t : tree) : bool :=
match t with
| Leaf => true
| Parent x y => false
end.
(* ...and we can use a [tree] as the decreasing argument of a [Fixpoint] *)
Fixpoint depth (t : tree) : nat :=
match t with
| Leaf => 0
| Parent l r => S (max (depth l) (depth r))
end.
(* Most importantly, we can use [induction] in proofs -- see the entry on
[induction] for more examples. This proof states that for all trees t,
either t has a depth greater than zero or t is a leaf. *)
Lemma depth_positive :
forall t : tree, 0 < depth t \/ is_leaf t = true.
Proof.
induction t.
(* now we have two cases : one in which t is a leaf, and one in which t is
a parent; we'll use curly braces to separate the proof of each case. *)
{ (* subgoal 1 : t is a leaf *)
cbv [depth is_leaf]. (* inline the definitions of [depth] and [is_leaf];
the [match] statements are automatically simplified
away *)
right. (* the left side of the "or" is clearly false, so we confine
ourselves to proving the right-hand side *)
reflexivity. (* [reflexivity] can easily prove that [true = true] *)
}
{ (* subgoal 2 : t is a parent *)
(* notice that two inductive hypotheses have appeared, stating that, for
both child trees, our proof statement holds *)
cbn [depth is_leaf]. (* inline again -- use [cbn] instead of [cbv] to avoid
inlining the recursive calls in [depth] *)
left. (* now, the right hand side of the "or" is clearly false, so we
confine ourselves to the left *)
lia. (* the successor of a nat is always < 0; we don't even have to use the
inductive hypotheses. *)
}
Qed.
(* [Inductive]s, like [Fixpoints], are typically recursive but don't have to
be. You can also use them like enums, if you want to simply define a type
that has a fixed set of constructors. *)
Inductive color_enum : Type :=
| RED : color_enum
| GREEN : color_enum
| BLUE : color_enum
.
(* ..then, just like before, you can easily split into cases *)
Definition is_blue (x : color_enum) : bool :=
match x with
| BLUE => true
| RED => false
| GREEN => false
end.
(* You *can* construct inductive types with no base cases, but it will be
impossible to construct anything of that type, so it's not very useful. *)
Inductive silly_thing : Type :=
| SillyConstructor : silly_thing -> silly_thing
.
(* [Inductive]s can also define [Prop]s, not just datatypes. This [Inductive]
states that a number is even if and only if either it's zero, or it's two
plus an even number. *)
Inductive is_even : nat -> Prop :=
| zero_is_even : is_even 0
| plus_two_is_even : forall n : nat, is_even n -> is_even (n + 2)
.
End InductiveExamples.
(*** Inspection ***)
(* Search :
One of the most useful tactics for discovering lemmas or functions that have
already been defined is [Search]. The syntax is simple:
Search <expression>.
When you process the statement, Coq will print out every function, definition,
lemma, or anything else in which the expression you entered is part of its
type signature/proof statement. That is, writing [Search Nat.mul] will show
you every lemma that says anything at all about the multiplication of natural
numbers in its proof statement. [Search nat] will give you every function
that operates on or returns natural numbers, every natural number that has
been defined already, and every lemma that says anything about [nat]s.
What constitutes an "expression" for [Search] is very flexible, as you
will see in the examples.
*)
Module SearchExamples.
(* simple statements : you can search about functions or about already-defined
terms like 2, or even expressions like (1+1). *)
Search Nat.mul.
Search Nat.log2.
Search 2.
Search (1 + 1).
(* You can also [Search] for things containing multiple expressions *)
Search Nat.mul Nat.sub.
Search Nat.mul Nat.sub 0.
(* We can also [Search] types, like [nat] and [list], to get every function or
definition with that type as a subset of its type signature, and every lemma
that has the type in its proof statement. *)
Search nat.
Search list.
Search (list nat). (* look for lemmas/functions about lists of natural numbers *)
Search (nat -> nat -> bool). (* look for functions that take in two natural
numbers and return a boolean *)
(* Extremely usefully, [Search] allows you to leave "blanks" in expressions
using underscores. *)
Search (_ * 1). (* find anything times 1 *)
Search (Nat.log2 _ = 0). (* find any lemma that says something about a [nat]
whose [log2] is 0 *)
(* You can also use [?] to define variables, which lets you repeat them within
the expression to narrow down your search. *)
Search (?x * 1). (* same as [Search (_ + 1)], since x not repeated *)
Search (?x * ?x).
Search (?x * _ <= ?x * _).
(* you can attach scope delimiters to [Search] expressions, which means that in
this [Search] the [1] and [*] are interpreted as the *integer* 1 and the
function [Z.mul] (integer multiplication), instead of the *natural number* 1
and the function [Nat.mul] (natural number multiplication). *)
Search (_ * 1)%Z.
(* You can also search for things you define yourself. *)
Definition x : nat := 5.
Search x. (* returns nothing because there are no lemmas about [x]; [x]
will not show up in its own [Search] because its *type*,
[nat], says nothing about [x]. *)
Search nat. (* However, [x] does show up when we [Search nat] *)
Lemma x_pos : 0 < x.
Proof.
cbv [x]. lia.
Qed.
Search x. (* now, we can see the lemma we just defined *)
End SearchExamples.
(* Check :
[Check] is a useful tool for looking at the types of lemmas, functions, etc.
The syntax is very similar to [Search] :
Check <expression>.
Coq will then print the name and type of the expression. This is most useful
for proofs, whose "types" are their proof statements.
*)
Module CheckExamples.
(* look at the types of functions or pre-defined terms like [2] *)
Check Nat.mul.
Check 2.
Check nat. (* the [nat] type is technically a [Set] (the difference between
[Set] and [Type] is rarely relevant; feel free to think of them
as synonyms) *)
Check list. (* the [list] type requires you to specify what type the list
elements are, so [list] has type [Type -> Type] *)
Check Type. (* [Type] has type [Type], in case you were curious *)
(* [Check] is most often used to look at proof statements, like so *)
Check Nat.log2_nonneg.
Check Nat.mul_le_mono_l.
(* you can even feed the proofs arguments to see what the proof statement
looks like partially filled in *)
Check (Nat.mul_le_mono_l 1 2 3).
Check (Nat.mul_le_mono_l 1 2).
Check (Nat.mul_le_mono_l _ _ 3).
(* [Check] works on things you define yourself *)
Definition x : nat := 5.
Check x.
(* [Check], like [Search], accepts scope delimiters. *)
Check 2%Z.
End CheckExamples.
(* Print :
While [Search] and [Check] show only the *types* of the things you search for,
[Print] shows you the actual values. The syntax is very similar to [Search]
and [Check]:
Print <expression>.
However, [Print] is more restrained in the kinds of expressions it accepts. In
particular, [Print] only accepts what's referred to in the Coq manual as
"qualid"s or "qualifier IDs" -- that means the *names* of functions, lemmas,
definitions, types, etc. Unlike [Search], you can't [Print] a partially-filled
expression like [(_ + 1)]; unlike [Check], you can't [Print] lemmas with
arguments filled in like [(Nat.mul_le_mono_l 1)]. You can only use names, by
themselves -- like [Print Nat.add] or [Print Nat.mul_le_mono_l].
*)
Module PrintExamples.
(* [Print]ing functions shows you the function definitions *)
Print Nat.mul.
(* You can also see the definitions of inductive types, which can be useful *)
Print nat.
Print list.
(* [Print]ing an inductive constructor shows you the whole [Inductive] *)
Print O.
Print cons.
(* printing lemmas is not usually useful, as you will see the raw form of the
proof and it might be very large *)
Print Nat.log2_nonneg.
End PrintExamples.
(*** Miscellaneous ***)
(* nat :
One of the most frequently used and most basic types in Coq, [nat] is the type
of natural numbers (0 and above).
The definition of [nat] (as shown by [Print nat]) is:
Inductive nat : Set :=
| O : nat
| S : nat -> nat
.
See the entry on [Inductive] for more detail about what this means exactly.
But the gist is that you can construct a [nat] one of two ways: 1) by using
the "O" constructor, which takes no arguments and represents zero, and 2) by
using the "S" constructor, which takes another [nat] as an argument and
represents the "successor" of the input (input + 1). In this format, 3 is
represented by [S (S (S O))], 1 is represented by [S O], and so on.
The Coq standard library contains many proofs about [nat], which can be found
using [Search]. It further contains definitions of arithmetic operations like
addition (Nat.add or +), multiplication (Nat.mul or * ), square root
(Nat.sqrt), maximum/minimum (Nat.max/Nat.min), and even bitwise operations
(Nat.lor, Nat.land, Nat.lxor, Nat.lnot). There are also definitions for
comparison operations like < (Nat.lt), <= (Nat.le), > (Nat.gt), and
>= (Nat.ge).
*)
Module NatExamples.
(* Define a term with type [nat] *)
Definition x : nat := 5.
(* we can split natural numbers into their two cases -- zero or successor *)
Definition is_nonzero (n : nat) : bool :=
match n with
| O => false
| S m => true
end.
(* an example lemma about natural numbers using comparison operators; states
that if a [nat] is greater than zero and you add another [nat] to it, the
result will also be greater than zero. *)
Lemma sum_positive :
forall n m : nat, 0 < n -> 0 < n + m.
Proof.
intros.
lia. (* [lia] is the "linear arithmetic" tactic, and solves this one easily *)
Qed.
(* It's important to keep in mind that [nat] is very inefficient when composing
large numbers. For anything where you're computing large numbers directly,
use Z or N, which are based on binary formats and scale much better. *)
Definition n : nat := 1000.
(* Uncomment to see what your system does -- mine stack overflows *)
(* Eval compute in (n * n). *)
Definition z : Z := 1000.
Eval compute in (z * z)%Z. (* just fine! *)
Eval compute in (z * z * z * z * z * z)%Z. (* still fine *)
(* Uncomment to see that at some point [Z] does get slow, but still no stack
overflow *)
(* Eval compute in (z ^ 500)%Z. *)
(* Most other entries in this reference have natural numbers in their examples,
too, so if you'd like more just look around! *)
End NatExamples.
(* match :
When you have an inductive datatype, you can split into cases based on its
constructors using [match]. The syntax is:
match <name> with
| <constructor> => <expression>
| <constructor> => <expression>
...
| <constructor> => <expression>
end.
This isn't unlike a [switch] or [case] statement in other programming
languages. Cases can be listed in any order.
You must put some expression for all cases. If you want a "default" behavior
that applies to many different cases, you can use an underscore to match "any
case not listed above". Therefore, for a [nat] called x, writing:
match x with
| O => true
| S _ => false
end
...is completely equivalent to both of the following:
match x with
| O => true
| _ => false
end
match x with
| S _ => false
| _ => true
end
Note: there's also a [match] you can use in proof-mode with similar syntax,
but it's not exactly the same thing.
*)
Module MatchExamples.
(* basic match -- two cases of nat constructors *)
Definition minus1 (n : nat) : nat :=
match n with
| O => 0 (* 0 - 1 = 0 with natural numbers, since they can't go negative *)
| S m => m
end.
(* If a constructor takes an argument, you can name the argument whatever you
want. The following is completely equivalent to [minus1]. *)
Definition minus1' (n : nat) : nat :=
match n with
| O => 0
| S what_a_long_name123 => what_a_long_name123
end.
(* If you're ignoring the argument(s) a constructor takes, you can put _ *)
Definition is_nonzero (n : nat) : bool :=
match n with
| O => false
| S _ => true
end.
(* you can match multiple things at once *)
Definition both_nonzero (n m : nat) : bool :=
match n, m with
| O, O => false
| O, S _ => false
| S _, O => false
| S _, S _ => true
end.
(* equivalent to both_nonzero; using an underscore to signify "any case not
listed above" *)
Definition both_nonzero' (n m : nat) : bool :=
match n, m with
| S _, S _ => true
| _, _ => false
end.
(* You can also match expressions *)
Definition sum_nonzero (n m : nat) : bool :=
match n + m with
| O => false
| S _ => true
end.
(* You can put matches in lemma statements, if you really want to, but it's
a little hard to read. This lemma says "if x and y are both zero, their sum
is zero; otherwise, their sum is greater than zero". *)
Lemma sum_zero_or_positive :
forall x y : nat,
match x, y with
| O, O => 0 = x + y
| _, _ => 0 < x + y
end.
Proof.
destruct x, y; lia.
Qed.
End MatchExamples.
(*** Propositions ***)
(* Prop :
The type of proof statements in Coq is called [Prop]. You can use it like any
other type, from making definitions with that type to writing functions that
take [Prop] as input. But it's more analogous to the type [Type] than it is
to a type like [nat].
Some extra notes for the curious:
When you define something with type [Prop], the proof statement you have
written can function a lot like a type. There can be many different ways to
prove the same statement, and you can think of these as many different members
of the type, much like there are many ways to construct a natural number, but
they all have the same type. You might even write a false [Prop], for which
there exist no proofs; this would be equivalent to a type with no members.
In this framework, writing a proof in Coq is essentially like writing a
function. This is called the Curry-Howard correspondence and is really cool if
you want to read further about it.
*)
Module PropExamples.
(* The two most basic [Prop]s are [True] and [False] *)
Check True.
Check False.
Print True. (* [True] has one constructor with no arguments; it can always be
constructed without input *)
Print False. (* [False] is an inductive with no constructors; it can never be
constructed *)
(* simple example: equality and comparison operations output [Prop] *)
Definition one_lt_2 : Prop := 1 < 2.
Definition one_eq_2 : Prop := 1 = 2. (* [Prop]s can be false! *)
(* You can take arguments when defining a [Prop] *)
Definition x_lt_2 : nat -> Prop := fun x => x < 2.
(* You can construct new [Prop]s from ones you've already defined *)
Definition x_le_2 : nat -> Prop := fun x => x_lt_2 x \/ x = 2.
(* A good example of using [Prop] is [In], a function that takes in an element
and a list and outputs a [Prop] saying the element is in the list. You can
see it with [Print In], but I'll also write it out here. *)
Fixpoint In' (A : Type) (a : A) (ls : list A) :=
match ls with
| nil => False
| cons b ls' => b = a \/ In' A a ls' (* a is equal to the first element, or
is in the remainder of the list *)
end.
(* We can see the full [Prop] provided by [In'] by plugging in a list *)
Eval compute in (fun x => In' nat x (cons 3 (cons 2 nil))).
(* We can also prove a statement in terms of [In'] *)
Lemma two_in_list : In' nat 2 (cons 3 (cons 2 nil)).
Proof.
cbv [In'].
auto.
Qed.
(* See the following entries for examples of the syntax used to construct
[Prop]s *)
End PropExamples.
(* forall :
The [forall] quantifier is exactly the same as a [forall] in mathematics, and
is used the same way when writing [Prop]s. The syntax looks like:
forall (<name> : <type>), <statement in terms of name>
*)
Module ForallExamples.
(* To showcase the various different ways of writing arguments to [forall],
here are several definitions that are all completely equivalent. *)
Definition nat_lt : Prop :=
forall (x : nat) (y : nat), x < y.
Definition nat_lt' : Prop :=
forall (x : nat), forall (y : nat), x < y.
Definition nat_lt'' : Prop :=
forall (x y : nat), x < y.
Definition nat_lt''' : Prop :=
forall x y, x < y. (* Coq knows that < is short for [Nat.lt], so x and y
must be [nat]s *)
Definition nat_lt'''' : Prop :=
forall x, forall y, x < y.
Definition nat_lt''''' : Prop :=
forall (x : nat) y, x < y.
(* You can also use [forall] for things with type [Prop], but it's usually
more readable to use [implies] *)
Definition lt_transitive : Prop :=
forall a b c (Hab : a < b) (Hbc : b < c),
a < c.
(* more readable version of [lt_transitive] *)
Definition lt_transitive' : Prop :=
forall a b c,
a < b ->
b < c ->
a < c.
End ForallExamples.
(* exists :
The [exists] quantifier works basically the same way as [forall], with the
same syntax and the meaning you would expect from a mathematical [exists].
Note: in proof mode, there is also a tactic called [exists], but it is a
different thing than the one used in defining [Prop]s.
*)
Module ExistsExamples.
Lemma exists_pos : exists x : nat, 0 < x.
Proof.
exists 1. (* here's that [exists] tactic; it takes a goal with an [exists]
on the outside and plugs in a specific member of the requested
type *)
lia.
Qed.
End ExistsExamples.
(* and (/\):
The [and] function takes two [Prop]s and creates another [Prop], representing
the conjunction of the two.
[and] is represented by the notation "/\".
It is defined as an inductive [Prop], with the single constructor [conj]. As
[Print and] will show:
Inductive and (A B : Prop) : Prop :=
| conj : A -> B -> A /\ B
.
*)
Module AndExamples.
(* states that a [nat] is in the range [low...high) *)
Definition in_range (low high : nat) : nat -> Prop :=
fun x => x < high /\ low <= x.
(* equivalent to [in_range], just not using the [/\] notation *)
Definition in_range' (low high : nat) : nat -> Prop :=
fun x => and (x < high) (low <= x).
Print in_range'. (* printing shows you the notation again *)
(* proof using [and]s; states that we can expand the range and know that it
still holds everything that was in the original range *)
Lemma loosen_range :
forall low high new_low new_high,
high <= new_high ->
new_low <= low ->
forall x,
in_range low high x ->
in_range new_low new_high x.
Proof.
cbv [in_range]. (* inline the definition of [in_range] *)
intros.
destruct H1. (* use [destruct] to separate an [and] in a hypothesis *)
split. (* use [split] to separate an [and] in a goal *)
{ lia. }
{ lia. }
Qed.
End AndExamples.
(* or (\/):
The [or] function is very analogous to [and], and is represented by the
notation "\/".
[or] is defined as an inductive [Prop] with two constructors: [or_introl] and
[or_intror]. These say that you can construct an [or] with a proof of either
the left side or the right side, respectively, which makes good sense. The
definition is:
Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
.
*)
Module OrExamples.
(* states that a [nat] is *outside* the range [low...high) *)
Definition out_of_range (low high : nat) : nat -> Prop :=
fun x => high <= x \/ x < low.
(* equivalent to [out_of_range], just without using the [\/] notation *)
Definition out_of_range' (low high : nat) : nat -> Prop :=
fun x => or (high <= x) (x < low).
Print out_of_range'. (* printing shows you the notation again *)
(* proof using [or]s; states that we can narrow the range and know that
everything that was outside the range is still outside it *)
Lemma tighten_range :
forall low high new_low new_high,
new_high <= high ->
low <= new_low ->
forall x,
out_of_range low high x ->
out_of_range new_low new_high x.
Proof.
cbv [out_of_range]. (* inline the definition of [out_of_range] *)
intros.
destruct H1. (* use [destruct] to separate an [or] in a hypothesis; this
will give you two subgoals *)
{ left. (* use [left] to prove an [or] by proving the left side *)
lia. }
{ right. (* use [right] to prove an [or] by proving the right side *)
lia. }
Qed.
End OrExamples.
(* implies (->) :
The [implies] function is represented by an arrow [->] and states that a
particular [Prop] implies another. It's used very frequently to add
preconditions to lemma statements.
*)
Module ImpliesExamples.
(* simple example: if n < m, then n <= m *)
Definition lt_le_incl : Prop :=
forall n m : nat, n < m -> n <= m.
(* chain multiple [implies] for multiple preconditions *)
Definition lt_transitive : Prop :=
forall a b c, a < b -> b < c -> a < c.
(* These statements are completely equivalent to each other and to
[lt_transitive]. *)
Definition lt_transitive' : Prop :=
forall a b c,
a < b ->
b < c ->
a < c.
Definition lt_transitive'' : Prop :=
forall a b c,
a < b
-> b < c
-> a < c.
Definition lt_transitive''' : Prop :=
forall a b c,
a < b -> b < c ->
a < c.
(* Using [and] works, but is annoying in proofs because then you have to
[destruct] hypotheses with [and] and [split] goals with [and], all over the
place. Chaining [implies] is recommended instead. *)
Definition lt_transitive'''' : Prop :=
forall a b c,
(a < b /\ b < c) -> (* not recommended *)
a < c.
End ImpliesExamples.
(* not (~):
The [not] function, represented by [~], actually has a very simple definition.
[Print not] will show you:
fun A : Prop => A -> False
Because we have the unconstructable [Prop], [False], saying a [Prop] is not
true is equivalent to saying that if it was true, then it would imply [False].
*)
Module NotExamples.
(* simple example of a [Prop] using [not] *)
Definition not_lt (a b : nat) : Prop :=
~ (a < b).
(* using [not] in preconditions *)
Definition not_lt_ge : Prop :=
forall a b,
~ (a < b) ->
a >= b.
(* proving a goal with [not] *)
Lemma ge_not_lt :
forall a b,
a >= b ->
~ (a < b).
Proof.
intros.
(* If you read the definition of [not], you'll see that what our goal really
says now is (a < b) -> False. [intros] won't pick it up, but if you use
the variant [intro] Coq will know you mean business and actually show you
the structure. *)
intro. (* now our goal says [False]! We have to prove that the hypotheses
contradict. *)
lia. (* luckily, [lia] is pretty smart. *)
Qed.
End NotExamples.
(* eq (=):
The default equality relation in Coq is [eq], represented by [=]. It is
defined as an inductive [Prop] with one constructor, [eq_refl]:
Inductive eq {A : Type} (x : A) : A -> Prop :=
| eq_refl : eq x x
.
(Note that A, the type of x, is "implicit"; Coq will infer what A is from x,
so you can use [eq] or [eq_refl] without writing the type.)
This definition says that for any type A, and any element x of that type, x
is equal to itself. So, to prove equality, you must have exactly the same
thing on either side of the [=] sign.
Extra notes for the curious:
This notion of equality produces some problems for the equivalence of
functions; even if two functions always produce the same output for every
possible input, if they are constructed differently they will not be equal
in this definition of [eq]. Assuming they can be swapped freely for each
other is called functional extensionality, and exists only as an axiom that I
do not recommend using. Instead, specifically prove in each place you need it
that swapping out a function argument for an equivalent function produces the
same result. It's annoying, but it's logically consistent. For an example of
this kind of proof, look at [map_ext] from the list library, which says that
you can swap out the functional argument of [map] for an equivalent function
without changing the result. (It's convention to give this kind of lemma a
name ending in "_ext" for "extensionality".)
The default equality used in Coq is Leibniz equality, in theoretical-math
terms. It's possible to create your own notions of equivalence in Coq, but
that is beyond the scope of this reference; if that's what you're looking to
do you should examine [RelationClasses.Equivalence]. To use [rewrite] with
custom equivalence relations, look at [Proper] and [setoid_rewrite] as well.
*)
Module EqExamples.
(* simple [Prop] using [eq] *)
Definition simple_eq : Prop := 1 = 2.
(* equivalent to [simple_eq], just not using the [=] notation *)
Definition simple_eq' : Prop := eq 1 2.
Print simple_eq'. (* notation shows up again when printed *)
(* [Prop] with equality on lists of [nat]s *)
Definition cons_hd_tl_nat : Prop :=
forall ls : list nat,
ls <> nil ->
cons (hd 0 ls) (tl ls) = ls.
(* [Prop] with equality on lists with unspecified element types *)
Definition cons_hd_tl : Prop :=
forall (A : Type) (ls : list A) (a : A),
ls <> nil ->
cons (hd a ls) (tl ls) = ls.
End EqExamples.
(* not-eq (<>) :
When you write something in Coq of the form [~ (x = y)], this gets shortened
into the notation [<>], meaning "not equal".
Since most of this is covered by the [eq] and [not] entries, this entry is
rather short; look at [eq] and [not] for further understanding.
*)
Module NotEqExamples.
(* using <> to state a simple [Prop] *)
Definition one_neq_2 : Prop := 1 <> 2.
(* using <> to state a precondition *)
Definition nonzero_pos : Prop :=
forall n : nat,
n <> 0 ->
0 < n.
End NotEqExamples.
(*** Proof mode ***)
(* intros :
The [intros] tactic is frequently run at the beginning of proofs and separates
the proof state into the things you already know (above the ===== line) and
the things you're trying to prove (below the ==== line).
It works both on [forall] arguments and on the first arguments to [implies];
that is, if your goal says something like:
forall x y, x < y -> x <= y
...then the things you "know", which [intros] will move above the line, are:
- x and y exist and are natural numbers
- x < y
Sometimes, particularly when using the [induction] tactic, it's important to
leave [forall]s intact, so resist the temptation to run [intros] automatically
on inductive proofs. See the entry on [induction] for details. *)
Module IntrosExamples.
(* [intros] pulls [forall] arguments into the "known" section *)
Lemma simple_intros : forall a : nat, 0 <= a.
Proof.
(*
============================
forall a : nat, 0 <= a *)
intros.
(* a : nat
============================
0 <= a *)
Abort.
(* if you put the argument before the colon, it's already "introduced" *)
Lemma intros_unneeded (a : nat) : 0 <= a.
Proof.
(* a : nat
============================
0 <= a *)
intros. (* no-op *)
Abort.
(* [intros] also pulls preconditions into the "known" section *)
Lemma intros_precondition : forall a : nat, a <> 0 -> 0 < a.
Proof.
(*
============================
forall a : nat, a <> 0 -> 0 <= a *)
intros.
(* a : nat
H : a <> 0
============================
0 <= a *)
Abort.
(* [intros] works if you don't have a [forall] as well *)
Lemma intros_precondition' : 1 <> 0 -> 0 < 1.
Proof.
(*
============================
1 <> 0 -> 0 < 1 *)
intros.
(* H : 1 <> 0
============================
0 < 1 *)
Abort.
(* [intros] can optionally rename your arguments/preconditions *)
Lemma intros_names : forall a : nat, a <> 0 -> 0 < a.
Proof.
(*
============================
forall a : nat, a <> 0 -> 0 <= a *)
intros x y.
(* x : nat
y : x <> 0
============================
0 <= x *)
Abort.
(* Leaving a [?] when providing names tells [intros] to name that argument
however it wants *)
Lemma intros_names : forall a : nat, a <> 0 -> 0 < a.
Proof.
(*
============================
forall a : nat, a <> 0 -> 0 <= a *)
intros x ?.
(* x : nat
H : x <> 0
============================
0 <= x *)
Abort.
End IntrosExamples.
(* apply :
The [apply] tactic is the simplest way to use a lemma or known hypothesis in
proof-mode. The basic syntax is:
apply <lemma name>.
If the lemma or hypothesis exactly matches the goal, then this step completes
the proof. If the lemma has preconditions, you'll be left with having to prove
them.
*)
Module ApplyExamples.
(* use [apply] to prove a goal using a hypothesis *)
Lemma simple_apply_hypothesis :
forall n : nat,
0 < n ->
0 < n.
Proof.
intros.
(* n : nat
H : 0 < n
============================
0 < n *)
apply H.
Qed.
(* use [apply] to prove a goal using a hypothesis with preconditions *)
Lemma apply_hypothesis_precondition :
(forall m, m <> 0 -> 0 < m) ->
0 < 5.
Proof.
intros.
(* H : forall m : nat, m <> 0 -> 0 < m
============================
0 < 5 *)
apply H.
(* H : forall m : nat, m <> 0 -> 0 < m
============================
5 <> 0 *)
lia.
Qed.
(* use an existing lemma about the distributive property of [mul] to prove
a simple arithmetic statement *)
Lemma mul_distributive :
forall n m : nat,
n * (m + n) = n * m + n * n.
Proof.
intros.
(* n, m : nat
============================
n * (m + n) = n * m + n * n *)
apply Nat.mul_add_distr_l.
Qed.
(* You can pass arguments to lemmas in [apply]. Look at the entries for [Check]
and [Search] to find out about inspecting lemmas to see which arguments are
which. *)
Lemma gt_5_implies_gt_3 :
forall a : nat,
5 < a ->
3 < a.
Proof.
intros.
(* a : nat
H : 5 < a
============================
3 < a *)
(* just plain [apply Nat.lt_trans] will fail, because the goal only mentions
[3] and [a] ("n" and "p" respectively in the lemma statement); Coq doesn't
know what to plug in for the variable "m" in the lemma statement (it
should be 5). *)
Check Nat.lt_trans. (* look at the lemma statement *)
Fail apply Nat.lt_trans. (* error message: "Unable to find an instance for
the variable m." *)
(* however, if we pass in all the arguments explicitly, it works fine *)
apply (Nat.lt_trans 3 5 a).
(* other options that would work the exact same way:
apply (Nat.lt_trans _ 5 _).
apply Nat.lt_trans with (m := 5).
*)
(* a : nat
H : 5 < a
============================
3 < 5
subgoal 2 (ID 14) is:
5 < a *)
{ (* subgoal 1 : 3 < 5 *)
lia. }
{ (* subgoal 2 : 5 < a *)
apply H. }
Qed.
End ApplyExamples.
(* rewrite :
The [rewrite] tactic is another essential one in Coq, and the other main way
of using already-proven lemmas or hypotheses in proofs. The basic syntax is:
rewrite <lemma name>.
[rewrite] works with proof statements of the form [a = b] and expressions that
mention something about [a]; if you know [a = b], you can restate your goal or
hypothesis in terms of [b]. If the lemma or hypothesis you [rewrite] with has
preconditions, these will appear as new subgoals.
*)
Module RewriteExamples.
(* use lemmas from the standard library to change the goal *)
Lemma simple_rewrite :
forall n,
n + 0 = 0 + n.
Proof.
intros.
(* n : nat
============================
n + 0 = 0 + n *)
rewrite Nat.add_0_r.
(* n : nat
============================
n = 0 + n *)
rewrite Nat.add_0_l.
(* n : nat
============================
n = n *)
reflexivity.
Qed.
(* use known hypotheses to change the goal *)
Lemma rewrite_with_hypothesis :
forall n m p,
n + m = 1 + p ->
(n + m) ^ 4 = (1 + p) ^ 4.
Proof.
intros.
(* n, m, p : nat
H : n + m = 1 + p
============================
(n + m) ^ 4 = (1 + p) ^ 4 *)
rewrite H.
(* n, m, p : nat
H : n + m = 1 + p
============================
(1 + p) ^ 4 = (1 + p) ^ 4 *)
reflexivity.
Qed.
(* with [<-], you can rewrite "backwards" *)
Lemma rewrite_with_hypothesis' :
forall n m p,
n + m = 1 + p ->
(n + m) ^ 4 = (1 + p) ^ 4.
Proof.
intros.
(* n, m, p : nat
H : n + m = 1 + p
============================
(n + m) ^ 4 = (1 + p) ^ 4 *)
rewrite <-H.
(* n, m, p : nat
H : n + m = 1 + p
============================
(n + m) ^ 4 = (n + m) ^ 4 *)
reflexivity.
Qed.
(* you can also [rewrite] in a hypothesis *)
Lemma rewrite_in_hypothesis :
forall n m,
n + 0 = m ->
n = m.
Proof.
intros.
(* n, m : nat
H : n + 0 = m
============================
n = m *)
rewrite Nat.add_0_r in H.
(* n, m : nat
H : n = m
============================
n = m *)
apply H.
Qed.
(* If you [rewrite] with a lemma that has preconditions, they will show up as
new subgoals. *)
Lemma rewrite_with_preconditions :
forall n,
n * 3 = 0 ->
n * 5 = 0.
Proof.
intros.
(* n : nat
H : n * 3 = 0
============================
n * 5 = 0 *)
rewrite (Nat.mul_eq_0_l n 3).
(* n : nat
H : n * 3 = 0
============================
0 * 5 = 0
subgoal 2 (ID 37) is:
n * 3 = 0
subgoal 3 (ID 38) is:
3 <> 0 *)
{ lia. }
{ lia. }
{ lia. }
Qed.
(* Writing [rewrite <lemma> by <tactic>] lets you rewrite if and only if all
the preconditions can be solved by <tactic>. *)
Lemma rewrite_by :
forall n,
n * 3 = 0 ->
n * 5 = 0.
Proof.
intros.
(* n : nat
H : n * 3 = 0
============================
n * 5 = 0 *)
rewrite (Nat.mul_eq_0_l n 3) by lia.
(* n : nat
H : n * 3 = 0
============================
0 * 5 = 0 *)
(* No new subgoals this time *)
lia.
Qed.
(* Like [apply], you can pass arguments to [rewrite]; this is useful if you
have multiple places that could be transformed by the same lemma and want
to specify which one you mean. *)
Lemma rewrite_with_arguments :
forall n m p,
p + m = n ->
n + n = m + p + n.
Proof.
intros.
(* n, m, p : nat
H : p + m = n
============================
n + n = m + p + n *)
(* Now, we want to [rewrite] with [Nat.add_comm] to switch the order of [p]
and [m] so we can use H. But when we try, Coq will attempt to change the
order of the first [Nat.add] it sees -- [n + n]. That fails, because it
doesn't change the goal at all. *)
Fail rewrite Nat.add_comm. (* error : "Tactic generated a subgoal identical
to the original goal" *)
(* if we specify the arguments to [Nat.add_comm], it works *)
rewrite (Nat.add_comm m p).
(* n, m, p : nat
H : p + m = n
============================
n + n = p + m + n *)
rewrite H.
reflexivity.
Qed.
End RewriteExamples.
(* reflexivity :
The [reflexivity] tactic is simple but powerful. Basically, you tell Coq "I'm
pretty sure both things on the side of this [eq] are the same" and Coq then
simplifies them until either they can't be simplified further or they're equal.
[reflexivity] takes no arguments.
[reflexivity] also works on other relations that are known to Coq to be
reflexive, like [<=].
Performance note : If [reflexivity] is very slow, Coq is probably simplifying
something it shouldn't be simplifying, and you should try transforming your
goal some more to get rid of any subterms that are huge when simplified, such
as a non-opaque proof or a term with a ton of [let]s in it.
*)
Module ReflexivityExamples.
(* if the two sides of the [eq] are precisely equal, call [reflexivity]! *)
Lemma basic_reflexivity :
5 = 5.
Proof.
reflexivity.
Qed.
(* also works on other reflexive relations like [<=] *)
Lemma reflexivity_le :
5 <= 5.
Proof.
reflexivity.
Qed.
(* [reflexivity] works even if it has to inline definitions for the two sides
to be equal *)
Definition x : nat := 5.
Lemma reflexivity_inlines :
x = 5.
Proof.
reflexivity.
Qed.
(* in this case, [reflexivity] inlines [Nat.add] *)
Lemma reflexivity_inlines' :
3 + 2 = 5.
Proof.
reflexivity.
Qed.
(* However, [reflexivity] knows nothing about math, and won't understand
anything in terms of variables unless the variables are in exactly the same
places on either side of the [eq]. *)
Lemma reflexivity_bad_at_math :
forall n m : nat,
n + m = m + n.
Proof.
Fail reflexivity. (* error : "Unable to unify 'm + n' with 'n + m'." *)
Abort.
(* Sometimes, if you're lucky, your expression simplifies in exactly the way
you want it to. In this case, [Nat.add] branches on the first argument
first, and simply returns the second argument. So [reflexivity] figures this
one out, even though it's bad at math. *)
Lemma reflexivity_lucky :
forall n : nat,
0 + n = n.
Proof.
reflexivity.
Qed.
(* However, it's not recommended to rely on this, because if the definition of
[Nat.add] changed, your proof would break. Already, this doesn't work if you
reverse the arguments, because [Nat.add] is trying to branch on the first
argument. *)
Lemma reflexivity_unlucky :
forall n : nat,
n + 0 = n.
Proof.
Fail reflexivity. (* error : "Unable to unify 'n' with 'n + 0'." *)
Abort.
(* You can see why [reflexivity] works for [0 + n] but not [n + 0] by running
[Eval compute] on the expression to simplify it yourself. *)
Eval compute in (fun n => 0 + n). (* simplifies to [fun n => n] *)
Eval compute in (fun n => n + 0). (* simplifies to a recursive match expression *)
End ReflexivityExamples.
(* cbv :
The [cbv] tactic inlines definitions in your goal or hypotheses. If you give
it no arguments, it will inline everything. If you give it a list of term
names, however, it will only inline the things you named. [cbv] will also
inline [let]s and apply functions (so something like [(fun x y => x + y) 5]
would become [(fun y => 5 + y)].
Performance note : like [reflexivity], it's not a good idea to use [cbv] on
very large terms, because it will be slow.
*)
Module CbvExamples.
(* With no arguments, [cbv] inlines everything *)
Lemma simple_cbv :
Nat.double 5 = 11 - 1.
Proof.
(*
============================
Nat.double 5 = 11 - 1 *)
cbv.
(*
============================
10 = 10 *)
reflexivity.
Qed.
(* With arguments, [cbv] inlines only the functions specified *)
Lemma cbv_arguments :
Nat.double 5 = 11 - 1.
Proof.
(*
============================
Nat.double 5 = 11 - 1 *)
cbv [Nat.double]. (* now [Nat.double] gets inlined but [Nat.add] and
[Nat.sub] do not *)
(*
============================
5 + 5 = 11 - 1 *)
reflexivity.
Qed.
(* You can pass multiple arguments *)
Lemma cbv_multiple_arguments :
Nat.double 5 = 11 - 1.
Proof.
(*
============================
Nat.double 5 = 11 - 1 *)
cbv [Nat.double Nat.sub].
(*
============================
5 + 5 = 10 *)
reflexivity.
Qed.
(* You can also use a "-" sign to say "inline everything *except*
these functions" *)
Lemma cbv_exclude :
Nat.double 5 = 11 - 1.
Proof.
(*
============================
Nat.double 5 = 11 - 1 *)
cbv - [Nat.add].
(*
============================
5 + 5 = 10 *)
reflexivity.
Qed.
(* [cbv] works in hypotheses too *)
Lemma cbv_in_hypothesis :
forall n,
Nat.double 5 = n ->
n = 10.
Proof.
intros.
(* n : nat
H : Nat.double 5 = n
============================
n = 10 *)
cbv [Nat.double] in H.
(* n : nat
H : 5 + 5 = n
============================
n = 10 *)
lia.
Qed.
(* [cbv] can make your goal very messy if you have recursive calls to the
same function or repeated uses of the function; it inlines whethet that
makes the goal nicer or not. If [cbv] is giving you this kind of problem,
try [cbn] instead. *)
Lemma cbv_messy :
forall n m,
S n + m = n + S m.
Proof.
intros.
(* n, m : nat
============================
S n + m = n + S m *)
cbv [Nat.add].
(* n, m : nat
============================
S ((fix add (n0 m0 : nat) {struct n0} : nat := match n0 with
| 0 => m0
| S p => S (add p m0)
end) n m) =
(fix add (n0 m0 : nat) {struct n0} : nat := match n0 with
| 0 => m0
| S p => S (add p m0)
end) n (S m) *)
Abort.
End CbvExamples.
(* cbn :
The [cbn] tactic is similar to [cbv], except that it only inlines definitions
if it thinks it can simplify the goal by doing so. This makes it very useful
in cases where [cbv] inlines too aggressively.
The syntax is exactly the same as [cbv]; it can either take no arguments or it
can take some term names and not inline anything except things in the list.
For inductive proofs about recursive functions, you almost always want to use
[cbn] instead of [cbv], because using your inductive hypothesis is easiest if
you don't inline the recursive calls.
*)
Module CbnExamples.
(* If everything becomes simpler when inlined, like if there are no variables,
[cbn] has the exact same behavior as [cbv]. *)
Lemma simple_cbn :
Nat.double 5 = 11 - 1.
Proof.
(*
============================
Nat.double 5 = 11 - 1 *)
cbn.
(*
============================
10 = 10 *)
reflexivity.
Qed.
(* Here's the same proof from the [cbv] entry that [cbv] made a mess of. [cbn]
handles things much better; it only inlines the single round of [Nat.add]
that can actually be simplified, and leaves the recursive calls and other
occurences of [Nat.add] intact. *)
Lemma cbn_not_messy :
forall n m,
S n + m = n + S m.
Proof.
intros.
(* n, m : nat
============================
S n + m = n + S m *)
cbn [Nat.add].
(* n, m : nat
============================
S (n + m) = n + S m *)
lia.
Qed.
End CbnExamples.
(* induction :
The [induction] tactic is Coq's built-in machinery for doing inductive proofs,
along with [Inductive]. If you have some term [x] in context, and [x]'s type
is an [Inductive], you can write [induction x] to set up an inductive proof.
Some advice for inductive proofs:
- If you're proving something about a [Fixpoint], the decreasing argument of
the [Fixpoint] is probably the thing you want to do induction on.
- If you're having trouble making use of your inductive hypothesis because
it's too specific, you may need to make it "stronger" (less specific) by
e.g. turning constants into variables in your lemma statement, or using
more arguments in your recursive function.
- Don't use [induction] multiple times in the same proof; if you feel the
urge to do so, consider making multiple proofs.
- Run [intros] *after* [induction] to sometimes avoid accidentally making
your inductive hypothesis too weak.
*)
Module InductionExamples.
Lemma simple_nat_induction :
forall n : nat,
0 <= n.
Proof.
intros.
(* n : nat
============================
0 <= n *)
induction n.
(*
============================
0 <= 0
subgoal 2 (ID 9) is:
0 <= S n *)
(* Now we have two subgoals, corresponding to the two constructors in the
[nat] inductive definition. In the first, [n] is 0, and in the second,
[n] is the successor of another [nat]. From both definitions, our original
[n] has disappeared; the [n] in the second case is actually the
predecessor of the original. *)
{ (* subgoal 1 : 0 <= 0 *)
reflexivity. }
{ (* subgoal 2 : 0 <= S n *)
(* Note that in context here we now have an inductive hypothesis, stating
that [0 <= n]. In this case, we don't need it, but often we will. *)
lia. }
Qed.
(* You can use [induction] with any inductive datatype; here's a slightly more
complex example using [list]. *)
Lemma list_induction :
forall (A : Type) (ls1 ls2 : list nat),
length (ls1 ++ ls2) = length ls1 + length ls2.
Proof.
induction ls1; intros.
{ (* subgoal 1 : length (nil ++ ls2) = length nil + length ls2 *)
rewrite app_nil_l.
cbn [length].
lia. }
{ (* subgoal 2 : length ((cons a ls1) ++ ls2)
= length (cons a ls1) + length ls2 *)
rewrite <-app_comm_cons.
cbn [length].
rewrite IHls1. (* use of the inductive hypothesis! *)
lia. }
Qed.
(* A common pitfall in inductive proofs in general (not just in Coq) is
accidentally making your inductive hypothesis too weak. Most commonly, if
your proof is about a recursive function and you need to be able to change
an argument *other* than the one you're doing [induction] on, you'll need
your inductive hypothesis to have a [forall] qualifier for the changing
argument. This takes a little explanation, but is a really common way to get
stuck and is worth being aware of.
To make things more concrete, I'll demonstrate making a too-weak inductive
hypothesis for a proof about the [seq] function, and how to fix it. *)
(* Reproduction of the [seq] function from the standard list library; produces
a list of [length] sequential natural numbers beginning with [start]. That
is, [seq 3 4] will be the list [3;4;5;6]. *)
Fixpoint seq (start len : nat) : list nat :=
match len with
| O => nil (* length 0; empty list *)
| S len' =>
(* increment start and decrease length *)
cons start (seq (S start) len')
end.
(* Since the [seq] function decreases on [len], that's the argument we want to
do [induction] on. But notice that [start] also changes between calls, and
that's how we can run into problems. *)
Lemma bad_inductive_hypothesis :
forall start len,
length (seq start len) = len.
Proof.
(*
============================
forall start len : nat, length (seq start len) = len *)
induction len.
{ (* subgoal 1 (len = 0) *)
(* start : nat
============================
length (seq start 0) = 0 *)
cbn [seq length].
(* start : nat
============================
0 = 0 *)
reflexivity. }
{ (* subgoal 2 (len = S len') *)
(* start, len : nat
IHlen : length (seq start len) = len
============================
length (seq start (S len)) = S len *)
(* Take a close look at the inductive hypothesis, and notice that it
doesn't apply to just any [start]; it requires the specific argument
we had to begin with, and that's going to be a problem. *)
cbn [seq length].
(* start, len : nat
IHlen : length (seq start len) = len
============================
S (length (seq (S start) len)) = S len *)
(* Now our goal talks about starting with [S start], and our inductive
hypothesis doesn't apply at all. We need the hypothesis to say
[forall start]. *)
Abort.
(* The reason the previous proof failed is that [induction] automatically
[intros] everything up to the variable you do induction on. In this case,
we want to leave the [forall start] intact in our lemma statement. The
easiest way to do this is simply to switch the order of the lemma
arguments. *)
Lemma good_inductive_hypothesis :
forall len start,
length (seq start len) = len.
Proof.
(*
============================
forall len start : nat, length (seq start len) = len *)
induction len.
{ (* subgoal 1 (len = 0) *)
(*
============================
forall start, length (seq start 0) = 0 *)
intros.
cbn [seq length].
(*
============================
0 = 0 *)
reflexivity. }
{ (* subgoal 2 (len = S len') *)
(* len : nat
IHlen : forall start, length (seq start len) = len
============================
forall start, length (seq start (S len)) = S len *)
(* Our inductive hypothesis has a [forall] now! *)
intros.
cbn [seq length].
(* len : nat
IHlen : forall start : nat, length (seq start len) = len
start : nat
============================
S (length (seq (S start) len)) = S len *)
rewrite IHlen. (* ...and we can use it to prove the goal *)
(* len : nat
IHlen : forall start : nat, length (seq start len) = len
start : nat
============================
S len = S len *)
reflexivity. }
Qed.
End InductionExamples.
(* lia :
The [lia] tactic tries to solve your goal using linear arithmetic. It's
pretty smart, and knows about minimum and maximum functions as well as the
usual arithmetic operations. It takes no arguments.
If your goal has [forall]s in it, always call [intros] before [lia].
Coq does not include [lia] by default; you need to import it from the standard
library with [Require Import Coq.micromega.Lia]. This import will give you
[nia] as well.
If it can't solve the goal, [lia] will fail and give you no clues about what
preconditions it might be missing.
Lots of the entries in this reference use [lia]; feel free to search for more
examples.
*)
Module LiaExamples.
Lemma simple_lia :
forall n m,
n < m ->
n <= m.
Proof.
intros.
lia.
Qed.
Lemma more_complex :
forall n m,
5 < Nat.min n m ->
3 < m.
Proof.
intros.
lia.
Qed.
(* save yourself lots of work! *)
Lemma annoying_algebra :
forall n m,
2 * n + m * (n + 3) = m * n + 3 * (m + n) - n.
Proof.
intros.
lia.
Qed.
(* this goal is too much for lia *)
Lemma lia_fails :
forall a b,
b <> 0 ->
b * a + b * (b - 1) * a = b * b * a.
Proof.
intros.
Fail lia. (* lia doesn't work! *)
(* but, if we give it some help by letting it put all the [b] expressions in
terms of [b-1], so it doesn't have to deal with the subtraction, it'll
figure it out *)
replace b with (S (b - 1)) by lia.
replace (S (b - 1) - 1) with (b - 1) by lia.
lia. (* now it works *)
Qed.
End LiaExamples.
(* nia :
The [nia] tactic is a stronger version of [lia]. It works on pretty much
everything [lia] works on, and some things [lia] doesn't. It can be, however,
much slower than [lia], so only use [nia] if [lia] doesn't work. No need to
use a hammer to crack a nut.
*)
Module NiaExamples.
(* this is the goal from the [lia] entry that [lia] needed help to solve. [nia]
requires no assistance. *)
Lemma lia_fails :
forall a b,
b <> 0 ->
b * a + b * (b - 1) * a = b * b * a.
Proof.
intros.
nia.
Qed.
End NiaExamples.
(* replace :
The [replace] tactic lets you replace one expression in your goal or
hypothesis with another expression, and leaves you a new subgoal to prove
that the two are equal. The syntax is:
replace <expression> with <expression>.
If you want to do the [replace] in a hypothesis instead of a goal, use:
replace <expression> with <expression> in <hypothesis>.
...and if you want to prove the new subgoal immediately:
replace <expression> with <expression> by <tactic>.
OR
replace <expression> with <expression> in <hypothesis> by <tactic>.
[replace] is most useful if you want to do a bunch of annoying algebra
manipulations on a term that's buried inside an expression. By creating a new
subgoal with only the algebra reasoning, you can prove the new goal with a
tactic like [lia] and save yourself work.
*)
Module ReplaceExamples.
Lemma simple_replace :
forall n ls,
cons (S n - 1) ls = cons n ls.
Proof.
intros.
(* n : nat
ls : list nat
============================
S n - 1 :: ls = n :: ls *)
(* Logically, we know this is true because [S n - 1] equals [n]. [lia] could
prove that, but it won't work to use [lia] here because the goal is in
terms of lists. Instead, we create a new subgoal that [lia] can solve. *)
replace (S n - 1) with n.
(* n : nat
ls : list nat
============================
n :: ls = n :: ls
subgoal 2 (ID 11) is:
n = S n - 1 *)
{ reflexivity. }
{ lia. (* this is the subgoal left by [replace] *) }
Qed.
(* like [rewrite], you can use [by] to immediately prove the new subgoal. *)
Lemma replace_by :
forall n ls,
cons (S n - 1) ls = cons n ls.
Proof.
intros.
(* n : nat
ls : list nat
============================
S n - 1 :: ls = n :: ls *)
replace (S n - 1) with n by lia.
(* n : nat
ls : list nat
============================
n :: ls = n :: ls *)
(* No new subgoal! *)
reflexivity.
Qed.
Lemma replace_in_hypothesis :
forall n m,
n + n <= m ->
2 * n <= m.
Proof.
intros.
(* n, m : nat
H : n + n <= m
============================
2 * n <= m *)
replace (n + n) with (2 * n) in H by lia.
apply H.
Qed.
End ReplaceExamples.To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.