Chapter "Introduction" of Software Foundations in F*

module Basics

(* Days of the Week *)

type day =
  | Monday: day
  | Tuesday: day
  | Wednesday: day
  | Thursday: day
  | Friday: day
  | Saturday: day
  | Sunday: day

let next_weekday (d: day): day =
  match d with
  | Monday -> Tuesday
  | Tuesday -> Wednesday
  | Wednesday -> Thursday
  | Thursday -> Friday
  | Friday -> Monday
  | Saturday -> Monday
  | Sunday -> Monday

val test_next_weekday: unit ->
  Lemma (next_weekday (next_weekday Saturday) = Tuesday)
let test_next_weekday () = ()


(* Booleans *)

let negb (b: bool): bool =
  match b with
  | true -> false
  | false -> true

let andb (b1: bool) (b2: bool): bool =
  match b1 with
  | true -> b2
  | false -> false

let orb (b1: bool) (b2: bool): bool =
  match b1 with
  | true -> true
  | false -> b2

val test_orb1: unit -> Lemma (orb true false = true)
let test_orb1 () = ()
val test_orb2: unit -> Lemma (orb false false = false)
let test_orb2 () = ()
val test_orb3: unit -> Lemma (orb false true = true)
let test_orb3 () = ()
val test_orb4: unit -> Lemma (orb true true = true)
let test_orb4 () = ()


(* Exercise: 1 star (nandb) *)
let nandb (b1: bool) (b2: bool): bool =
  match b1, b2 with
  | true, true -> false
  | _, _ -> true

val test_nandb1: unit -> Lemma (nandb true false = true)
let test_nandb1 () = ()
val test_nandb2: unit -> Lemma (nandb false false = true)
let test_nandb2 () = ()
val test_nandb3: unit -> Lemma (nandb false true = true)
let test_nandb3 () = ()
val test_nandb4: unit -> Lemma (nandb true true = false)
let test_nandb4 () = ()


(* Exercise: 1 star (andb3) *)
let andb3 (b1: bool) (b2: bool) (b3: bool): bool =
  andb (andb b1 b2) b3

val test_andb31: unit -> Lemma (andb3 true true true = true)
let test_andb31 () = ()
val test_andb32: unit -> Lemma (andb3 false true true = false)
let test_andb32 () = ()
val test_andb33: unit -> Lemma (andb3 true false true = false)
let test_andb33 () = ()
val test_andb34: unit -> Lemma (andb3 true true false = false)
let test_andb34 () = ()


(* Numbers *)

type nat =
  | O: nat
  | S: n:nat -> nat

let pred (n: nat): nat =
  match n with
  | O -> O
  | S n' -> n'

