Require Import ZArith List Bool predefined_functions.

Import ListNotations.

Open Scope Z_scope.

(* The Zseq function takes a number n as argument and returns the sequence of
  n elements 0 ... (n - 1) *)
Compute Zseq 10.

(* The Zfactorial function takes a number n as argument and returns the
  product of the n first positive integers (if n is positive) *)

(* We can use + - * / ^  and  mod  to compute binary operation with numbers. *)
Compute 2 ^ 64 - Zfactorial 21.

Compute 64 mod 10.

(* We can also build objects that are pairs of two objects of different type. *)

Compute (3, true).

(* We can define a new function by using the keyword Definition *)

Definition polynom1 (x : Z) := x ^ 2 + 3 * x + 1.

(* We can check that an expression is well formed by using the command.
  Check.    Moreover, this command says what is the type of the result. *)
Check polynom1 (polynom1 (polynom1 (Zfactorial 100))).

(* We can also build functions without naming them. *)

Check (fun x => x + 1, fun x y => (x + 1, x * y)).

Check ((Z -> Z) -> Z).

Definition function_with_function_argument (f : Z -> Z) := f 0.
Check  function_with_function_argument.

Definition my_add (x y : Z) : Z := x + y.
Check my_add.

(* When a variable is used in an anonymous function, it remains undefined
  outside that function. *)

Fail Check x.

(* ## Working with lists *)

(* The function cons and its specific notation. *)

Check fun (x : Z) (l : list Z) => cons x l.

Check fun (x : Z) (l : list Z) => x :: l.

Check 3 :: [0; 1].

(* We can also have lists whose elements are list. *)

Check [[1; 2; 3]; [4; 5; 6]].

(* Boolean values : true false, and number testing. *)

Check (3 <=? 2).

Compute (3 <=? 2).

(* Optional values : Some and None. *)

Check Some 3.

Check Some [3].

(* ## Observing, testing, making decisions in algorithms. *)

Compute 
  match (3 :: 4 :: nil) with
  | a :: tl => a
  | nil => 0
  end.

Compute
  match (3 :: 4 :: nil) with
  | a :: tl => tl
  | nil => nil
  end.


(* Here is how we define a function that returns the sum of the first
  two arguments of a list if they exist, the first argument if there is
  only one, and 0 otherwise. *)

Definition sum2_from_list (l : list Z) :=
  match l with
  | (a :: b :: _) => a + b
  | a :: nil => a
  | nil => 0
  end.

Module alternative_syntax.

  Definition sum2_from_list (l : list Z) :=
  match l with
  | a :: tl => match tl with b :: _ => a + b | nil => a end
  | nil => 0
  end.

End alternative_syntax.

(* for boolean values we can use both match with and if-then-else *)

Definition my_version_of_max (x y : Z) :=
  if x <=? y then y else x.

(* Recursion: computing the sum of all elements of a list. *)

Fixpoint sum_list_Z (l : list Z) :=
 match l with nil => 0 | a::tl => a + sum_list_Z tl end.

 Eval cbn [sum_list_Z] in sum_list_Z [0; 1; 2; 3].

Fixpoint teo (l : list Z) :=
  match l with
    nil => nil
  | a::nil => a::nil
  | a::b::tl => a::teo tl
  end.

Fixpoint list_digit_to_Z (l : list Z) :=
  match l with nil => 0 | a :: tl => a + 10 * list_digit_to_Z tl end.

(* Example : division of numbers represented as sequences of digits. *)

Fixpoint add1 (l : list Z) :=
  match l with
    a :: tl => if a =? 9 then 0 :: add1 tl else (a + 1) :: tl 
  | nil => [1] end.

Fixpoint add_with_carry (l1 l2 : list Z) (carry : bool) :=
  match l1, l2 with
  | nil, nil => if carry then [1] else []
  | nil, l2 => if carry then add1 l2 else l2
  | a :: l1', nil => if carry then add1 (a :: l1') else a :: l1'
  | a :: l1', b :: l2' =>
    let first_digit_sum := (if carry then a + 1 else a) + b in
    if first_digit_sum <? 10 then
      first_digit_sum :: add_with_carry l1' l2' false
    else
      (first_digit_sum - 10) :: add_with_carry l1' l2' true
  end.

Definition add l1 l2 := add_with_carry l1 l2 false.

Fixpoint sub1 (l : list Z) :=
  match l with
  | nil => nil
  | a :: tl => if a =? 0 then 9 :: sub1 tl else (a - 1) :: tl
  end.

Fixpoint subtract_with_carry (l1 l2 : list Z) (carry : bool) :=
  match l1, l2 with
  | nil, nil => nil
  | nil, _l2 => nil
  | a :: l1', nil => if carry then sub1 (a :: l1') else a :: l1'
  | a :: l1', b :: l2' =>
    let first_digit_diff := a - (if carry then b + 1 else b) in
    if first_digit_diff <? 0 then
      (first_digit_diff + 10) :: subtract_with_carry l1' l2' true
    else
      first_digit_diff :: subtract_with_carry l1' l2' false
  end.

Definition subtract (l1 l2 : list Z) :=
  subtract_with_carry l1 l2 false.

Fixpoint one_digit_mul (x : Z) (l : list Z) :=
  match l with
  | a :: tl =>
    let first_prod := x * a in
    let big_prod := one_digit_mul x tl in
    (first_prod mod 10) :: 
      add ((first_prod / 10) :: nil)
        big_prod
  | _ => nil
  end.

Fixpoint mul_aux (l1 l2 : list Z) :=
  match l1 with
  | nil => nil
  | a :: tl =>  add (one_digit_mul a l2) (0 :: mul_aux tl l2)
  end.

Fixpoint is_zero (l : list Z) :=
  match l with
  | a :: tl => (a =? 0) && is_zero tl
  | nil => true
  end.

Definition multiply (l1 l2 : list Z) :=
  if is_zero l2 then [] else mul_aux l1 l2.

Fixpoint eq_number (l1 l2 : list Z) :=
  match l1, l2 with
  | a::t1, b::t2 => (a =? b) && eq_number t1 t2
  | _, _ => is_zero l1 && is_zero l2
  end.

Fixpoint less_than (l1 l2 : list Z) :=
  match l1, l2 with
  | a :: tl1, b :: tl2 => 
    if eq_number tl1 tl2 then a <=? b else less_than tl1 tl2
  | _, b :: tl2 => true
  | _, _ => is_zero l1
  end.

Fixpoint small_div (ks : list Z) l q :=
  match ks with
  | k :: tl =>
    if less_than (one_digit_mul k q) l then k else small_div tl l q
  | _ => 0
  end.

Definition small_divide l q := 
  small_div (9 :: 8 :: 7 :: 6 :: 5 :: 4 :: 3 :: 2 :: 1 :: nil) l q.  

Fixpoint divide (input d : list Z) : list Z * list Z :=
  match input with
    a :: l => let (q, r) := divide l d in
    let n := small_divide (a::r) d in
    (n::q, subtract (a::r) (multiply (n::nil) d))
  | nil => (nil, nil)
  end.