MPRI PRFA — Proof Assistants

Inductive types — part 1

This week, we will talk about inductive types. At their basis, inductive types are similar to algebraic data types from OCaml or Haskell. In Rocq, they are however more expressive, and can for instance also be used to express certain logical predicates.

We first make sure that the use of bullets is enforced:

Set Default Goal Selector "!".

Inductive types can be defined using the Inductive keyword.

Below, we give the definition of natural numbers nat. They are exactly the same as the ones from the standard library which we have seen in the first lecture.

The type nat is made of two constructors: O and S. We have O : nat and S n : nat if n : nat. (Notice how this is O and not 0 as names cannot start with a numeral. The use of 0 is allowed thanks to a notation mechanism.) Rocq uses BNF (Backus-Naur-form) notation for inductive types:

Inductive nat : Type :=
| O : nat
| S : nat -> nat.nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined
nat_sind is defined

Check nat.nat
     : Set
Check O.O
     : nat
Check S.S
     : nat -> nat

If you look carefully, you will see that Rocq says that nat is of type Set when we wrote nat : Type. This is mostly for historical reasons and you can roughly conflate the two. We encourage you to use Type though.

Elements of the type nat now consist exactly of O, S O, S (S O), and so on:

Check (S O).S O
     : nat
Check (S (S O)).S (S O)
     : nat

The Inductive command allows syntactic flexibility. We could also have written the following:

Inductive nat := | O : nat | S (n : nat) : nat.

Inductive nat := O | S (n : nat).

In practice you get to pick the variant that suits you the most as they are anyway equivalent: they merely differ in how you write them, but produce the same definition.

As the word inductive type hints, one can do proofs by induction about them. Mathematically, an inductive type is the smallest type closed under the type's constructors. You are already familiar with induction on natural numbers from week 1. However, make sure that you are also familiar with the exact formulation of the induction principle:

Check nat_ind.nat_ind
     : forall P : nat -> Prop, P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

As you have seen in week 1, one can define recursive functions operating on inductive arguments with the Fixpoint keyword:

Fixpoint add (n m : nat) {struct n} :=
  match n with
  | O => m
  | S n => S (add n m)
  end.add is defined
add is recursively defined (guarded on 1st argument)

Rocq ensures that recursive functions are terminating, for reasons we will discuss later.

To ensure termination, recursion has to be performed on a structurally smaller argument. In the case of double from last week, there was only one argument so it was obvious which one had to decrease. This time, there is an ambiguity: it could be either n or m. The {struct n} annotation above tells Rocq that n is the one that is structurally decreasing.

Of course, it won't blindly trust us, there is a complex termination checker (sometimes called guard checker) which will make sure this is indeed the case. For instance, if you were to suggest that m was structurally decreasing, Rocq would rightfully complain:

