ssrinductive.v

From Corelib Require Import ssreflect.

(** Logical connectives and quantifiers *)

(* Universal quantification and implication *)
(* In the first tutorial, you have seen how to [move=>] when a goal
  starts with [forall] or is an implication. *)
Goal forall A: Prop, A -> A.
Proof.
  (* Use [move=> A H] to introduce proposition [A] and a proof of [A] named [H]
  in the context. *)

  (* If the goal matches an hypothesis in the context, you can use [assumption]
  to finish the goal. *)

(* Once you are done, replace [Admitted] with [Qed]. *)
Admitted.

(* When an implication is in the context, you can use the [apply:] tactic
  if its right-hand side matches the goal. *)
Goal forall A B: Prop, A -> (A -> B) -> B.
Proof.
  (* Start by introducing everything. *)
  move=> A B a H.

  (* [apply:] the implication on the goal with [apply: H]. *)

  (* Notice the goal has changed from [B] to [A]. Now you should be able to
  finish like previously. *)

Admitted.

(* Let's do it again in another way by combinig the two hypotheses on the
  fly to solve the goal. *)
Goal forall A B: Prop, A -> (A -> B) -> B.
Proof.
  (* Start by introducing everything. *)
  move=> A B a H.

  (* now apply [H] while providing [a] as an argument, by doing [apply: (H a)]. *)

  (* This was exactly what was expected as a goal, so the proof is complete. *)
Admitted.

(* Using hypotheses starting with a universal quantifier is the same as with
implications. Try solving the following goal with one of the previous methods. *)
Goal forall (X: Type) (P: X -> Prop) (a: X), (forall x, P x) -> P a.
Proof.

Admitted.

(* We will now see how to handle conjunction, both as a hypothesis and as a goal. *)
Goal forall A B: Prop, A /\ B -> B /\ A.
Proof.
  move=> A B H.
  
  (* Here you can try [apply: H] and see that it fails. In order to solve this,
  we first want to do [case] on the hypothesis [H] so that we obtain two hypotheses,
  one for each side. Try [case: H]. *)

  (* Now we want to prove the goal by proving one side, then the other. The
  tactic to achieve this is called [split]. *)

  (* We now have two distinct goals to prove, and you should be able to solve them. *)

Admitted.

(* We will now do the same with disjunction. *)
Goal forall A B: Prop, A \/ B -> B \/ A.
Proof.
  move=> A B H.

  (* In this case, we want to do a case analysis on [H]. The tactic is still
  [case: H]. *)

  (* This time the two goals appear at this point, one where [A] is true, the
  other when [B] is. *)
  (* When the goal is a disjunction, you can choose which side to prove using
  [left] and [right]. *)

Admitted.

(* One last tactic for this section: providing a witness to an existential
  quantifier. *)
Goal forall (X: Type) (P: X -> Prop) (x: X), P x -> exists (y: X), P y.
Proof.
  move=> X P x Px.

  (* If you need to prove a goal of the shape [exists _, _], you can use the
  tactic [exists] to provide a witness. Try [exists x]. *)

Admitted.

(* If the existential quantifier is in a hypothesis, you can use [case]
just like before. *)
(* The next goal involves [bool], the type of booleans, with two elements:
[true] and [false]. *)
(* Hint: you can use [case] on a boolean for a case analysis. *)
Goal forall (P: bool -> Prop), (exists x, P x) -> P true \/ P false.
Proof.

Admitted.

(* To conclude this section, a note on negation: the negation of [A], noted [~A],
is defined as [A -> False]. With this information, you can prove the next goal. *)
Goal forall (A: Prop), A -> ~~A.
Proof.

Admitted.




(** Inductive types *)

(* As was shown during the first tutorial, the type [nat] of natural numbers
  is defined with two rules, called constructors.
*)

(* Look at the output of this command to see the definition of [nat] *)
Print nat.

(* [O] is the constructor corresponding to 0, and [S] is for successor.
  The type of natural numbers is the smallest type generated by those two
  constructors.
*)

(* Functions on inductive types are often recursive. To define a recursive
  function, you can use [Fixpoint], like in this example. *)

Fixpoint add (n m: nat): nat := match n with
  | O => m
  | S n' => S (add n' m)
  end.
  
(* We use the [match _ with _ end] to look at the "shape" of the first argument
  (its head constructor), and act accordingly.
  If we are in the case [0 + m], we return [m].
  If we are in the case [(n' + 1) + m], we return [(n' + m) + 1].
*)

(* Note: Rocq has a safeguard against infinite recursion: it requires one argument
  to be strictly smaller in any recursive call. Managing this requirement is out
  of the scope of this tutorial, so we will stay on simple cases.
*)

(* You have seen in the first tutorial how to do proofs by induction, using the
  [elim] tactic. For an example, see [addn0] in [ssrnat_solution.v].
  Using this tactic, one goal will be generated for each constructor, with an
  induction hypothesis for every argument of the constructor that is of the
  same type.
*)

(** Lists *)

From Stdlib Require Import List.
Import ListNotations.

(* You can try to define an inductive type for lists, in the same way as
  [nat]. The difference is that lists hold elements of a certain type, which
  is given as an argument named [A] here.
*)

(* Uncomment the following block, and define the two constructors. *)
(*Inductive list' (A: Type) :=
  | (* The empty list *)
  | (* The [cons] operator, adding an element of type [A] at the beginning *)
.*)

(* You can now check you answer against the actual implementation of lists. *)
Print list.

