<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />

(*
Inductive bool := true | false.

Inductive nat := O : nat | S : nat -> nat.

Inductive list A := nil : list A | cons : A -> list A -> list A.
*)

Definition negb b :=
 match b with
  | true => false
  | false => true
 end.

Eval vm_compute in (negb true).
Eval vm_compute in (negb false).
Eval vm_compute in (negb (negb true)).

(*
Definition wrong_negb b :=
 match b with
  | true => false
 end.

Error: Non exhaustive pattern-matching: no clause found for pattern false
*)

(*
Definition wrong_negb b :=
 match b with
  | true => false
  | true => true
  | false => true
 end.

Error: This clause is redundant.
*)

(* Beware of the misspelling : ttrue below is read as a pattern variable!

Definition wrong_negb b :=
 match b with
  | ttrue => false
  | false => true
 end.
*)

Definition pred x :=
 match x with
  | S x => x
  | O => O
 end.

Definition iszero x :=
 match x with
  | O => true
  | _ => false   (* or: | S _ => false *)
 end.

Definition istwo x :=
 match x with
  | S (S O) => true   (* or: | 2 => true *)
  | _ => false
 end.

Unset Printing Matching. (* prevent Coq attempts to pretty-print things *)
Print istwo.

Definition andb b1 b2 :=
 match b1, b2 with
  | true, true => true
  | _, _ => false
 end.

Print andb.

(* Exercise: write andb with only one simple match *)

Definition simplier_andb (b1 b2:bool) := if b1 then b2 else false.


(** Recursion *)

Fixpoint div2 n :=
 match n with
  | S (S n') => S (div2 n')   (* (n'+2)/2 = n'/2+1 *)
  | _ => O                    (* n is 0 or 1 *)
 end.

(*Fixpoint div2_ko n := if leb n 1 then 0 else S (div2_ko (n-2)).*)

Eval vm_compute in (div2 13).

Fixpoint plus n m :=
 match n with
  | O => m
  | S n' => S (plus n' m)      (* (n+1)+m = (n+m)+1 *)
 end.

Eval vm_compute in (plus 5 6).

(* Exercise:
   - define an div2sup function that return ceil(n/2) instead of
     floor(n/2)
   - check experimentally that for all n below 1000,
      plus (div2 n) (div2sup n) is n
   - how could we write a div3 ? Is it possible to write a div this way ?
*)

Fixpoint div2sup n :=
 match n with
  | S (S n') => S (div2sup n')
  | n => n
 end.

(* or *)

Definition div2sup' n := div2 (S n).

Eval vm_compute in (div2sup 3).


Fixpoint check_forall_below (f:nat->bool)(n:nat) :=
 match n with
  | 0 => true
  | S n' => andb (f n') (check_forall_below f n')
 end.

Require Import EqNat

Eval vm_compute in
 check_forall_below (fun n => beq_nat (div2sup' n) (div2sup n)) 1000.

Eval vm_compute in
 check_forall_below (fun n => beq_nat n (div2 n + div2sup n)) 1000.

(** Later, you'll be able to _prove_ these kind of statements for
    all numbers. *)

Require Import Omega.

Lemma div2sup_equiv : forall n, div2sup n = div2sup' n.
Proof.
 induction n using lt_wf_ind.
 destruct n.
 reflexivity.
 unfold div2sup'. simpl.
 destruct n.
 reflexivity.
 f_equal.
 apply H; auto.
Qed.

Lemma div2_plus_div2sup : forall n, div2 n + div2sup n = n.
Proof.
 induction n using lt_wf_ind.
 destruct n.
 reflexivity.
 destruct n.
 reflexivity.
 simpl.
 rewrite <- plus_n_Sm.
 do 2 f_equal.
 apply H; auto.
Qed.


(** More functions about numbers: *)

Fixpoint mult n m :=
 match n with
  | O => O
  | S n' => plus m (mult n' m)
 end.

Fixpoint minus n m :=
 match n with
  | O => O
  | S n' =>
    match m with
     | O => n
     | S m' => minus n' m'
    end
 end.

Fixpoint minus_bis n m :=
 match n, m with
  | S n', S m' => minus_bis n' m'
  | _, _ => n
 end.

Fixpoint nat_beq n m :=
 match n, m with
  | O, O => true
  | S n', S m' => nat_beq n' m'
  | _, _ => false
 end.

Fixpoint leb n m :=
 match n, m with
  | O, _ => true
  | _, O => false
  | S n', S m' => leb n' m'
 end.


(** Recursion over lists *)

Open Scope list_scope. (* for having :: *)

Set Implicit Arguments.

Fixpoint length A (l : list A) :=
 match l with
  | nil => O
  | _ :: l' => S (length l')
 end.

(** NB: without Implicit Arguments, we should write (lenght A l')
    even if type A can be inferred automatically. *)

Fixpoint app A (l1 l2 : list A) :=
 match l1 with
  | nil => l2
  | a :: l1' => a :: (app l1' l2)
 end.

(** With fold_right, computation starts at the end of the list:
    fold_right f init (a::b::c::nil) = f a (f b (f c init)) *)

Fixpoint fold_right A B (f:B->A->A) (init:A) (l:list B) : A :=
 match l with
  | nil => init
  | x :: l' => f x (fold_right f init l')
 end.

