PRFA.live_coding2

Live coding session for the second lecture of MPRI PRFA (2-7-2)

This time we will look at inductive types. If you already know algebraic data types from OCaml or Haskell then it shouldn't be too surprising. If you don't, don't worry we'll explain.

Set Default Goal Selector "!".

Module define_nat.

Inductive types can be defined using the Inductive keyword.
Below, we give the definition of nat. It's exactly the same definition as the one you have used before.
Basically, you can read the following as introducing the type nat which is made of: either O or of S n for some n : nat.
In BNF (Backus-Naur-form) one would write
n : nat ::= O | S n
You can then think of nat as the type containing O and S O and then S (S O) and so on…
  Inductive nat : Type :=
  | O : nat
  | S : nat → nat.

  Check nat.
  Check O.
  Check S.

Slightly different notations for introducing constructors exist. We are using modules to be able to define them without name clashes - that's the only purpose we will use modules for in this course so you don't really have to learn about them.

  Module variant1.

In this variant, we write S (n : nat) : nat instead of S : nat → nat to specify that S takes a natural number argument.
    Inductive nat :=
    | O : nat
    | S (n : nat) : nat.

  End variant1.

  Module variant2.

This more compact version doesn't even specify that O and S n must be of type nat, Coq already knows this.
    Inductive nat := O | S (n : nat).

  End variant2.

An inductive type is the smallest type closed under the type constructors. This is reflected in the induction principle:
  Check nat_ind.

For nat this is the induction on natural numbers you know probably since high school.
We can define recursive functions operating on inductive arguments with the Fixpoint keyword.
  Fixpoint add (n m : nat) {struct n} :=
    (* the match keyword allows case analysis on terms of an inductive type *)
    match n with
    | O ⇒ m
    | S n ⇒ S (add n m)
      (* Recursion has to be performed on a structurally smaller argument
        (see the {struct n} annotation above telling Coq that n is the one
        that is structuallt decreasing) *)
    end.

Note that there are other ways to define functions using more complex recursion patterns - you will learn about them soon
Note how the following evaluates to fun m ⇒ m
  Eval simpl in (fun m ⇒ add O m).

However, the following expression cannot be simplified using computation
  Eval simpl in (fun n ⇒ add n O).

  (*** Instead, we can prove this equation **)
  Lemma add_0 n :
    add n O = n.
  Proof.
    induction n as [| n IHn].
    - reflexivity.
    - simpl. rewrite IHn. reflexivity.
  Qed.

  (* We can introduce infix notations as follows: *)
  Infix "+" := add.

  Check add_0.

  Lemma add_S n m :
    add n (S m) = S (add n m).
  Proof.
    induction n as [| n IHn].
    - reflexivity.
    - simpl. rewrite IHn. reflexivity.
  Qed.

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.

Note that we did not provide a {struct _} argument here because Coq can infer it automatically.

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

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

  Lemma add_sub n m :
    (n + m) - n = m.
  Proof.
    induction n.
    - cbn. destruct m. all: reflexivity.
    - assumption.
  Qed.

In Coq, everything is computational, including propositions. We can define
  Definition is_zerob (n : nat) : bool :=
    match n with
    | O ⇒ true
    | S n ⇒ false
    end.

but also
  Definition is_zero (n : nat) : Prop :=
    match n with
    | O ⇒ True
    | S n ⇒ False
    end.

In general, constructors are different from each other
  Lemma S_O n :
    S n ≠ O.
  Proof.
    (* This can be proved manually *)
    intros E.
    (* We use the change tactic to change the goal to something equivalent
      w.r.t. computation *)
    change (is_zero (S n)).
    (* We can simplify again to get the old goal *)
    simpl.
    change (is_zero (S n)).
    rewrite E.
    simpl.
    split.
  Qed.

There is also a tactic to automatically discharge such goals
  Lemma S_0' n :
    S n ≠ O.
  Proof.
    discriminate.
  Qed.

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 so that by congruence (f_equal) we 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.

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.
  Proof.
    intros E.
    change (pred (S n) = m).
    rewrite E.
    reflexivity.
  Qed.

We could in fact do it without pred
  Lemma S_inj_2 n m :
    S n = S m → n = m.
  Proof.
    intros E.
    change (match S n with O ⇒ True | S n ⇒ n = m end).
    rewrite E.
    reflexivity.
  Qed.

We can also use the f_equal lemma (not the tactic!)
  Lemma S_inj_3 n m :
    S n = S m → n = m.
  Proof.
    Check f_equal.
    intros E.
    apply (f_equal pred) in E.
    assumption.
  Qed.

Finally, we have tactics that do this automatically such as inversion
  Lemma S_inj_4 n m :
    S n = S m → n = m.
  Proof.
    intros E.
    inversion E.
    reflexivity.
  Qed.

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.