(* We can use the following notations for lists:
  "[]" is [nil]
  "x :: l" is [cons x l]
  "[a; b; c]" is [cons a (cons b (cons c nil))]. *)

(* We will now define some functions on lists. *)

(* First, the [append] function, which concatenates two lists.
  Hint: this is essentially addition for lists, so it is very similar to [add].
*)

(* Fixpoint append .. *)

(* This is of course part of the standard library, so we will now use the
notation "l1 ++ l2" for the concatenation of [l1] and [l2]. *)

(* Next, the [rev] function, which reverses the order of elements in a list. *)

(* Fixpoint rev ... *)

(* Now we are going to prove the following result by induction. *)

Goal forall A (l1 l2: list A), rev A (l1 ++ l2) = rev A l2 ++ rev A l1.
Proof.
  (* Start by introducting the variables *)
  move=> A l1 l2.

  (* Now given that append is defined by matching on [l1], we will do the same
  in our proof, and do an induction on l1. *)

  (* First case: l1 is the empty list [nil] (the first constructor) *)
  (* Hint: you can use the following result in your proof, using
  the [rewrite] tactic. If you don't remember it, look at the second goal
  of [nat_solution.v]. *)
  Check app_nil_r.

  (* Now [append] should be able to reduce [([] ++ l2)] into [l2],
  we can use [simpl] to tell it to do so. *)

  (* We can conclude with [reflexivity]. *)
  
  (* Second case: [l1] has been replaced with [a :: l1] (the second constructor). *)
  (* There is also a new hypothesis: since [cons] has an argument which is a [list],
    Rocq generates an induction hypothesis for this argument. *)
  
  (* look at the following results: *)
  Check app_comm_cons.
  Check app_assoc.

  (* Now use [rewrite] to solve this goal, and don't forget to [simpl] when you
  want [rev] to do a step! *)

Admitted.


(* A type can be defined using the [Inductive] keyword without actually being
inductive. Look at the following definitions for example. *)

(* This is the [option] type, also known as the Maybe monad. Given a type [A],
the elements of [option A] are [Some a] with [a] in [A] and [None]. This type
is often used to replace errors, by returning [None] when something is wrong. *)
Print option.

(* These are the direct sum and product for types. *)
Print sum.
Print prod.

(* We used [elim] for proofs in this section, however when an induction
hypothesis is not needed, you can simply use [case], like in the first section.
Indeed, everything we [case]ed was an inductive type! *)
(* Some of them have only one constructor, so they only generate more hypotheses,
such as [/\] and [exists _, _]. *)
Print and.
Print ex.
(* Some others have several constructors, and generate several goals, such as
[\/] or [bool]. *)
Print or.
Print bool.


(* A crucial property of type constructors is that they are injective. This means
that, in [option A], if [Some a = Some a'] then [a = a']. In addition, two
elements of a type can only be equal if they start with the same constructor.
For example, in [option A], [Some a = None] can never be true. *)

(* Let's see this with the following goals. *)
Goal forall (A: Type) (x1 x2: A) (l1 l2: list A),
  x1 :: l1 = x2 :: l2 -> x1 = x2 /\ l1 = l2.
Proof.
  move=> A x1 x2 l1 l2 H.

  (* The tactic to use the injectivity of constructors is once again [case].
  Try [case: H]. *)

Admitted.

Goal forall (A: Type) (x: A) (l: list A), x :: l = [] -> False.
Proof.
  move=> A x l H.

  (* The tactic to show that [H] is a contradiction is [discriminate].
  You can give [H] as an argument to the tactic, but it is also able to find
  it by itself. *)

Admitted.


(* Define the [head] function on lists, which returns [None] if the list
is empty, and [Some x] if it isn't, with [x] the first element of the list. *)
(* We don't need recursion for this function, so you should define it with
[Definition] instead of [Fixpoint]. *)

(* Definition head ... *)

(* Now prove the following goals. *)

Goal forall (A: Type) (l: list A), head A l = None -> l = [].
Proof.

Admitted.

Goal forall (A: Type) (l: list A), forall x, head A l = Some x
  -> exists l', l = x :: l'.
Proof.

Admitted.

(* Hint: if you have a contradiction in your context, you can use [contradiction]. *)
Goal forall (A: Type) (l l1 l2: list A), ~ l = nil
  -> head A (l ++ l1) = head A (l ++ l2).
Proof.

Admitted.


Require Import PeanoNat Init.
(** Binary trees *)
(* Define a type for binary trees, which can either be empty or a node with two
chlidren. *)

(* Inductive BTree := ... *)

(* Define a function computing the height of a binary tree. *)

(* Hint: there is a [max] function. *)
(* Fixpoint height ... *)

Goal forall (t: BTree), height t = 0 -> t = Empty.
Proof.
Admitted.

(* Define a function computing the size of a binary tree. *)

(* Fixpoint size ... *)

(* Now prove the following goal with these hints. *)

(* You can use this lemma, proven by magic. *)
Require Import Lia.
Lemma S_plus_lt: forall a b c d: nat, a < c -> b < d -> S (a + b) < c + d.
  lia.
Qed.
(* And look at the following results. *)
Check Nat.lt_0_1.
Check Nat.add_0_r.
Check Nat.lt_le_trans.
Check Nat.pow_le_mono_r.
Check Nat.le_max_l.
Check Nat.le_max_r.

Goal forall (t: BTree), size t < 2 ^ (height t).
Proof.
Admitted.