Skip to content

Quick Reference for Beginners

alex argunov edited this page Aug 29, 2019 · 2 revisions

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.
Clone this wiki locally
You can’t perform that action at this time.