We're going to prove that it indeed decides equality of natural numbers.
  Lemma eq_nat_spec n m :
    eq_nat n m = true ↔ n = m.
  Proof.
    induction n as [ | n' IH]. all: simpl.
    - destruct m. all: simpl.
      + split. all: reflexivity.
        (* Notice reflexivity is able to conclude A → 0 = 0 for any A *)
      + split. all: intros E. all: discriminate E.
    - destruct m.
      + split. all: discriminate.
      + (* We are 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.

Let's try again.
  Lemma eq_nat_spec n m :
    eq_nat n m = true ↔ n = m.
  Proof.
    (* We revert m back into the goal *)
    revert m.
    induction n as [ | n' IH]. all: intro m.
    - destruct m. all: simpl.
      + split. all: reflexivity.
      + split. all: discriminate.
    - (* This way the IH is quantified for all m *)
      destruct m. all: simpl.
      + split. all: discriminate.
      + split. all: intros E.
        × apply IH in E. rewrite E. reflexivity.
        × apply IH. inversion E. reflexivity.
  Qed.

End define_nat.

Booleans are even simpler.

Module define_bool.

  Inductive bool := true | false.

  Check true.
  Check bool. (* Set is basically the same as Type, so bool is a type. *)

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.

Again, since it's an inductive type, the constructors are disjoint.
  Lemma true_false :
    true ≠ false.
  Proof.
    discriminate.
  Qed.

End define_bool.

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

Module define_prod.

We define product types inductively with one constructor taking two arguments.
  Inductive prod X Y :=
  | pair (x : X) (y : Y).

Note how the constructor pair takes 4 arguments:
  Check pair.
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 Coq.
  Check pair nat.

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.

  Check pair'.

Also, the type arguments have to be passed.
  Fail Check pair' 0 0.

However, we can declare arguments as implicit using the Arguments command by marking implicit arguments with braces (or squigly brackets {}).
  Arguments pair' {X} x {Y} y.

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

We can use the following command to force Coq to print implicit arguments.
  Set Printing Implicit.

There we can the nat that have been inferred.
  Check pair' 0 0.

We reactivate the printing of 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.

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.

End define_prod.

Module define_list.

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.

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).
  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'
  Check list_ind.

End define_list.

Proofs by induction

We import Coq's list library
From Coq Require Import List.

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.
About rev.

Lemmas about lists we typically prove by induction as we did for natural numbers.
Lemma app_nil_r A (l : list A) :
  l ++ nil = l.
Proof.
  induction l. all: simpl.
  - reflexivity.
  - f_equal. assumption.
Qed.

Lemma rev_app_distr {A} (l1 l2 : list A) :
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  induction l1 as [| a l IHl]. all: simpl.
  - rewrite app_nil_r. reflexivity.
  - (* For rewrite we can separate two lemmas to rewrite by a comma. *)
    rewrite IHl, app_assoc. reflexivity.
Qed.

Lemma rev_rev {A} (l : list A) :
  rev (rev l) = l.
Proof.
  induction l. all: simpl.
  - reflexivity.
  - rewrite rev_app_distr. simpl. rewrite IHl. reflexivity.
Qed.

The rev defined above is not very smart because it use 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.

We can show the two behave the same.
Lemma fast_rev_eq {A} (l : list A) :
  fast_rev l nil = rev l.
Proof.
  induction l. all: simpl.
  - reflexivity.
  - (* 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.
Proof.
  (* We prove a more lemma locally *)
  assert (H : ∀ acc, fast_rev l acc = rev l ++ acc).
  { induction l as [| a l IHl]. all: simpl. all: intros acc.
    - reflexivity.
    - rewrite IHl. rewrite <- app_assoc. reflexivity.
  }
  rewrite H. Search app nil. rewrite app_nil_r. reflexivity.
Qed.

We can prove things in a different way.
Lemma fast_rev_eq_alt {A} (l : list A) :
  fast_rev l nil = rev l.
Proof.
  (* We are going to generalise the empty list to any acc. *)
  rewrite <- app_nil_r. generalize (@nil A) as acc.
  induction l as [| a l IHl]. all: simpl. all: intros acc.
  - reflexivity.
  - rewrite IHl. rewrite <- app_assoc. reflexivity.
Qed.

Dependent pairs


Module define_sigma.

We define the type of dependent pairs, where the second component can depend on the first. We often call those Σ-types (hence the name sigT).
  Inductive sigT {A} (B : A → Type) :=
  | existT (a : A) (b : B a) : sigT B.

  Arguments existT {A B}.

For instance, we can create a type of pairs, where the first component is always a boolean b, but the second is of type nat when b is true and of type list nat otherwise.
  Definition T := sigT (fun (b : bool) ⇒ if b then nat else list nat).

  Definition pair1 : T :=
    existT true 17.

  Definition pair2 : T :=
    existT false [ 90 ; 4 ; 8 ].

Do you understand the induction principle?
  Check sigT_ind.

End define_sigma.

We are now going to use the definition from the standard library.

Arguments existT {A P}.

Similar to how a function of type A × B → C is the same as A → B → C (which we call currying), we can turn a function of type sigT {A} B → C to a (dependent) function of type ∀ (x : A), B x → C.
Notice that ∀ can work for dependent functions and not just for propositions.
Definition cur {A} {B : A → Type} {C} (f : sigT B → C) :
  ∀ (x : A), B x → C :=
  fun a b ⇒ f (existT a b).

We can perform the opposite transformation.
Definition car {A} {B : A → Type} {C} (f : ∀ x, B x → C) :
  sigT B → C :=
  fun p ⇒
    match p with
    | existT a b ⇒ f a b
    end.

And now we can prove that they are indeed inverse of each other.
Lemma car_cur :
  ∀ A (B : A → Type) C (f : sigT B → C) p,
    car (cur f) p = f p.
Proof.
  intros A B C f p.
  (* Notice that { x : A & B x } is a notation for sigT B. *)
  destruct p as [a b]. reflexivity.
Qed.

And now the other direction.
Lemma cur_car :
  ∀ A (B : A → Type) C (f : ∀ (x : A), B x → C) a b,
    cur (car f) a b = f a b.
Proof.
  intros A B C f a b.
  (* This time there is nothing to destruct, the proof is direct. *)
  reflexivity.
Qed.

Polymorphic iteration

We will now have a look at iter, a function such that iter f n x applies n times the function f, starting with the argument x. For instance iter f 2 x is f (f x).
We will start by importing some lemmas and definitions from the Nat library.

Require Import Nat.

Fixpoint iter {A : Type} (f : A → A) (n : nat) (x : A) : A :=
  match n with
  | 0 ⇒ x
  | S n' ⇒ f (iter f n' x)
  end.

We can show that iterating the successor n times is the same as adding n.
Lemma iter_add :
  ∀ n x,
    n + x = iter S n x.
Proof.
  intros n x.
  induction n as [|n IH]. all: simpl.
  - reflexivity.
  - f_equal. assumption.
Qed.

Similarly, multiplication is iterated addition.
Lemma iter_mul :
  ∀ n x,
    n × x = iter (add x) n 0.
Proof.
  intros n x.
  induction n as [|n IH]. all: simpl.
  - reflexivity.
  - f_equal. assumption.
Qed.

Indexed inductive types

We can define predicates using the Inductive keyword as well
Inductive even : nat → Prop :=
| evenO : even 0
| evenS n : even n → even (S (S n)).

Being inductive, their proofs can be constructed using the constructor tactic.
Note: The Goal command is similar to Lemma except it doesn't require a name for a lemma which is useful when just checking things that are not useful later such as the fact the 4 is even…
Goal even 4.
Proof.
  constructor. constructor. constructor.
Qed.

Case analysis works using inversion
Goal ¬ even 3.
Proof.
  intros h.
  inversion h.
  (* Here we learnt from even 3 that to build it we must have had even 1
    first. *)
  inversion H0.
  (* But there is no rule (neither evenO nor evenS) that can _unify_ with
    even 1 so there is no goal left, we are done!
  *)
Qed.

inversion is useful but it is hard to predict its behaviour and to name the resulting hyoptheses. So we might want to use regular case analysis instead, ie. use destruct.
Goal ¬ even 3.
Proof.
  intro h.
  destruct h.
  (* Here this quite terrible because destruct completely forgets about
    the fact we had 3 so we are left with an unprovable goal.
  *)
Abort.

There is a way to recover this information by telling Coq to remember it as an equality using the remember tactic.
Goal ¬ even 3.
Proof.
  intro h.
  remember 3 as n eqn: e.
  destruct h.
  - (* See that n has been replaced by 0 but since we also kept the
      equality e we know this case is impossible.
    *)
    discriminate.
  - (* In the other branch, we have that 3 must be 2 + n for some even n
      which is also impossible but requires noticing that n must be 1.
      inversion on the equality will give us that.
    *)
    inversion e.
    (* We can then use subst to automatically substitute n by 1. *)
    subst.
    (* We can now rely on inversion again to discharge the goal. *)
    inversion h.
Qed.

Rather than an inductive predicate, we can also define a boolean function that checks whether its argument is even.
Fixpoint evenb n :=
  match n with
  | 0 ⇒ true
  | 1 ⇒ false
  | S (S n) ⇒ evenb n
  end.

We can show that the two are equivalent.
Lemma even_to_evenb :
  ∀ n, even n → evenb n = true.
Proof.
  intros n h.
  (* We can perform induction on the proof! *)
  induction h.
  - reflexivity.
  - simpl. assumption.
Qed.

And now the other direction.
Lemma evenb_to_even :
  ∀ n, evenb n = true → even n.
Proof.
  intros n h.
  (* This time we have to perform the induction on n *)
  induction n as [ | n ih].
  - constructor.
  - destruct n.
    + simpl in h. discriminate.
    + constructor.
      (* Note how we are stuck here: The inductive hypothesis talks about S n
        instead of n. But this we cannot generalise. *)
Abort.

The solution is to use a stronger form of induction that lets you conclude about any smaller argument. We'll require Lia to help us deal with some arithmetic goals.

Require Import Lia.

Lemma strong_nat_ind :
  ∀ (P : nat → Prop),
    (∀ n, (∀ m, m < n → P m) → P n) →
    ∀ n, P n.
Proof.
  intros P h n.
  assert (hn : ∀ m, m ≤ n → P m).
  { induction n as [| n ih].
    - intros m hm. inversion hm.
      apply h. intros k hk. lia. (* lia knows there can't be k < 0 *)
    - intros m hm. inversion hm.
      + apply h. intros k hk. apply ih. lia.
      + apply ih. lia.
  }
  apply hn. lia.
Qed.

Back to even.
Lemma evenb_to_even :
  ∀ n, evenb n = true → even n.
Proof.
  intros n h.
  induction n as [n ih] using strong_nat_ind.
  (* We have to consider the cases 0, 1 and S (S n). *)
  destruct n as [| [| n]].
  - constructor.
  - simpl in h. discriminate.
  - simpl in h. constructor.
    apply ih.
    + lia.
    + assumption.
Qed.

The "less than" predicate ≤ we have used above is defined as follows.
The idea is that n ≤ n always holds, and if n ≤ m then n ≤ S m. In other words, if you can remove successors S from m and reach n then n ≤ m.
Inductive le : nat → nat → Prop :=
| leO n : le n n
| leS n m : le n m → le n (S m).

We build the proof as hinted above, by removing S from 5 until we reach 3 which takes only two steps.
Goal le 3 5.
Proof.
  constructor. constructor. constructor.
Qed.

To show that 1 is now below 0 we can use inversion again.
Goal ¬ le 1 0.
Proof.
  intros h. inversion h.
Qed.

As for even we can also do it more manually.
Goal ¬ le 1 0.
Proof.
  intros h. remember 1 as n1 eqn: e1. remember 0 as n0 eqn: e0.
  destruct h.
  - subst. discriminate.
  - subst. discriminate.
Qed.

As a sanity check, we can verify the following property.
Below ∃ (x : A), P x is very similar to sigT P except that P x is a proposition. We can prove ∃ x, P x by eg. using ∃ 0 and then proving P 0.
Lemma le_iff :
  ∀ n m,
    le n m ↔ ∃ k, k + n = m.
Proof.
  intros n m.
  split.
  - intros h. induction h as [n | n m h ih].
    + ∃ 0. reflexivity.
    + destruct ih as [k ih]. subst.
      ∃ (S k). simpl. reflexivity.
  - (* Instead of doing intro x and then destruct x as [a b] we can do
      intros [a b]. *)
    intros [k h]. subst.
    induction k as [| k ih].
    + simpl. constructor.
    + simpl. constructor. assumption.
Qed.

We can also show transitivity.
Lemma le_trans :
  ∀ n m k,
    le n m →
    le m k →
    le n k.
Proof.
  intros n m k hnm hmk. induction hmk as [ m | m k hmk ih ].
  - assumption.
  - constructor. apply ih. assumption.
Qed.

We can also define the notion of reflexive transitive closure of a relation R : A → A → Prop on A like so.
Inductive rtclos {A} (R : A → A → Prop) : A → A → Prop :=
| refl x : rtclos R x x
| incl x y : R x y → rtclos R x y
| trans x y z : rtclos R x y → rtclos R y z → rtclos R x z.

Arguments trans {A R}.

Then le is just the closure of being the successor.
Lemma le_rtclos :
  ∀ n m,
    le n m ↔ rtclos (fun n m ⇒ m = S n) n m.
Proof.
  intros n m.
  split.
  - intros h. induction h as [ n | n m h ih ].
    + constructor.
    + (* If we just apply constructor then it's going to pick incl
        which is not what we want. What we want is to use trans: *)
      apply (trans _ m _). 1: assumption.
      (* We just applied assumption to the first goal this way. *)
      (* It can be nicer than having many levels of nested bullets. *)
      constructor. reflexivity.
  - intros h. induction h as [ n | n m h | n m k hnm ihnm hmk ihmk ].
    + constructor.
    + subst. constructor. constructor.
    + apply (le_trans _ m _). all: assumption.
Qed.