Fail Fixpoint add' (n m : nat) {struct m} :=
  match n with
  | O => m
  | S n => S (add' n m)
  end.The command has indeed failed with message:
Recursive definition of add' is ill-formed.
In environment
add' : nat -> nat -> nat
n : nat
m : nat
n0 : nat
Recursive call to add' has principal argument equal to "m" instead of a subterm of "m".
Recursive definition is: "fun n m : nat => match n with | O => m | S n0 => S (add' n0 m) end".

The important bit of the error message is the one saying:

Recursive call to add' has principal argument equal to "m" instead of a subterm of "m".

In other words it's complaining about the recursive call being performed on m again.

Note that there are other ways to define functions using more complex recursion patterns — you will learn about them soon.

Evaluating functions

It is possible to evaluate a function, such as the add function above by using the Eval command.

Note how the following evaluates to fun m => m (the identity function):

Eval simpl in (fun m => add O m).= fun m : nat => m
: nat -> nat

However, the following expression cannot be simplified using computation.

Eval simpl in (fun n => add n O).= fun n : nat => add n O
: nat -> nat

Instead, we can prove this equation:

Lemma add_0 n :
  add n O = n.n: nat
add n O = n
Proof.n: nat
add n O = n
  induction n as [| n IHn].add O O = O
n: nat
IHn: add n O = n
add (S n) O = S n
  -add O O = O reflexivity.
  -n: nat
IHn: add n O = n
add (S n) O = S n simpl.n: nat
IHn: add n O = n
S (add n O) = S n rewrite IHn.n: nat
IHn: add n O = n
S n = S n reflexivity.
Qed.add_0 is defined

We can introduce infix notations as follows:

Infix "+" := add.

See how Rocq prints the lemma statement using + now!

Check add_0.add_0
     : forall n : nat, n + O = n

Now, even if we still use add, Rocq will print the goal using +.

Lemma add_S n m :
  add n (S m) = S (add n m).n, m: nat
n + S m = S (n + m)
Proof.n, m: nat
n + S m = S (n + m)
  induction n as [| n IHn].m: nat
O + S m = S (O + m)
n, m: nat
IHn: n + S m = S (n + m)
S n + S m = S (S n + m)
  -m: nat
O + S m = S (O + m) reflexivity.
  -n, m: nat
IHn: n + S m = S (n + m)
S n + S m = S (S n + m) simpl.n, m: nat
IHn: n + S m = S (n + m)
S (n + S m) = S (S (n + m)) rewrite IHn.n, m: nat
IHn: n + S m = S (n + m)
S (S (n + m)) = S (S (n + m)) reflexivity.
Qed.add_S is defined

We define (truncating) subtraction on natural numbers:

Fixpoint sub (n m : nat) : nat :=
  match n, m with
  | O, _  => O
  | S n', O => n
  | S n', S m' => sub n' m'
  end.sub is defined
sub is recursively defined (guarded on 1st argument)

Note that we did not provide a {struct _} argument here because Rocq can infer it automatically. On paper, we will however often ask you to tell us which argument is structurally decreasing, so it is good to think for yourself about which argument decreases when writing a function.

Instead of using Infix to give a notation to sub we can also use the Notation command. It asks for more information and is sometimes tricky to use but it is very powerful. We will see more examples over the course of the lecture so don't worry too much about it.

Notation "n - m" := (sub n m).

An alternative to Eval simpl in e is Compute e. See what it does to the following two expressions.

Compute (S (S O) - S O). (* 2 - 1 = 1 *)= S O
: nat
Compute (S O - S (S O)). (* 1 - 2 = 0 *)= O
: nat

We can now prove a lemma involving addition and subtraction that we just defined.

Lemma add_sub n m :
  (n + m) - n = m.n, m: nat
n + m - n = m
Proof.n, m: nat
n + m - n = m
  induction n.m: nat
O + m - O = m
n, m: nat
IHn: n + m - n = m
S n + m - S n = m
  -m: nat
O + m - O = m simpl.m: nat
m - O = m destruct m.O - O = O
m: nat
S m - O = S m all: reflexivity.
  -n, m: nat
IHn: n + m - n = m
S n + m - S n = m assumption.
Qed.add_sub is defined

Predicates, propositions and injectivity of constructors

In Rocq, everything is computational, including propositions.

We can define the following Boolean predicate testing whether a natural number is 0 or not.

Definition is_zerob (n : nat) : bool :=
  match n with
  | O => true
  | S n => false
  end.is_zerob is defined

But we can also produce directly a proposition asserting asserting whether the natural number is 0 or not. Pay attention to the use of Prop instead of bool and of capital True and False.

Definition is_zero (n : nat) : Prop :=
  match n with
  | O => True
  | S n => False
  end.is_zero is defined

Of course, a proposition stating that n is 0 could equivalently be written as n = 0 as we have seen already. Similarly, we can express what it means to be different from 0 by writing n <> 0, which is Rocq's way of writing n ≠ 0 (in fact, if you use Unicode with Rocq you can also write n ≠ 0 directly, it is mostly a matter of taste and getting used to, see our FAQ to know more). This notation is nothing more than the negation of n = 0, in other words it unfolds to (n = 0) -> False.

We can use this to prove the fact that, in general, constructors are distinct. For nat this means that 0 and S n can always be distinguished.

Lemma S_O n :
  S n <> O.n: nat
S n <> O
Proof.n: nat
S n <> O

This can be proved manually

  intros E.n: nat
E: S n = O
False

We use the change tactic to change the goal to something equivalent w.r.t. computation.

  change (is_zero (S n)).n: nat
E: S n = O
is_zero (S n)

We can simplify again to get the old goal. This is in fact the reason why change succeeded in the first place.

  simpl.n: nat
E: S n = O
False
  change (is_zero (S n)).n: nat
E: S n = O
is_zero (S n)

Now that our goal is is_zero (S n) we want to use our hypothesis E : S n = 0 to get is_zero 0 instead. We can do this using the rewrite tactic which will replace occurrence of S n in the goal by the right-hand side of the equation, namely 0.

  rewrite E.n: nat
E: S n = O
is_zero O

Computation is now handy again, because is_zero 0 is much easier to prove than False. We simplify and then conclude.

  simpl.n: nat
E: S n = O
True
  split.
Qed.S_O is defined

There is also a tactic to automatically discharge such goals: discriminate.

Lemma S_0' n :
  S n <> O.n: nat
S n <> O
Proof.n: nat
S n <> O
  discriminate.
Qed.S_0' is defined

Say now we want to prove that S is injective. We can achieve this by using an auxiliary function pred such that pred (S n) = n (in other words, it is a left inverse to S). By congruence (f_equal) we can thus go from S n = S m to pred (S n) = pred (S m) which is then the same as n = m.

You can see here that it doesn't matter what value we choose for pred 0. We're just going to pick 0.

Definition pred n :=
  match n with
  | O => O
  | S n => n
  end.pred is defined

We can now prove that S is injective. It is in fact true for all constructors.

Lemma S_inj n m :
  S n = S m -> n = m.n, m: nat
S n = S m -> n = m
Proof.n, m: nat
S n = S m -> n = m
  intros E.n, m: nat
E: S n = S m
n = m
  change (pred (S n) = m).n, m: nat
E: S n = S m
pred (S n) = m
  rewrite E.n, m: nat
E: S n = S m
pred (S m) = m
  reflexivity.
Qed.S_inj is defined

We could in fact do it without pred.

Lemma S_inj_2 n m :
  S n = S m -> n = m.n, m: nat
S n = S m -> n = m
Proof.n, m: nat
S n = S m -> n = m
  intros E.n, m: nat
E: S n = S m
n = m
  change (match S n with O => True | S k => k = m end).n, m: nat
E: S n = S m
match S n with | O => True | S k => k = m end
  rewrite E.n, m: nat
E: S n = S m
m = m
  reflexivity.
Qed.S_inj_2 is defined

We can also use the f_equal lemma (not the tactic!).

Lemma S_inj_3 n m :
  S n = S m -> n = m.n, m: nat
S n = S m -> n = m
Proof.n, m: nat
S n = S m -> n = m
  Check f_equal.f_equal
     : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y
n, m: nat
S n = S m -> n = m
  intros E.n, m: nat
E: S n = S m
n = m
  apply (f_equal pred) in E.n, m: nat
E: pred (S n) = pred (S m)
n = m
  assumption.
Qed.S_inj_3 is defined

Finally, we have tactics that do this automatically such as inversion.

Lemma S_inj_4 n m :
  S n = S m -> n = m.n, m: nat
S n = S m -> n = m
Proof.n, m: nat
S n = S m -> n = m
  intros E.n, m: nat
E: S n = S m
n = m
  inversion E.n, m: nat
E: S n = S m
H0: n = m
m = m
  reflexivity.
Qed.S_inj_4 is defined

Generalising induction hypotheses

Let us now try and prove things about functions operating on inductive types. We're going to start by defining a function for deciding equality between natural numbers.

Fixpoint eq_nat x y : bool :=
  match x, y with
  | O, O => true
  | O, S _ => false
  | S _, O => false
  | S x', S y' => eq_nat x' y'
  end.eq_nat is defined
eq_nat is recursively defined (guarded on 1st argument)

We're going to prove that it indeed decides equality of natural numbers. Below, we make use of the notation P <-> Q which corresponds to logical equivalence, in other words the conjunction of P -> Q and Q -> P.

Lemma eq_nat_spec n m :
  eq_nat n m = true <-> n = m.n, m: nat
eq_nat n m = true <-> n = m
Proof.n, m: nat
eq_nat n m = true <-> n = m
  induction n as [ | n' IH].m: nat
eq_nat O m = true <-> O = m
n', m: nat
IH: eq_nat n' m = true <-> n' = m
eq_nat (S n') m = true <-> S n' = m all: simpl.m: nat
match m with | O => true | S _ => false end = true <-> O = m
n', m: nat
IH: eq_nat n' m = true <-> n' = m
match m with | O => false | S y' => eq_nat n' y' end = true <-> S n' = m

In case you are wondering, we made use of all: simpl. here to apply the simpl tactic to all subgoals, before even focusing them. all is called a goal selector and can be useful in certain situations.

  -m: nat
match m with | O => true | S _ => false end = true <-> O = m destruct m.true = true <-> O = O
m: nat
false = true <-> O = S m all: simpl.true = true <-> O = O
m: nat
false = true <-> O = S m
    +true = true <-> O = O split.true = true -> O = O
O = O -> true = true all: reflexivity.

Notice reflexivity is able to conclude A -> 0 = 0 for any A.

    +m: nat
false = true <-> O = S m split.m: nat
false = true -> O = S m
m: nat
O = S m -> false = true all: intros E.m: nat
E: false = true
O = S m
m: nat
E: O = S m
false = true all: discriminate E.

Here we provided E to discriminate to tell it which assumption was inconsistent (equating two distinct constructors).

  -n', m: nat
IH: eq_nat n' m = true <-> n' = m
match m with | O => false | S y' => eq_nat n' y' end = true <-> S n' = m destruct m.n': nat
IH: eq_nat n' O = true <-> n' = O
false = true <-> S n' = O
n', m: nat
IH: eq_nat n' (S m) = true <-> n' = S m
eq_nat n' m = true <-> S n' = S m
    +n': nat
IH: eq_nat n' O = true <-> n' = O
false = true <-> S n' = O split.n': nat
IH: eq_nat n' O = true <-> n' = O
false = true -> S n' = O
n': nat
IH: eq_nat n' O = true <-> n' = O
S n' = O -> false = true all: discriminate.
    +n', m: nat
IH: eq_nat n' (S m) = true <-> n' = S m
eq_nat n' m = true <-> S n' = S m

We are now stuck. The IH talks about S m, but we need it for m. Note that this always happens when a recursive function changes other arguments apart from its structural argument.

Abort.

The proper way to deal with this is by generalising the induction hypothesis. We have to do this before we start perfoming induction. The reason we have to do this is because Rocq is trying to infer the property we prove by induction on its own: we only say we want to perform induction on n and it then tries to infer the property from the goal. Fortunately, the induction tactic also supports generalisation with the keyword in, as follows.

Lemma eq_nat_spec n m :
  eq_nat n m = true <-> n = m.n, m: nat
eq_nat n m = true <-> n = m
Proof.n, m: nat
eq_nat n m = true <-> n = m
  induction n as [ | n' IH] in m |- *.m: nat
eq_nat O m = true <-> O = m
n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') m = true <-> S n' = m

The syntax is bit heavy: m |- * represents which information should Rocq take into account when generating the induction hypothesis. The turnstile |- is supposed to represent the whole proof goal, with the hypotheses on the left, and the proposition to prove on the right. We use * to indicate that we want to include the goal (which you always will want to do) and m on the left to indicate we generalise over it, and nothing else.

  -m: nat
eq_nat O m = true <-> O = m destruct m.eq_nat O O = true <-> O = O
m: nat
eq_nat O (S m) = true <-> O = S m all: simpl.true = true <-> O = O
m: nat
false = true <-> O = S m
    +true = true <-> O = O split.true = true -> O = O
O = O -> true = true all: reflexivity.
    +m: nat
false = true <-> O = S m split.m: nat
false = true -> O = S m
m: nat
O = S m -> false = true all: discriminate.
  -n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') m = true <-> S n' = m

See how the IH is quantified for all m.

    destruct m.n': nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') O = true <-> S n' = O
n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') (S m) = true <-> S n' = S m all: simpl.n': nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
false = true <-> S n' = O
n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat n' m = true <-> S n' = S m
    +n': nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
false = true <-> S n' = O split.n': nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
false = true -> S n' = O
n': nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
S n' = O -> false = true all: discriminate.
    +n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat n' m = true <-> S n' = S m split.n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
eq_nat n' m = true -> S n' = S m
n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
S n' = S m -> eq_nat n' m = true all: intros E.n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: eq_nat n' m = true
S n' = S m
n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
eq_nat n' m = true
      *n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: eq_nat n' m = true
S n' = S m apply IH in E.n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: n' = m
S n' = S m rewrite E.n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: n' = m
S m = S m reflexivity.
      *n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
eq_nat n' m = true apply IH.n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
n' = m inversion E.n', m: nat
IH:= forall m: nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
H0: n' = m
m = m reflexivity.
Qed.eq_nat_spec is defined

Booleans

Booleans are even simpler.

Inductive bool := true | false.bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined
bool_sind is defined

Check true.true
     : bool
Check bool.bool
     : Set

Since bool is not recursive, the induction principle is a lot simpler. In this case, it makes sense to talk about case anlysis instead.

Check bool_ind.bool_ind
     : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b

Again, since it's an inductive type, the constructors are disjoint.

Lemma true_false :
  true <> false.true <> false
Proof.true <> false
  discriminate.
Qed.true_false is defined

Cartesian product

We can define more types, such as the cartesian product.

We define product types inductively with one constructor taking two arguments.

Inductive prod X Y :=
| pair (x : X) (y : Y).prod is defined
prod_rect is defined
prod_ind is defined
prod_rec is defined
prod_sind is defined

Note how the constructor pair takes 4 arguments:

Check pair.pair
     : forall X Y : Type, X -> Y -> prod X Y

Namely types X and Y, and elements x : X and y : Y.

The first two arguments are real arguments that can be passed explicitly: types are first-class in Rocq.

Check pair nat.pair nat
     : forall Y : Type, nat -> Y -> prod nat Y

Furthermore, types can appear at any position in arguments, unlike OCaml where the quantification is necessarily prenex.

Definition pair' X (x : X) Y (y : Y) :=
  pair X Y x y.pair' is defined

Check pair'.pair'
     : forall X : Type, X -> forall Y : Type, Y -> prod X Y

Also, the type arguments have to be passed.

Fail Check pair' 0 0.The command has indeed failed with message:
The term "0" has type "Datatypes.nat" while it is expected to have type "Type".

However, we can declare arguments as implicit using the Arguments command by marking implicit arguments with braces {} (sometimes called squigly brackets).

Arguments pair' {X} x {Y} y.

When an argument is implicit, Rocq tries to infer what it has to be, based on the other passed arguments. If we build the pair (O,O) then both types have to be nat and Rocq is able to figure it out.

Check pair' O O.pair' O O
     : prod nat nat

We can use the following command to force Rocq to print implicit arguments.

Set Printing Implicit.

There we can see the nat that have been inferred.

Check pair' O O.@pair' nat O nat O
     : prod nat nat

We go back to not printing implicit arguments.

Unset Printing Implicit.

We can define the first projection by pattern matching.

Note that we mark arguments as implicit directly.

Definition fst {X Y} (p : prod X Y) : X :=
  match p with
  | pair _ _ x y => x
  end.fst is defined

Remark: In the pattern matching above, we had to also talk about the type parameters of pair even though they are not necessary. By making them implicit in the constructor pair, we can write nicer pattern matching.

Arguments pair {X Y} x y.

Definition snd {X Y} (p : prod X Y) : Y :=
  match p with
  | pair x y => y
  end.snd is defined

Lists

The type of list is both recursive and has a type parameter.

Inductive list (A : Type) :=
| nil : list A
| cons : A -> list A -> list A.list is defined
list_rect is defined
list_ind is defined
list_rec is defined
list_sind is defined

We declare arguments as implicit. Note here we can specify a prefix if we want.

Arguments nil {A}.
Arguments cons {A}.

Set Printing Implicit.
Compute (cons 5 nil).= @cons Datatypes.nat 5 (@nil Datatypes.nat)
: list Datatypes.nat
Unset Printing Implicit.

Check now the induction principle we get for lists. It's saying that to prove P l for some list l, you only need to prove

P nil

P (cons a l') for any a and l' such that P l'

Have a look at its type:

Check list_ind.list_ind
     : forall (A : Type) (P : list A -> Prop), P nil -> (forall (a : A) (l : list A), P l -> P (cons a l)) -> forall l : list A, P l

Proofs by induction

We reimport all these datatypes from Rocq, to be able to use functions from the standard library.

From Stdlib  Require Import Datatypes List.
Open Scope nat.

Like for nat, list in the standard library comes with nice notations to be able to write x :: l or [ a ; b ; c ; d ]. We can load them as follows.

Import ListNotations.

Below we check the types of concatenation and reversal of lists.

About app.app : forall [A : Type], list A -> list A -> list Aapp is not universe polymorphicArguments app [A]%type_scope (_ _)%list_scopeapp is transparentExpands to: Constant Corelib.Init.Datatypes.appDeclared in library Corelib.Init.Datatypes, line 337, characters 11-14
About rev.rev : forall [A : Type], list A -> list Arev is not universe polymorphicArguments rev [A]%type_scope l%list_scoperev is transparentExpands to: Constant Stdlib.Lists.List.revDeclared in library Stdlib.Lists.List, line 978, characters 2-113

Lemmas about lists we typically proven by induction as we did for natural numbers.

Lemma app_nil_r A (l : list A) :
  l ++ nil = l.A: Type
l: list A
l ++ [] = l
Proof.A: Type
l: list A
l ++ [] = l
  induction l.A: Type
[] ++ [] = []
A: Type
a: A
l: list A
IHl: l ++ [] = l
(a :: l) ++ [] = a :: l all: simpl.A: Type
[] = []
A: Type
a: A
l: list A
IHl: l ++ [] = l
a :: l ++ [] = a :: l
  -A: Type
[] = [] reflexivity.
  -A: Type
a: A
l: list A
IHl: l ++ [] = l
a :: l ++ [] = a :: l f_equal.A: Type
a: A
l: list A
IHl: l ++ [] = l
l ++ [] = l assumption.
Qed.app_nil_r is defined

Lemma rev_app_distr {A} (l1 l2 : list A) :
  rev (l1 ++ l2) = rev l2 ++ rev l1.A: Type
l1, l2: list A
rev (l1 ++ l2) = rev l2 ++ rev l1
Proof.A: Type
l1, l2: list A
rev (l1 ++ l2) = rev l2 ++ rev l1
  induction l1 as [| a l IHl].A: Type
l2: list A
rev ([] ++ l2) = rev l2 ++ rev []
A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
rev ((a :: l) ++ l2) = rev l2 ++ rev (a :: l) all: simpl.A: Type
l2: list A
rev l2 = rev l2 ++ []
A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
rev (l ++ l2) ++ [a] = rev l2 ++ rev l ++ [a]
  -A: Type
l2: list A
rev l2 = rev l2 ++ [] rewrite app_nil_r.A: Type
l2: list A
rev l2 = rev l2 reflexivity.
  -A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
rev (l ++ l2) ++ [a] = rev l2 ++ rev l ++ [a]

For rewrite we can separate two lemmas to rewrite by a comma.

    rewrite IHl, app_assoc.A: Type
a: A
l, l2: list A
IHl: rev (l ++ l2) = rev l2 ++ rev l
(rev l2 ++ rev l) ++ [a] = (rev l2 ++ rev l) ++ [a] reflexivity.
Qed.rev_app_distr is defined

Lemma rev_rev {A} (l : list A) :
  rev (rev l) = l.A: Type
l: list A
rev (rev l) = l
Proof.A: Type
l: list A
rev (rev l) = l
  induction l.A: Type
rev (rev []) = []
A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev (a :: l)) = a :: l all: simpl.A: Type
[] = []
A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev l ++ [a]) = a :: l
  -A: Type
[] = [] reflexivity.
  -A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev l ++ [a]) = a :: l rewrite rev_app_distr.A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev [a] ++ rev (rev l) = a :: l simpl.A: Type
a: A
l: list A
IHl: rev (rev l) = l
a :: rev (rev l) = a :: l rewrite IHl.A: Type
a: A
l: list A
IHl: rev (rev l) = l
a :: l = a :: l reflexivity.
Qed.rev_rev is defined

The rev defined above is not very smart because it uses concatenation on the right which is expensive. However, it works as a specification for a smarter version using an accumulator.

Fixpoint fast_rev {A} (l : list A) (acc : list A) :=
  match l with
  | [] => acc
  | x :: l => fast_rev l (x :: acc)
  end.fast_rev is defined
fast_rev is recursively defined (guarded on 2nd argument)

We can show the two behave the same.

Lemma fast_rev_eq {A} (l : list A) :
  fast_rev l nil = rev l.A: Type
l: list A
fast_rev l [] = rev l
Proof.A: Type
l: list A
fast_rev l [] = rev l
  induction l.A: Type
fast_rev [] [] = rev []
A: Type
a: A
l: list A
IHl: fast_rev l [] = rev l
fast_rev (a :: l) [] = rev (a :: l) all: simpl.A: Type
[] = []
A: Type
a: A
l: list A
IHl: fast_rev l [] = rev l
fast_rev l [a] = rev l ++ [a]
  -A: Type
[] = [] reflexivity.
  -A: Type
a: A
l: list A
IHl: fast_rev l [] = rev l
fast_rev l [a] = rev l ++ [a]

We are stuck again, because the acc argument is changed.

Abort.

Lemma fast_rev_eq {A} (l : list A) :
  fast_rev l nil = rev l.A: Type
l: list A
fast_rev l [] = rev l
Proof.A: Type
l: list A
fast_rev l [] = rev l

We prove a more general lemma locally. We're using forall here to introduce a parameter.

  assert (H : forall acc, fast_rev l acc = rev l ++ acc).A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc
A: Type
l: list A
H:= forall acc: list A, fast_rev l acc = rev l ++ acc
fast_rev l [] = rev l
  {A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc induction l as [| a l IHl].A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc
A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc all: simpl.A: Type
forall acc : list A, acc = acc
A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc all: intros acc.A: Type
acc: list A
acc = acc
A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc
    -A: Type
acc: list A
acc = acc reflexivity.
    -A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc rewrite IHl.A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = (rev l ++ [a]) ++ acc rewrite <- app_assoc.A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ [a] ++ acc reflexivity.
  }A: Type
l: list A
H:= forall acc: list A, fast_rev l acc = rev l ++ acc
fast_rev l [] = rev l
  rewrite H.A: Type
l: list A
H:= forall acc: list A, fast_rev l acc = rev l ++ acc
rev l ++ [] = rev l Search app nil.app_nil_r: forall (A : Type) (l : list A), l ++ [] = l
app_nil_end_deprecated: forall [A : Type] (l : list A), l = l ++ []
List.app_nil_r: forall [A : Type] (l : list A), l ++ [] = l
app_nil_l: forall [A : Type] (l : list A), [] ++ l = l
removelast_last: forall [A : Type] (l : list A) (a : A), removelast (l ++ [a]) = l
last_last: forall [A : Type] (l : list A) (a d : A), last (l ++ [a]) d = a
app_cons_not_nil: forall [A : Type] (x y : list A) (a : A), [] <> x ++ a :: y
rev_unit: forall [A : Type] (l : list A) (a : A), rev (l ++ [a]) = a :: rev l
last_length: forall [A : Type] (l : list A) (a : A), length (l ++ [a]) = S (length l)
repeat_cons: forall [A : Type] (n : nat) (a : A), a :: repeat a n = repeat a n ++ [a]
rev_ind: forall [A : Type] (P : list A -> Prop), P [] -> (forall (x : A) (l : list A), P l -> P (l ++ [x])) -> forall l : list A, P l
app_eq_nil: forall [A : Type] (l l' : list A), l ++ l' = [] -> l = [] /\ l' = []
seq_S: forall len start : nat, seq start (S len) = seq start len ++ [start + len]
removelast_app: forall [A : Type] (l : list A) [l' : list A], l' <> [] -> removelast (l ++ l') = l ++ removelast l'
app_removelast_last: forall [A : Type] [l : list A] (d : A), l <> [] -> l = removelast l ++ [last l d]
map_last: forall [A B : Type] (f : A -> B) (l : list A) (a : A), map f (l ++ [a]) = map f l ++ [f a]
exists_last: forall [A : Type] [l : list A], l <> [] -> {l' : list A & {a : A | l = l' ++ [a]}}
app_inj_tail: forall [A : Type] (x y : list A) (a b : A), x ++ [a] = y ++ [b] -> x = y /\ a = b
app_inj_tail_iff: forall [A : Type] (x y : list A) (a b : A), x ++ [a] = y ++ [b] <-> x = y /\ a = b
elt_eq_unit: forall [A : Type] (l1 l2 : list A) (a : A) [b : A], l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []
Relation_Operators.d_conc: forall (A : Set) (leA : A -> A -> Prop) (x y : A) (l : list A), Relation_Operators.clos_refl A leA x y -> Relation_Operators.Desc A leA (l ++ [y]) -> Relation_Operators.Desc A leA ((l ++ [y]) ++ [x])
app_eq_unit: forall [A : Type] (x y : list A) [a : A], x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []
app_eq_cons: forall [A : Type] (x y : list A) [z : list A] [a : A], x ++ y = a :: z -> x = [] /\ y = a :: z \/ (exists x' : list A, x = a :: x' /\ z = x' ++ y)
Relation_Operators.Desc_ind: forall (A : Set) (leA : A -> A -> Prop) (P : list A -> Prop), P [] -> (forall x : A, P [x]) -> (forall (x y : A) (l : list A), Relation_Operators.clos_refl A leA x y -> Relation_Operators.Desc A leA (l ++ [y]) -> P (l ++ [y]) -> P ((l ++ [y]) ++ [x])) -> forall l : list A, Relation_Operators.Desc A leA l -> P l
Relation_Operators.Desc_sind: forall (A : Set) (leA : A -> A -> Prop) (P : list A -> SProp), P [] -> (forall x : A, P [x]) -> (forall (x y : A) (l : list A), Relation_Operators.clos_refl A leA x y -> Relation_Operators.Desc A leA (l ++ [y]) -> P (l ++ [y]) -> P ((l ++ [y]) ++ [x])) -> forall l : list A, Relation_Operators.Desc A leA l -> P l
A: Type
l: list A
H:= forall acc: list A, fast_rev l acc = rev l ++ acc
rev l ++ [] = rev l rewrite app_nil_r.A: Type
l: list A
H:= forall acc: list A, fast_rev l acc = rev l ++ acc
rev l = rev l reflexivity.
Qed.fast_rev_eq is defined

We can prove things in a different way.

Lemma fast_rev_eq_alt {A} (l : list A) :
  fast_rev l nil = rev l.A: Type
l: list A
fast_rev l [] = rev l
Proof.A: Type
l: list A
fast_rev l [] = rev l

We are going to generalise the empty list to any acc. We write @nil A to provide the type argument A explicitly.

  rewrite <- app_nil_r.A: Type
l: list A
fast_rev l [] = rev l ++ [] generalize (@nil A) as acc.A: Type
l: list A
forall acc : list A, fast_rev l acc = rev l ++ acc
  induction l as [| a l IHl].A: Type
forall acc : list A, fast_rev [] acc = rev [] ++ acc
A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev (a :: l) acc = rev (a :: l) ++ acc all: simpl.A: Type
forall acc : list A, acc = acc
A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
forall acc : list A, fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc all: intros acc.A: Type
acc: list A
acc = acc
A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc
  -A: Type
acc: list A
acc = acc reflexivity.
  -A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
fast_rev l (a :: acc) = (rev l ++ [a]) ++ acc rewrite IHl.A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = (rev l ++ [a]) ++ acc rewrite <- app_assoc.A: Type
a: A
l: list A
IHl:= forall acc: list A, fast_rev l acc = rev l ++ acc
acc: list A
rev l ++ a :: acc = rev l ++ [a] ++ acc reflexivity.
Qed.fast_rev_eq_alt is defined