(* Precept 5:  Proofs about Fuctional Programs *)

(* This precept will help familiarize you with material on proving
 * things about programs.  As part of your homework this week, you must
 * read the online notes about proving things about programs. 
 *)

(* Refer to these notes to help you through this week's precept
 * materials: 
 * http://www.cs.princeton.edu/~cos326/notes/reasoning.php
 * http://www.cs.princeton.edu/~cos326/notes/reasoning-data.php
 *)

(*
 * 1.  Consider the function tail, below.
 * 
 * Is tail a total function? No (match is not exhaustive - [])
 * 
 * Is tail [] a valuable expression? No 
 * 
 * Is tail [3] a valuable expression? Yes
*)

let tail (xs: 'a list) : 'a list =
  match xs with hd :: tail -> tail


(*
 * 2. Consider the function safediv, below.
 * 
 * Is safediv a total function? Yes
 * 
 * Is safediv (1, 0) valuable? Yes
*)

let safediv (nums : int * int) : int option =
  let (x,y) = nums in
  if y == 0 then None
  else Some (x/y)

(*
 * 3. Consider the following type and function declarations
 * 
 * Is free_var total? Yes 
 * 
 * Is free_vars total? Yes
*)

type form = 
  Var of string
| And of form list

let rec free_var (f : form) =
  match f with
    Var s -> [s]
  | And fs -> free_vars fs

and free_vars (fs: form list) =
  match fs with
    [] -> []
  | f :: rest -> free_var f @ free_vars rest

(* 
 * 4. Consider the mutually recursive functions f and g: 
 * 
 * Is f total? No 
 * 
 * Is g total? No
 * 
 * (if x passed to f or y passed to g <= 0, infinite recursion)
*)

let rec f (x:int) =
  if x > 50 then 1 + f (x-1) else g x

and g (y: int) =
  if y > 0 then 1 else f (y-1)

(* 
 * 5. Consider f', a function used by g', and the definition of g'
 * 
 * What do we need to know about f' to know that g' is total?
 *       f' must be total
 * 
*)

let f' x = (* some definition *) ;;

let g' x = 
  if f' x then 1 else 0


(* 6. Given the definition of inc, give justifications for each of the
 * equations below using the equational rules given in the online
 * notes.  Whenever you need to use reflexivity, transitivity,
 * symmetry, congruence, etc., say so. 
 *)

(* inc 3 == 4                                        eval, math, transitivity
 * inc 4 == 5                                        eval, math, transitivity
 * inc (inc 3) == 5              1st line, congruence, 2nd line, transitivity
 * fun x -> x + 1 == inc          syntactic sugar, substitution, transitivity
 * for all values v, v + 1 == inc v                                      eval 
 * for all valuable expressions e, e + 1 == inc e                        eval
*)

let inc x = x + 1

(* 7. Consider the function multo, below: *)
let multo (x:int option) (y:int option) =
  match (x,y) with
    (Some m, Some n) -> Some ((m + m)*n)
  | (_, _) -> None
in
(* Prove the following equation holds, step by step, for all o : int option. 
 * Note: You can start top down, or you can start bottom up, or go from both 
 * ends to meet in the middle.
*)

multo o o == (match o with Some i -> Some (2*(i*i)) | None -> None)

(* Proof: by cases on the structure of o, each by simple equational reasoning.
case o = None:
   multo None None                                                 (LHS)
== match (None, None) with (... | (_, _) -> None)                 (eval)
== None                                                           (eval)
== match None with Some i -> Some (2*(i*i)) | None -> None   (inv. eval)

case o = Some j:
   multo (Some j) (Some j)                                         (LHS)
== match (Some j, Some j) with 
   (Some m, Some n) -> Some (m+m)*n | None -> None)               (eval)
== Some (j+j)*j                                                   (eval)
== Some (2*(j*j))                                                 (math)
== match Some j with 
   Some i -> Some (2*(i*i)) | None -> None)                  (inv. eval)

*)

