Require Import Nat Arith List ssrbool.
Import ListNotations.

(* ################################################ *)
(** ** Warming up: induction on natural numbers *)

(** You can use the stdlib variants of lemmas proven in lecture 1: *)
About Nat.add_0_r.
About Nat.add_succ_r.
About Nat.add_comm.

(** Show that addition is associative *)

Lemma add_assoc (m n p : nat) : m + (n + p) = (m + n) + p.
Proof.
  induction m ; cbn.
  - reflexivity.
  - now rewrite IHm.
Qed.

(** Show that multiplication is commutative — you might need additional lemmas! *)

Lemma mul_0_r m : m * 0 = 0.
Proof.
  induction m ; cbn.
  - reflexivity.
  - assumption.
Qed.

Lemma mul_succ_r (m n : nat) : n * S m = n + n * m.
Proof.
  induction n ; cbn.
  - reflexivity.
  - rewrite IHn.
    f_equal.
    rewrite !add_assoc.
    f_equal.
    apply Nat.add_comm.
Qed.

Lemma mul_comm (m n : nat) : m * n = n * m.
Proof.
  induction m ; cbn.
  - rewrite mul_0_r.
    reflexivity.
  - rewrite IHm.
    rewrite mul_succ_r.
    reflexivity.
Qed.

(* ################################################ *)
(** ** A bit of (classical) logic *)

(** Show the following constructively valid theorems. *)

(** The first two were done in class,
  go check them if needed, but try yourself
  first *)
Theorem contraposite (P Q : Prop) : (Q -> P) -> ~ P -> ~ Q.
Proof.
  intros Hi Hp Hq.
  apply Hp, Hi, Hq.
Qed.

Theorem double_neg (P : Prop) : P -> ~ (~ P).
Proof.
  intros p np.
  apply np, p.
Qed.

Theorem dist_exists_or (X:Type) (P Q : X -> Prop) :
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
  split.
  - intros [x [|]].
    1: left.
    2: right.
    all: now exists x.
  - intros [[x]|[x]].
    all: exists x ; auto.
Qed.

Theorem de_morgan_or (P Q : Prop) : ~ (P \/ Q) -> ~ P /\ ~ Q.
Proof.
  intros Hneg.
  split.
  all: intros H.
  all: apply Hneg ; auto.
Qed.

Theorem de_morgan_ex (A : Type) (P : A -> Prop) : ~ (exists x, P x) -> forall x, ~ (P x).
Proof.
  intros Hneg x Hx.
  apply Hneg.
  now exists x.
Qed.

Theorem excluded_middle_irrefutable (P : Prop) : ~ ~ (P \/ ~ P).
Proof.
  intros Hneg.
  apply Hneg.
  right.
  intros Hp.
  apply Hneg.
  left.
  assumption.
Qed.

(** Show the equivalence of these various ways of phrasing classical logic. *)

Definition excluded_middle := forall P : Prop, P \/ ~ P.

Definition peirce := forall P Q: Prop, ((P -> Q) -> P) -> P.

Definition double_negation_elimination := forall (P:Prop),  ~ ~ P -> P.

Definition de_morgan_not_and_not := forall (P Q:Prop), ~(~ P /\ ~ Q) -> P \/ Q.

Definition implies_to_or := forall (P Q:Prop), (P -> Q) -> (~ P \/ Q).

Definition consequentia_mirabilis := forall P:Prop, (~P -> P) -> P.

Lemma em_peirce : excluded_middle -> peirce.
Proof.
  unfold excluded_middle, peirce.
  intros em P Q H.
  destruct (em P) as [|Hneg].
  1: easy.
  apply H.
  intros p.
  now exfalso.
Qed.

Lemma peirce_dneg : peirce -> double_negation_elimination.
Proof.
  unfold peirce, double_negation_elimination.
  intros peirce P nnP.
  apply (peirce _ False).
  intros Hneg.
  exfalso.
  easy.
Qed.

Lemma dneg_de_morgan : double_negation_elimination -> de_morgan_not_and_not.
Proof.
  unfold double_negation_elimination, de_morgan_not_and_not.
  intros dneg P Q H.
  apply dneg.
  intros Hneg.
  apply de_morgan_or in Hneg.
  auto.
Qed.

Lemma de_morgan_implies : de_morgan_not_and_not -> implies_to_or.
Proof.
  unfold de_morgan_not_and_not, implies_to_or.
  intros Hmor P Q Hi.
  apply Hmor.
  intros [Hp Hq].
  eapply Hp, contraposite ; eauto.
Qed.

Lemma implies_mirabilis : implies_to_or -> consequentia_mirabilis.
Proof.
  unfold implies_to_or, consequentia_mirabilis.
  intros Hor P Hp.
  specialize (Hor P P) as [].
  all: auto.
Qed.

Lemma mirabilis_em : consequentia_mirabilis -> excluded_middle.
Proof.
  unfold consequentia_mirabilis, excluded_middle.
  intros Hmir P.
  apply Hmir.
  intros Hneg.
  right.
  intros Hp.
  apply Hneg.
  left.
  assumption.
Qed.

(* ################################################ *)
(** ** Discriminate, your way *)

(** How does one prove that [0 <> 1]? The key is the following function. *)

Definition disc (n : nat) :=
  match n with
  | 0 => True
  | S _ => False
  end.

(** Show the following theorem, without using [discriminate], [inversion], etc.
  Only [intros], [apply] and [rewrite] should suffice. You might also need [change]
  or [assert]. And of course, you will want to use [disc] in a crucial way. *)

Lemma disc_use : 0 <> 1.
Proof.
  intros He.
  change (disc 1).
  rewrite <- He.
  easy.
Qed.

(* ################################################ *)
(** ** Subsequences (from Software Foundations)

A list is a _subsequence_ of another list if all of the elements
in the first list occur in the same order in the second list,
possibly with some extra elements in between. For example,

  [1;2;3]

is a subsequence of each of the lists

  [1;2;3]
  [1;1;1;2;2;3]
  [1;2;7;3]
  [5;6;1;9;9;2;7;3;8]

but it is _not_ a subsequence of any of the lists

  [1;2]
  [1;3]
  [5;6;2;1;7;3;8].

- Define an inductive proposition [subseq] on [list nat] that
  captures what it means to be a subsequence. (Hint: You'll need
  three cases.)

- Prove [subseq_refl] that subsequence is reflexive, that is,
  any list is a subsequence of itself.

- Prove [subseq_app] that for any lists [l1], [l2], and [l3],
  if [l1] is a subsequence of [l2], then [l1] is also a subsequence
  of [l2 ++ l3].

- (Harder) Prove [subseq_trans] that subsequence is
  transitive -- that is, if [l1] is a subsequence of [l2] and [l2]
  is a subsequence of [l3], then [l1] is a subsequence of [l3]. *)

  Inductive subseq : list nat -> list nat -> Prop :=
  | sub_empty l : subseq [] l
  | sub_keep x l l' : subseq l l' -> subseq (x :: l) (x :: l')
  | sub_drop x l l' : subseq l l' -> subseq l (x :: l').
  
  Theorem subseq_refl : forall (l : list nat), subseq l l.
  Proof.
    intros l.
    induction l.
    all: now constructor.
  Qed.

  Theorem subseq_app (l1 l2 l3 : list nat) :
    subseq l1 l2 ->
    subseq l1 (l2 ++ l3).
  Proof.
    intros H.
    induction H in l3 |- *.
    all: cbn ; constructor ; eauto.
  Qed.

  Theorem subseq_trans (l1 l2 l3 : list nat) :
    subseq l1 l2 ->
    subseq l2 l3 ->
    subseq l1 l3.
  Proof.
    intros H H'.
    induction H' in l1, H |- *.
    - inversion H ; subst.
      now constructor.
    - inversion H ; subst.
      all: constructor ; eauto.
    - constructor.
      eauto.
  Qed.

(** An alternative, more complicated proof, if you do the induction on the other side. *)


  Theorem subseq_app_r (l1 l2 l3 : list nat) :
    subseq l1 l3 ->
    subseq l1 (l2 ++ l3).
  Proof.
  intros H.
  induction l2 ; cbn ; auto.
  now constructor.
  Qed.

  Theorem subseq_inv (x : nat) (l l' : list nat) :
    subseq (x :: l) l' ->
    exists l1 l2, subseq l l2 /\ l' = l1 ++ x :: l2.
  Proof.
  intros H.
  remember (x :: l) as lcons eqn:He.
  induction H in x, l, He |- *.
  - inversion He.
  - injection He ; intros ; subst.
    eexists [], _ ; split ; cbn ; eauto.
  - subst.
    edestruct IHsubseq as (l1&l2&Hs&->).
    1: reflexivity.
    eexists (_ :: _), _ ; split ; cbn ; eauto.
  Qed.

  Theorem subseq_trans' (l1 l2 l3 : list nat) :
    subseq l1 l2 ->
    subseq l2 l3 ->
    subseq l1 l3.
  Proof.
    intros H H'.
    induction H in l3, H' |- *.
    - constructor.
    - eapply subseq_inv in H' as (l1&l2&?&->).
      apply subseq_app_r.
      constructor ; eauto.
    - eapply subseq_inv in H' as (l1&l2&?&->).
      apply subseq_app_r.
      constructor ; eauto.
  Qed.

(* ################################################ *)
(** ** 100 versions of list membership *)

(** An inductive version *)

Inductive In_ind {A : Type} : A -> list A -> Prop :=
  | In_here a l : In_ind a (a :: l)
  | In_there a x l : In_ind a l -> In_ind a (x :: l).

(** A recursive version, computing a boolean *)

Fixpoint In_rec {A : Type} (eq : A -> A -> bool) (a : A) (l : list A) : bool :=
  match l with
  | [] => false
  | x :: l => (eq x a) || (In_rec eq a l)
  end.

(** A version based on indexing *)

Definition In_nth {A : Type} (a : A) (l : list A) :=
    exists (n : nat), nth_error l n = Some a.

(** A version based on counting *)

Fixpoint count {A : Type} (eq : A -> A -> bool) (a : A) (l : list A) : nat :=
  match l with
  | [] => 0
  | x :: l => let c := (count eq a l) in if (eq x a) then S c else c
  end.

Definition In_count {A : Type} (eq : A -> A -> bool) (a : A) (l : list A) :=
  1 <= count eq a l.

(** State and show that all versions are equivalent. You will have to assume some property of
  the [eq] function you pass to [In_rec]. *)

(** You'll probably want to use logical equivalence, written [A <-> B], which is
  simply an abbreviation for [A -> B /\ B -> B]. *)

Lemma In_ind_rec {A : Type} (eq : A -> A -> bool) (a : A) (l : list A) :
  (forall x y, reflect (x = y) (eq x y)) ->
  In_ind a l <-> In_rec eq a l.
Proof.
  intros Heq.
  split.
  - induction 1 ; cbn.
    + destruct (Heq a a) ; cbn.
      1: easy.
      easy.
    + rewrite IHIn_ind.
      apply orbT.
  - intros HIn.
    induction l as [|x l IH] in HIn |- * ; cbn in *.
    1: easy.
    destruct (Heq x a) ; cbn in *.
    + subst.
      constructor.
    + constructor.
      auto.
Qed.

Lemma In_rec_count {A : Type} (eq : A -> A -> bool) (a : A) (l : list A) :
  In_rec eq a l <-> In_count eq a l.
Proof.
  unfold In_count.
  induction l as [|x l IH] ; cbn.
  - split.
    1: easy.
    intros ?%Nat.nle_succ_0.
    easy.
  - destruct (eq x a) ; cbn.
    2: assumption.
    split ; try easy.
    intros _.
    apply le_n_S, Nat.le_0_l.
Qed.

Lemma In_ind_nth {A : Type} (a : A) (l : list A) :
  In_ind a l <-> In_nth a l.
Proof.
  split.
  - induction 1.
    + unfold In_nth.
      exists 0 ; reflexivity.
    + destruct IHIn_ind as [n].
      exists (S n) ; cbn.
      assumption.
  - destruct 1 as [n Hn].
    induction n in l, Hn |- *.
    + destruct l ; cbn in *.
      1: congruence.
      inversion Hn.
      constructor.
    + destruct l ; cbn in *.
      1: congruence.
      constructor.
      auto.
Qed.

(** Write corresponding versions of the
  [All : forall {A : Type} (P : A -> Prop) (l : list A), Prop]
  which assert that all elements of a list satisfy a certain property.
  For the "computable" versions, you can assume that [P : A -> bool]
  instead. *)

  Inductive All_ind {A : Type} (P : A -> Prop) : list A -> Prop :=
    | All_nil : All_ind P []
    | All_cons a l : P a -> All_ind P l -> All_ind P (a :: l).

  Fixpoint All_rec {A : Type} (p : A -> bool) (l : list A) : bool :=
    match l with
    | [] => true
    | a :: l => p a && All_rec p l
    end.

  Definition All_nth {A : Type} (P : A -> Prop) (l : list A) : Prop :=
    forall (n : nat) (a : A), nth_error l n = Some a -> P a.

  Fixpoint count' {A : Type} (p : A -> bool) (l : list A) : nat :=
    match l with
    | [] => 0
    | x :: l => let c := (count' p l) in if (p x) then S c else c
    end.
    
  Definition All_count {A : Type} (p : A -> bool) (l : list A) : Prop :=
    count' p l = length l.

(* ################################################ *)
(** ** Binary natural numbers *)
(** Exercise inspired by Software Foundation, Vol. 1 *)

(** Define the type of binary natural numbers as follows:
  - Z represents the "empty" binary representation /\ ~ Q.
  - B0 b and B1 b represent the binary number with low-order bit respectively with 0 or 1,
    and continuing with b
*)

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin)
.

(** Define the following increment function on bin *)

Fixpoint incr (m:bin) : bin :=
  match m with
  | Z => B1 Z
  | B0 b => B1 b
  | B1 b => B0 (incr b)
  end.

(** Use it to define a mapping *)

Fixpoint bin_to_nat (m:bin) : nat :=
  match m with
  | Z => 0
  | B0 b => 2*(bin_to_nat b)
  | B1 b => 1 + 2*(bin_to_nat b)
  end.


(** Prove that these definitions agree! You might want to design your definitions
  to make this easier… *)

Theorem bin_to_nat_pres_incr : forall b : bin,
  bin_to_nat (incr b) = 1 + bin_to_nat b.
Proof.
  induction b ; cbn.
  all: repeat rewrite Nat.add_0_r ; try reflexivity.
  rewrite IHb ; cbn.
  f_equal.
  rewrite Nat.add_succ_r.
  reflexivity.
Qed.

(** Write a function to convert natural numbers to binary numbers. *)

Fixpoint nat_to_bin (n:nat) : bin :=
  match n with
  | 0 => Z
  | S n' => incr (nat_to_bin n')
  end.

(** Prove that, if we start with any [nat], convert it to [bin], and
    convert it back, we get the same [nat] which we started with.

    Hint: This proof should go through smoothly using the previous
    exercise about [incr] as a lemma. If not, revisit your definitions
    of the functions involved and consider whether they are more
    complicated than necessary: the shape of a proof by induction will
    match the recursive structure of the program being verified, so
    make the recursions as simple as possible. *)

Theorem nat_bin_nat (n : nat) : bin_to_nat (nat_to_bin n) = n.
Proof.
  induction n ; cbn.
  - reflexivity.
  - rewrite bin_to_nat_pres_incr, IHn.
    reflexivity.
Qed.

(** Beware, this second part is more tricky! *)

(** The opposite direction -- starting with a [bin], converting to [nat],
    then converting back to [bin] -- turns out to be problematic. That
    is, the following theorem does not hold. *)

Theorem bin_nat_bin (b : bin) : nat_to_bin (bin_to_nat b) = b.
Abort.

(** Show it is indeed false. Undertanding where the issue lies will be
  important to prove a correct theorem. *)

Theorem bin_nat_bin_fails : exists b, nat_to_bin (bin_to_nat b) <> b.
Proof.
  exists (B0 Z).
  cbn.
  easy.
Qed.

(** Let's explore why that theorem fails, and how to prove a modified
    version of it. We'll start with some lemmas that might seem
    unrelated, but will turn out to be relevant. *)
    
(** First, a lemma about doubling. *)

Lemma double_incr (n : nat) : 2 * (S n) = S (S (2 * n)).
Proof.
  cbn.
  repeat rewrite Nat.add_0_r, Nat.add_succ_r.
  reflexivity.
Qed.

(** Now define a similar doubling function for [bin]. *)

Definition double_bin (b:bin) : bin :=
  match b with
  | Z => Z
  | b => B0 b
  end.

(** Check that your function correctly doubles zero. *)

Example double_bin_zero : double_bin Z = Z.
Proof.
  reflexivity.
Qed.

(** Prove this lemma, which corresponds to [double_incr]. *)

Lemma double_incr_bin (b : bin) :
    double_bin (incr b) = incr (incr (double_bin b)).
Proof.
  destruct b ; reflexivity.
Qed.

(** Let's return to our desired theorem: *)

Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = b.
Abort.

(** We can introduce a _normalization_ function
    that selects the simplest [bin] out of all the equivalent
    [bin]. Then we can prove that the conversion from [bin] to [nat] and
    back again produces that normalized, simplest [bin]. *)

(** Define [normalize]. You will need to keep its definition as simple
    as possible for later proofs to go smoothly. Do not use
    [bin_to_nat] or [nat_to_bin], but do use [double_bin].

    Hint: Structure the recursion such that it _always_ reaches the
    end of the [bin] and process each bit only once. Do not try to
    "look ahead" at future bits. *)

Fixpoint normalize (b:bin) : bin :=
  match b with
  | Z => Z
  | B1 b => incr (double_bin (normalize b))
  | B0 b => double_bin (normalize b)
end.

(** Do not hesitate to play around with your definition of [normalize]
  to check that your definition works the way you intend before you proceed,
  for instance using [Compute]. *)

(** Finally, prove the main theorem. The inductive cases could be a
    bit tricky.

    Hint: Start by trying to prove the main statement, see where you
    get stuck, and see if you can find a lemma -- perhaps requiring
    its own inductive proof -- that will allow the main proof to make
    progress. We have one lemma for the [B0] case (which also makes
    use of [double_incr_bin]) and another for the [B1] case. *)

Lemma double_to_bin (n : nat) : nat_to_bin (2*n) = double_bin (nat_to_bin n).
Proof.
  induction n ; cbn.
  1: reflexivity.
  rewrite Nat.add_0_r, Nat.add_succ_r ; cbn.
  replace (n + n) with (2*n).
  2:{ cbn ; now rewrite Nat.add_0_r. }
  rewrite IHn.
  rewrite double_incr_bin.
  reflexivity.
Qed.

Theorem bin_nat_bin (b : bin) : nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  induction b.
  - reflexivity.
  - cbn -[mul].
    now rewrite double_to_bin, IHb.
  - cbn -[mul].
    f_equal.
    now rewrite double_to_bin, IHb.
Qed.