(*******************************************************************************)
(* Coq Unit Testing project                                                    *)
(* Copyright 2015-2017 Catherine Dubois, Richard Genestier and Alain Giorgetti *)
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** General definitions for Coq unit testing *)

Require Import List Arith Omega.

(** * Coq lists and functions on natural numbers *)

(** Let [l] be a list of [n] naturals. ([list2fun l]) is the function [f] such that 
   [l = [f(0);f(1);...;f(n-1)]] and [f(i) = i] for [i >= n]. *)

Definition list2fun (l : list nat) : nat -> nat := fun (n : nat) => nth n l n.

(** [(fun2list n f) = [f(0);f(1);...;f(n-1)]]. *)

Fixpoint fun2list n f : list nat := match n with
  O => nil
| S m => (fun2list m f) ++ ((f m) :: nil) 
end.

(* Where are these lemmas in standard Coq? *)

Lemma eqb_nat_prop : forall a b:nat, Nat.eqb a b = true -> a = b.
Proof.
induction a; intros; simpl; auto.
- induction b; intros; simpl; auto. discriminate H.
- induction b; intros; simpl; auto. discriminate H.
Qed.

Lemma eqb_nat_true_intro : forall a b:nat, a = b -> Nat.eqb a b = true.
Proof.
induction a; intros; simpl; auto; subst; auto.
Qed.

Lemma eqb_nat_true_iff : forall a b:nat, Nat.eqb a b = true <-> a = b.
Proof. split. apply eqb_nat_prop. apply eqb_nat_true_intro. Qed.

(** * Decidable equality on the [n] first values of natural functions *)

(** ** Equality of functions up to [n] *)

Definition eq_natfun (n : nat) (f g : nat -> nat) :=
 forall i, i < n -> f i = g i.

(** ** Corresponding Boolean function *)

Fixpoint eq_natfunb (n : nat) (f g : nat -> nat) : bool :=
 match n with 
   0 => true
 | S m => andb ((f m) =? (g m)) (@eq_natfunb m f g)
 end.

Lemma eq_natfun_dec (n : nat) (f g : nat -> nat) :
 eq_natfun n f g <-> eq_natfunb n f g = true.
Proof.
split; intro H.
- {
 induction n; simpl; intros; auto.
 apply andb_true_intro. split. 
 - apply eqb_nat_true_iff. apply H. omega.
 - apply IHn. unfold eq_natfun. intros i I.
  apply H. omega.
}
- {
 intros i I.
 induction n; simpl; intros; auto.
 - omega.
 - {
  simpl in H.
  apply andb_prop in H. destruct H as [N E].
  assert (i < n \/ i = n) as C. omega.
  destruct C as [L|J].
  - {
   apply IHn.
   - apply E.
   - apply L.
  }
  - subst. apply eqb_nat_true_iff. apply N.
 }
}
Qed.

(** * Decidable equality on lists of natural numbers *)

Fixpoint list_eqb (x y : list nat) : bool :=
    match x, y with
      | nil, nil => true
      | cons hd tl, cons hd' tl' =>
        if Nat.eqb hd hd' then
          if list_eqb tl tl' then true else false
          else false
      | _, _ => false
    end.