(* 8. Consider the function compose, below: *)
let compose (f:'a -> 'b) (g:'b -> 'c) (x:'a) = g (f x) in

(* Prove the following equation holds, step by step, for all n : int *)
compose (fun x -> x * 2) (fun y -> y * 8) n  == compose (fun z -> z * 4) (fun w -> w * 4) n

(* Proof: by simple equational reasoning
   compose (fun x -> x * 2) (fun y -> y * 8) n                     (LHS)
== (fun y -> y*8) ((fun x -> x*2) n)			          (eval)
== (fun y -> y*8) (n*2) 				    	  (eval)
== (n*2)*8				      (eval, since n*2 valuable)
== (n*4)*4                                      	          (math)
== (fun w -> w*4) (n*4)                         	     (inv. eval)
== (fun w -> w*4) ((fun z -> z*4) n)            	     (inv. eval)
== compose (fun z -> z * 4) (fun w -> w * 4) n  	     (inv. eval)

*)

(* 9. Consider the functions double and half, below: *)
  

let rec double (xs: int list) : int list =
  match xs with
    [] -> []
  | hd :: rest -> hd::hd::double rest

let rec half (xs: int list) : int list =
  match xs with
    [] -> []
  | [x] -> []
  | x::y::rest -> y::half rest

(* Disprove this conjecture: for all l, double(half l) == l.  
 * Rhetorical question:  How does one disprove such a conjecture? 
*)

(* Proof by counterexample:
   When l == [3], 
   double(half [3]) == double [] == []
   but [] != [3]
*)


(* Prove that for all integer lists l. half (double l) == l.
 * Structure your proof as an inductive proof in two cases 
 * on the structure of the list l.
 *)

(* Proof, in two cases, by induction on the structure of the list l:

case l = []           		
To show:  half (double []) == []

   half (double [])                (LHS)
== half []                (eval 2 steps)
== []                     (eval 2 steps)

case l = hd::tail           	
To show:  half (double (hd::tail)) == hd::tail
IH:  half (double tail) == tail

   half (double (hd::tail))             (LHS)
== half (hd::hd::double tail)  (eval 2 steps)
== hd::(half(double tail))     (eval 2 steps)
== hd::tail                              (IH)

*)

(* 10. Recall the familiar map and function composition operators, below. 
 * Note that (%%) is the same as the function compose from problem 8, 
 * but defined using an infix operator instead, just for fun.
*)

let rec map (f: 'a -> 'b) (xs : 'a list) : 'b list =
  match xs with
    [] -> []
  | hd::tail -> f hd :: map f tail

let (%%) (g:'b -> 'c)  (f:'a -> 'b) (x:'a) : 'c = 
  g (f x)

(* A common program optimization is to take a series of several map
 * operations and compress them in to a single map operation.  Instead
 * of traversing a list multiple times (once for each application of
 * the map operation), one only traverses the list once.  More
 * specifically, the following property of map is true (for any total
 * functions f and g with the correct types): 
*)

map (g %% f) == (map g) %% (map f)

(* We are going to prove this fact with the aid of the following
 * lemma: 
 * For all types 'a, 'b and values f : 'a -> 'b, 
 * if f is total then map f is valuable and total.
 * 
 * Now the theorem.  We will provide each step in the proof of the
 * theorem.  It is up to you to provide the correct justification.
 * However, you can omit mentioning reflexivity, transitivity,
 * symmetry or congruence explicitly (just use these laws wherever
 * you see fit from now on without mentioning them).
 * 
 * 
 * For all types 'a, 'b, 'c 
 * and for all values f : 'a ->'b and g : 'b -> 'c and l : 'a list, 
 * if f and g are total then ((map g) %% (map f)) l == map (g %% f) l
 *)

(*
 * Facts we know, observations, and justifications:
 * 
 * 1. f is total                        Given
 * 2. g is total                        Given
 * 
 * 3. map f is valuable and total       
 * 4. map g is valuable and total
 * 5. g %% f is valuable
 * 6. g %% f is total
 * 7. map (g %% f) is valuable and total
 * 
 * 8. ((map g) %% (map f)) l == (fun x -> map g (map f x)) l
 * 9. == map g (map f l)
 * 
 * 10. thus, by transitivity of equality, we only have to prove that:
 * map g (map f l) == map (g %% f) l
 * 
 * Structure your proof as an inductive proof in two cases 
 * on the structure of the list l.
 * 
 *)

(* Proof, in two cases, by induction on the structure of the list l:

case l = []           		
To show:  map g (map f []) == map (g %% f) []

   map g (map f [])                     (LHS)
== map g ([])                           (eval 2 steps)
== []                                   (eval 2 steps)
== match [] with [] -> [] | ...         (inv eval)
== map (g %%f) []                       (inv eval)

case l = hd::tail           	
To show:  map g (map f hd::tl) == map (g %% f) hd::tl
IH:  map g (map f tl) == map (g %% f) tl

   map g (map f hd::tl)                 (LHS)
   map g (f hd :: map f tl)             (eval f 2 steps)
   g (f hd) :: map g (map f tl)         (eval g 2 steps)
   g (f hd) :: map (g %% f) tl          (IH)
   (g %% f) hd :: map (g %% f) tl       (inv. eval %%)
   map (g %% f) hd::tl                  (inv. eval map)

*)