let minustwo (n: nat): nat =
  match n with
  | O -> O
  | S O -> O
  | S (S n') -> n'

val evenb: n: nat -> Tot bool
let rec evenb n =
  match n with
  | O -> true
  | S O -> false
  | S (S n') -> evenb n'

val oddb: n: nat -> Tot bool
let oddb n = negb (evenb n)

val test_oddb1: unit -> Lemma (oddb (S O) = true)
let test_oddb1 () = ()
val test_oddb2: unit -> Lemma (oddb (S (S (S (S O)))) = false)
let test_oddb2 () = ()

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

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

val minus: n: nat -> m: nat -> Tot nat
let rec minus n m =
  match n, m with
  | O, _ -> O
  | S _, O -> n
  | S n', S m' -> minus n' m'

val exp: base: nat -> power: nat -> Tot nat
let rec exp base power =
  match power with
  | O -> S O
  | S p -> mult base (exp base p)


(* Auxiliaries for converting between our nats and F*'s nats. *)

val to_nat: i: int{i >= 0} -> Tot nat
let rec to_nat i =
  if i = 0 then O else S (to_nat (i-1))

val of_nat: n: nat -> Tot (i: int{i >= 0})
let rec of_nat n =
  match n with
  | O -> 0
  | S n' -> 1 + of_nat n'

val to_nat_of_nat: i: int{i >= 0} -> Lemma (of_nat (to_nat i) = i)
let rec to_nat_of_nat i =
  if i = 0 then () else to_nat_of_nat (i-1)

val of_nat_to_nat: n: nat -> Lemma (to_nat (of_nat n) = n)
let rec of_nat_to_nat n = by_induction_on n of_nat_to_nat


(* Exercise: 1 star (factorial) *)

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

val test_factorial1: unit -> Lemma (of_nat (factorial (to_nat 3)) = 6)
let test_factorial1 () = ()
val test_factorial1': unit -> Lemma (factorial (to_nat 3) = to_nat 6)
let test_factorial1' () = ()

val test_factorial2: unit ->
  Lemma (factorial (to_nat 5) = mult (to_nat 10) (to_nat 12))
let test_factorial2 () = (* FIXME! *) admit ()


val beq_nat: n: nat -> m: nat -> Tot bool
let rec beq_nat n m =
  match n with
  | O -> (match m with
          | O -> true
          | S m' -> false)
  | S n' -> (match m with
             | O -> false
             | S m' -> beq_nat n' m')

val ble_nat: n: nat -> m: nat -> Tot bool
let rec ble_nat n m =
  match n with
  | O -> true
  | S n' ->
    match m with
    | O -> false
    | S m' -> ble_nat n' m'

val test_ble_nat1: unit -> Lemma (ble_nat (to_nat 2) (to_nat 2) = true)
let test_ble_nat1 () = ()
val test_ble_nat2: unit -> Lemma (ble_nat (to_nat 2) (to_nat 4) = true)
let test_ble_nat2 () = ()
val test_ble_nat3: unit -> Lemma (ble_nat (to_nat 4) (to_nat 2) = false)
let test_ble_nat3 () = ()


(* Exercise: 2 stars (blt_nat) *)

val blt_nat: n: nat -> m: nat -> Tot bool
let blt_nat n m = ble_nat (S n) m

val test_blt_nat1: unit -> Lemma (blt_nat (to_nat 2) (to_nat 2) = false)
let test_blt_nat1 () = ()
val test_blt_nat2: unit -> Lemma (blt_nat (to_nat 2) (to_nat 4) = true)
let test_blt_nat2 () = ()
val test_blt_nat3: unit -> Lemma (blt_nat (to_nat 4) (to_nat 2) = false)
let test_blt_nat3 () = ()


(* Proof by Simplification *)

val plus_O_n: n: nat -> Lemma (plus O n = n)
let plus_O_n n = ()

val plus_1_l: n: nat -> Lemma (plus (S O) n = S n)
let plus_1_l n = ()

val mult_0_l: n: nat -> Lemma (mult O n = O)
let mult_0_l n = ()


(* Proof by Rewriting *)

val plus_id_example: n: nat -> m: nat -> Lemma (n = m ==> plus n n = plus m m)
let plus_id_example n m = ()


(* Exercise: 1 star (plus_id_exercise) *)

val plus_id_exercise:
  n: nat -> m: nat -> o: nat ->
  Lemma (n = m /\ m = o ==> plus n m = plus m o)
let plus_id_exercise n m o = ()


val mult_0_plus: n: nat -> m: nat -> Lemma (mult (plus O n) m = mult n m)
let mult_0_plus n m = plus_O_n n  (* not really necessary *)


(* Exercise: 2 stars (mult_S_1) *)

val mult_S_1:
  n: nat -> m: nat ->
  Lemma (m = S n ==> mult m (plus (S O) n) = mult m m)
let mult_S_1 n m = ()  (* could call plus_1_l n, but it's not needed *)


(* Proof by Case Analysis *)

val plus_1_neq_0: n: nat -> Lemma (beq_nat (plus n (S O)) O = false)
let plus_1_neq_0 n = ()

val negb_involutive: b: bool -> Lemma (negb (negb b) = b)
let negb_involutive b = ()


(* Exercise: 1 star (zero_nbeq_plus_1) *)

val zero_nbeq_plus_1: n: nat -> Lemma (beq_nat O (plus n (S O)) = false)
let zero_nbeq_plus_1 n = ()


(* More Exercises *)

(* Exercise: 2 stars (boolean_functions) *)

val identity_fn_applied_twice:
  f: (bool -> Tot bool) ->
  Lemma ((forall (x: bool). f x = x) ==> (forall (b: bool). f (f b) = b))
let identity_fn_applied_twice f = ()

val negation_fn_applied_twice:
  f: (bool -> Tot bool) ->
  Lemma ((forall (x: bool). f x = negb x) ==> (forall (b: bool). f (f b) = b))
let negation_fn_applied_twice f = ()


(* Exercise: 2 stars (andb_eq_orb) *)

val andb_eq_orb: b: bool -> c: bool -> Lemma (andb b c = orb b c ==> b = c)
let andb_eq_orb b c = ()


(* Exercise: 3 stars (binary) *)

type bin =
  | BZ
  | B0: b: bin -> bin
  | B1: b: bin -> bin

val incr: b: bin -> Tot bin
let rec incr b =
  match b with
  | BZ -> B1 BZ
  | B0 b' -> B1 b'
  | B1 b' -> B0 (incr b')

val bin_to_nat: b: bin -> Tot nat
let rec bin_to_nat b =
  match b with
  | BZ -> O
  | B0 b' -> mult (S (S O)) (bin_to_nat b')
  | B1 b' -> plus (S O) (mult (S (S O)) (bin_to_nat b'))

val test_bin_incr1: unit -> Lemma (bin_to_nat (incr BZ) = S O)
let test_bin_incr1 () = ()

val test_bin_incr2:
  b: bin ->
  Lemma (bin_to_nat (B1 b) = plus (S O) (bin_to_nat (B0 b)))
let test_bin_incr2 b = ()

val test_bin_incr3:
  b: bin ->
  Lemma (bin_to_nat (B0 b) = mult (S (S O)) (bin_to_nat b))
let test_bin_incr3 b = ()

val test_bin_incr4:
  b: bin ->
  Lemma (bin_to_nat (incr (B1 b)) = mult (S (S O)) (plus (S O) (bin_to_nat b)))
let rec test_bin_incr4 b =
  match b with
  | BZ -> ()
  | B0 b' -> test_bin_incr4 b'
  | B1 b' -> (* FIXME *) admit ()

val test_bin_incr5:
  b: bin ->
  Lemma (bin_to_nat (incr b) = plus (S O) (bin_to_nat b))
let rec test_bin_incr5 b =
  match b with
  | BZ -> ()
  | B0 b' -> test_bin_incr5 b'
  | B1 b' -> (* FIXME *) admit ()