Eval vm_compute in
 fold_right plus 0 (1::2::3::nil). (* = (1+(2+(3+0))) *)

Eval vm_compute in
 fold_right (fun x l => x::l) nil (1::2::3::nil). (* = 1::2::3::nil *)

(** With fold_left, computation starts at the top of the list:
    fold_left f (a::b::c::nil) init = f (f (f init a) b) c *)

Fixpoint fold_left A B (f:A->B->A) (l:list B) (init:A) : A :=
 match l with
  | nil => init
  | x :: l' => fold_left f l' (f init x)
 end.

Eval vm_compute in
 fold_left plus (1::2::3::nil) 0. (* = (((0+1)+2)+3) *)

Eval vm_compute in
 fold_left (fun l x => x::l) (1::2::3::nil) nil. (* = 3::2::1::nil *)


(* Exercise : define map filter seq rev combine *)

(* Exercise : give an alternate definition of vec_prod (of session 1)
   without using fold_right or combine. *)

Fixpoint vec_prod l1 l2 :=
 match l1, l2 with
  | x1::l1', x2::l2' => x1 * x2 + vec_prod l1' l2'
  | _, _ => 0
 end.

(* Conversely, write map filter rev by using fold_right or fold_left *)


(** Merge sort *)

Fixpoint split A (l : list A) : list A * list A :=
 match l with
  | nil => (nil, nil)
  | a::nil => (a::nil, nil)
  | a::b::l' => let (l1, l2) := split l' in (a::l1, b::l2)
 end.

Eval vm_compute in split (1::2::3::4::5::nil).

(** Exercise : what is length (fst (dispatch l)) ? Same for snd ? *)

Definition merge A (less:A->A->bool) : list A -> list A -> list A :=
 fix merge l1 :=
   match l1 with
    | nil =>
       fun l2 => l2
    | x1::l1' =>
       fix merge_l1 l2 :=
         match l2 with
          | nil => l1
          | x2::l2' =>
            if less x1 x2 then x1 :: merge l1' l2
                          else x2 :: merge_l1 l2'
         end
   end.

Definition mergeloop A (less:A->A->bool) :=
 fix loop (l:list A) (n:nat) :=
  match n with
   | O => nil
   | S n => match l with
             | nil => l
             | _::nil => l
             | _ => let (l1,l2) := split l in
                    merge less (loop l1 n) (loop l2 n)
            end
  end.

(** Invariant above: n >= length l *)

Definition mergesort A less (l:list A) :=
  mergeloop less l (length l).

Eval vm_compute in mergesort leb (4::2::6::3::9::1::nil).

(** Exercise: what happen if we remove the "| _::nil => l" in mergeloop ? *)


(** Exercise: define a nat_iter ? a nat_rect ? give the intuition
   that all recursion/matching over nat can be done via nat_rect... *)