(*|
=============
Week 1: Intro
=============

Author
  Aurèle Barrière.

Inspiration from Software Foundations and a previous lecture by Nate Foster.

.. contents::

Types and functions
===================

In this class, we'll use Rocq to write programs, and prove things about them!
Rocq has three languages: one for commands (the “Vernacular”), one for terms (“Gallina”), and one for proof tactics (“Ltac”).

Let's start by defining a custom type in Gallina, an enumerated type.
We define the type `day`, which has seven constructors: seven possible values for this type.
|*)

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

(*|
So far this is just an enumerated type, like you would write an enum in C. But we'll see later that we can define much more complex types.

Now, let's write our first function in Gallina, with some pattern-matching. Note that functions have to be total, I have to provide a result for all possible values of the argument.
|*)

Definition next_weekday (d: day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

(*|
One way to check the result of executing our function is to use the vernacular command `Compute`. Another way could be to extract our Rocq functions into OCaml or Haskell!
|*)

Compute (next_weekday friday). (* .unfold *)

(*|
Another way is to prove that the execution of my function gives the expected result. Here we'll see our first interactive proof buffer, with an horizontal line. Above the line are our hypotheses (in this particular proof, there aren't any. Below the line is our proof goal.
|*)

Theorem next_wed:
  next_weekday wednesday = thursday.
Proof.
  simpl. (* .unfold *)
  reflexivity.
Qed.

(*|
The `simpl` tactic simplifies the aplication of a function by following its definition. And `reflexivity` conclude when our goal is an equality were both sides are exactly the same.

Now, I want to prove that our function never returns a day that is part of the weekend. Let us start by defining which days are part of the weekend. This function takes a day and returns a boolean. I could define my own boolean type, just like I did for `day`. But this is part of the standard library already. Let's look at its definition with `Print`.
|*)

Print bool. (* .unfold *)

(*|
Now we can write our `weekend` definition, returning a boolean. Note that in many cases, Rocq can do some type inference and figure out some types by itself, I could remove all of the type annotations below and the definition would still be accepted.
|*)

Definition weekend (d: day) : bool :=
  match d with
  | saturday | sunday => true
  | _ => false
  end.

(*|
Gallina is strongly typed, every term has a type. We can check these types with `Check`. Of course, Rocq will reject ill-typed terms.
|*)

Check next_weekday. (* .unfold *)
Check (next_weekday monday). (* .unfold *)
Fail Check (next_weekday true). (* .unfold .fails *)

(*|
We are now ready for our proof, using the universal quantifier `forall` to quantify over any possible input to the function. This theorem is proved by case analysis over the input `d`. To do so, we use the tactic `destruct`. We use `-` to focus on the current sub-goal and structure our proofs.
|*)

Theorem next_not_weekend:
  forall (d: day), weekend (next_weekday d) = false.
Proof.
  intros d. (* .unfold *)
  destruct d. (* .unfold *)
  - (* .unfold *)
    simpl next_weekday. (* .unfold *)
    simpl weekend. (* .unfold *)
    reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

(*|
So far, we only defined a simple enumerated type. But we can define more complex abstract data types. let's define natural numbers and polymorphic lists. Natural numbers use an unary representation, where each number is either 0 or the successor of another natural.
|*)

Inductive mynat : Type :=
| O
| S (n:mynat).

Inductive mylist (X:Type) : Type :=
| nil: mylist X
| cons (x:X) (l:mylist X) : mylist X.

(*|
In fact, those definitions are already in the standard library. With `Search`, we can even search for definitions related to these types.
|*)

Print list. (* .unfold *)
Print nat. (* .unfold *)
Search list. (* .unfold *)
Search nat. (* Quite a large list of results! *)
Search (nat -> nat -> bool). (* .unfold *)
Search (nat -> nat -> nat).

(*|
Now let's introduce some more proof tactics. Here, we use `rewrite` to use an equality in our hypotheses. Note that using `rewrite <-` would rewrite the equality in the other direction.
|*)

Theorem plus_same :
  forall n m:nat,
    n = m ->
    n + n = m + m.
Proof.
  intros n m. (* .unfold *)
  intros H. (* .unfold *)
  rewrite H. (* .unfold *)
  reflexivity.
Qed.

(*|
In this proof, we use the keyword `as` to name the new terms introduce by case analysis. In that case, we need to name the natural of which `n` is a successor of.
|*)

Theorem plus_1_neq_0 : forall n : nat,
  Nat.eqb (n + 1) 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E. (* .unfold *)
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

(*|
Note that `destruct` typically forgets entirely about what we did case analysis on. We can remember that term and what it's equal to with the keyword `eqn:`.
|*)

Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

(*|
Propositions and Propositional Logic
====================================

We said that every term has a type, what is the type of the statements we've been proving?
|*)

Check (next_weekday wednesday = thursday). (* .unfold *)

(*|
Rocq has a special kind of type, named `Prop` to represent propositions, that we might try to prove. Note that not all propositions are true, they are just statements for which we may provide a proof. Propositions are a first-class entity in Rocq that can be defined, manipulated almost like any other type.
|*)

Definition false_prop: Prop :=
  3 = 2.

Theorem false_proof:
  3 = 2.
Proof.
  simpl. Fail reflexivity. (* .unfold .fails .no-goals *)
Abort.

Definition plus_claim : Prop := 2 + 2 = 4.
Check plus_claim. (* .unfold *)

(*|
We often define functions that create propositions. This defines properties of the arguments.
|*)

Definition is_three (n : nat) : Prop :=
  n = 3.
Check is_three. (* .unfold *)

Definition injective {A B:Type} (f : A ->  B) : Prop :=
  forall x y : A, f x = f y -> x = y.

(*|
Now that we have propositions, we can do propositional logic.
Let's see how we manipulate conjunctions, disjunctions and implications.
|*)

Example and_example : 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
  split. (* .unfold *)
  - reflexivity.
  - reflexivity.
Qed.

Example or_example: 1 = 2 \/ 3 + 9 = 12.
Proof.
  right. (* .unfold *)
  reflexivity.
Qed.

Theorem and_elim_left:
  forall A B, A /\ B -> A.
Proof.
  intros A B H.
  destruct H as [HA HB]. (* .unfold *)
  exact HA.
Qed.

Theorem or_commut:
  forall A B, A \/ B -> B \/ A.
Proof.
  intros A B H.
  destruct H as [HA | HB]. (* .unfold *)
  - right. exact HA.
  - left. exact HB.
Qed.

(*|
We can also have equivalences, which is in practice a conjunction of two implications.
|*)

Theorem and_commut:
  forall A B, A /\ B <-> B /\ A.
Proof.
  intros A B. split.
  - intros H.
    destruct H as [HA HB].
    split.
    + exact HB.
    + exact HA.
  - intros H.
    destruct H as [HB HA].
    split.
    + exact HA.
    + exact HB.
Qed.

(*|
To use an implication, the tactic `apply` allows us to match the conclusion of an hypothesis with the goal, and replace the goal with the premise of that implication. Note that we could also have made progress in the hypotheses instead of the goal using `apply ... in ...`. In fact, a lot of tactics can work on either the goal or the hypotheses. We can do both forward and backward reasoning, and often even meet in the middle.
|*)

Theorem modus_ponens:
  forall A B, (A -> B) -> A -> B.
Proof.
  intros A B Himpl HA.
  apply Himpl. (* .unfold *)
  (* apply Himpl in HA. *)
  apply HA.
Qed.

(*|
Finally, negation is defined as implying `False`. The `False` proposition is a proposition with no constructors, so we cannot construct a proof of it.
|*)

Print not. (* .unfold *)
Print True. (* .unfold *)
Print False. (* .unfold *)

Lemma exfalso_quodlibet:
  forall P, False -> P.
Proof.
  intros P H. (* .unfold *)
  contradiction.
Qed.

Lemma using_not:
  forall P, ~ P -> P -> False.
Proof.
  intros P Hnot HP.
  unfold not in Hnot.
  apply Hnot. apply HP.
Qed.

Theorem zero_not_one : 0 <> 1.
Proof.
  unfold not. intros. inversion H.
Qed.

Theorem double_neg:
  forall P, P -> ~~P.
Proof.
  unfold not. intros. apply H0. apply H.
Qed.

Theorem contrapositive:
  forall P Q,
    (P -> Q) ->
    (~Q -> ~P).
Proof.
  unfold not. intros P Q H H0 H1. apply H0. apply H. apply H1.
Qed.

(*|
Finally, let's see how we can work with quantifiers, universal and existential. We've seen that `intros` is useful when our goal is a `forall`. When we have a `forall` as an hypothesis, we can use `apply ... with` to use it, or `specialize` it.
|*)

Theorem forall_elim:
  forall A (f:A -> A),
  (forall x, f x = f (f x)) ->
  forall y, f (f y) = f (f (f y)).
Proof.
  intros A f Hinvol y.
  (* specialize (Hinvol (f y)). exact Hinvol.  *)
  apply Hinvol with (x:= f y).
Qed.

(*|
For existential quantifiers, we can use the `exists` tactic to provide a witness. And we can `destruct` an existential hypothesis to exhibit the witness.
|*)

Theorem exists_intro:
  forall (x: nat), exists y, y = x.
Proof.
  intros x. exists x. reflexivity.
Qed.

Theorem exists_elim:
  (exists x, x + 2 = 5) ->
  exists y, 3 * (y + 2) = 15.
Proof.
  intros H. destruct H as [x Hx].
  exists x. rewrite Hx. reflexivity.
Qed.