Chapter "Induction" of Software Foundations in F*

(*--build-config
    other-files: basics.fst
  --*)

module Induction

open Basics


(* Naming Cases *)

val andb_true_elim1:
  b: bool -> c: bool ->
  Lemma (andb b c = true ==> b = true)
let andb_true_elim1 b c = ()


(* Exercise: 2 stars (andb_true_elim2) *)

val andb_true_elim2:
  b: bool -> c: bool ->
  Lemma (andb b c = true ==> b = true)
let andb_true_elim2 b c = ()


(* Proof by Induction *)

val plus_0_r: n: nat -> Lemma (plus n O = n)
let rec plus_0_r n = by_induction_on n plus_0_r

val minus_diag: n: nat -> Lemma (minus n n = O)
let rec minus_diag n = by_induction_on n minus_diag


(* Exercise: 2 stars (basic_induction) *)

val mult_0_r: n: nat -> Lemma (mult n O = O)
let rec mult_0_r n = by_induction_on n mult_0_r

val plus_n_Sm: n: nat -> m: nat -> Lemma (S (plus n m) = plus n (S m))
let rec plus_n_Sm n m =
  match n with
  | O -> ()
  | S n' -> plus_n_Sm n' m

val plus_comm: n: nat -> m: nat -> Lemma (plus n m = plus m n)
let rec plus_comm n m =
  match n with
  | O -> plus_0_r m
  | S n' ->
      (* plus (S n') m = S (plus n' m) = S (plus m n') by induction *)
      plus_comm n' m;
      (* S (plus m n') = plus m (S n') *)
      plus_n_Sm m n'

val plus_assoc:
  n: nat -> m: nat -> p: nat ->
  Lemma (plus n (plus m p) = plus (plus n m) p)
let rec plus_assoc n m p =
  match n with
  | O -> ()
  | S n' -> plus_assoc n' m p


(* Exercise: 2 stars (double_plus) *)

val double: n: nat -> Tot nat
let rec double n =
  match n with
  | O -> O
  | S n' -> S (S (double n'))

val double_plus: n: nat -> Lemma (double n = plus n n)
let rec double_plus n =
  match n with
  | O -> ()
  | S n' -> plus_n_Sm n' (S n'); plus_comm n' (S (S n')); double_plus n'


(* Proofs Within Proofs *)

val mult_0_plus':
  n: nat -> m: nat ->
  Lemma (mult (plus O n) m = mult n m)
let mult_0_plus' n m =
  let h: unit -> Lemma (plus O n = n) = (fun _ -> ()) in
  h()

val plus_rearrange:
  n: nat -> m: nat -> p: nat -> q: nat ->
  Lemma (plus (plus n m) (plus p q) = plus (plus m n) (plus p q))
let plus_rearrange n m p q =
  let h: unit -> Lemma (plus n m = plus m n) =
    (fun _ -> plus_comm n m; ())
  in
  h()


(* Exercise: 4 stars (mult_comm) *)

val plus_swap:
  n: nat -> m: nat -> p: nat ->
  Lemma (plus n (plus m p) = plus m (plus n p))
let plus_swap n m p =
  plus_assoc n m p; plus_comm n m; plus_assoc m n p

(* Proof of mult_comm using these lemmas inspired by Lindsey Kuper's proof
 * at https://github.com/lkuper/software-foundations/blob/master/Induction.v
 *)
val plus_elim: n: nat -> m: nat -> Lemma (plus n (mult n m) = mult n (S m))
let rec plus_elim n m =
  match n with
  | O -> ()
  | S n' ->
      (* plus (S n') (mult (S n') m) = S (plus n' (plus m (mult n' m))) *)
      plus_swap n' m (mult n' m);  (* = S (plus m (plus n' (mult n' m))) *)
      plus_elim n' m;              (* = S (plus m (mult n' (S m))) *)
      ()             (* = plus (S m) (mult n' (S m)) = mult (S n') (S m) *)

val mult_m_Sn: m: nat -> n: nat -> Lemma (mult m (S n) = plus m (mult n m))
let rec mult_m_Sn m n =
  match m with
  | O -> mult_0_r n
  | S m' ->
      (* mult (S m') (S n) = plus (S n) (mult m' (S n)) *)
      mult_m_Sn m' n;     (* = plus (S n) (plus (m' (mult n m))) *)
      plus_swap n m' (mult (S n) m');
                          (* = plus m' (plus (S n) (mult (S n) m')) *)
      plus_elim (S n) m'  (* = plus m' (mult (S n) (S m')) *)

val mult_comm: m: nat -> n: nat -> Lemma (mult m n = mult n m)
let rec mult_comm m n =
  match n with
  | O -> mult_0_r m
  | S n' ->
      mult_m_Sn m (S n');  (* mult m (S n') = plus m (mult n' m) *)
      mult_comm m n';      (* = plus m (mult m n') *)
      plus_elim m n'       (* = mult m (S n') *)