(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************)
(*           The Calculus of Inductive Constructions            *)
(*                       COQ v5.10                              *)
(*                                                              *)
(* Laurent Arditi.  Laboratoire I3S. CNRS ura 1376.             *)
(* Universite de Nice - Sophia Antipolis                        *)
(* arditi@unice.fr, http://wwwi3s.unice.fr/~arditi/lolo.html    *)
(*                                                              *)
(* date: july 1995                                              *)
(* file: LemPrelim.v                                            *)
(* contents: VERIFICATION OF A SEQUENTIAL MULTIPLIER. Proofs of *)
(* some preliminary lemmas.                                     *)
(****************************************************************)

(* Des lemmes preliminaires *)

Require Export Definitions.

Lemma R1_lem :
 forall t : nat, (* R1(t)[0:n-1-t]=B[t:n-1] *)
 t <= size -> truncbv (R1 t) (size - t) = stripbv V1 t.
(* Goal: forall (t : nat) (_ : le t size), @eq BV (truncbv (R1 t) (Nat.sub size t)) (stripbv V1 t) *)
simple induction t. elim minus_n_O. rewrite <- (length_R1 0).
(* Goal: forall _ : le O (lengthbv (R1 O)), @eq BV (truncbv (R1 O) (lengthbv (R1 O))) (stripbv V1 O) *)
(* Goal: le O size *)
(* Goal: forall (n : nat) (_ : forall _ : le n size, @eq BV (truncbv (R1 n) (Nat.sub size n)) (stripbv V1 n)) (_ : le (S n) size), @eq BV (truncbv (R1 (S n)) (Nat.sub size (S n))) (stripbv V1 (S n)) *)
intro. rewrite (trunc_all bool). rewrite (strip_O bool). auto with arith.
(* Goal: le (S O) (S (Nat.sub m t)) *)
(* Goal: le t m *)
(* Goal: @eq (list bool) (trunc bool (strip bool (R1 t) O) (Nat.sub size t)) (strip bool V1 t) *)
auto with arith. intros. rewrite R1_eq2. rewrite highs_is_strip.
(* Goal: @eq BV (truncbv (appbv (stripbv (R1 n) (S O)) (Mux (lowbit (R1 n)) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv))) (Nat.sub size (S n))) (stripbv V1 (S n)) *)
rewrite (trunc_app bool). rewrite (trunc_strip bool).
(* Goal: le (Nat.sub size (S n)) (Nat.add (@length bool (stripbv (R1 n) (S O))) (@length bool (consbv (lowbit (R2 n)) nilbv))) *)
rewrite (length_strip bool). rewrite length_R1.
(* Goal: @eq BV (@app bool (strip bool (trunc bool (R1 n) (Nat.add (S O) (Nat.sub size (S n)))) (S O)) (trunc bool (Mux (lowbit (R1 n)) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv)) (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))))) (stripbv V1 (S n)) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
replace (size - S n - (size - 1)) with 0.
(* Goal: @eq BV (@app bool (strip bool (trunc bool (R1 n) (Nat.add (S O) (Nat.sub size (S n)))) (S O)) (trunc bool (Mux (lowbit (R1 n)) (consbv (lowbit (BV_full_adder_sum (R2 n) V2 false)) nilbv) (consbv (lowbit (R2 n)) nilbv)) O)) (stripbv V1 (S n)) *)
(* Goal: @eq nat O (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
rewrite (trunc_O bool).
(* Goal: @eq BV (@app bool (strip bool (trunc bool (R1 n) (Nat.add (S O) (Nat.sub size (S n)))) (S O)) (@nil bool)) (stripbv V1 (S n)) *)
(* Goal: @eq nat O (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
replace (1 + (size - S n)) with (size - n).
(* Goal: @eq BV (@app bool (strip bool (trunc bool (R1 n) (Nat.sub size n)) (S O)) (@nil bool)) (stripbv V1 (S n)) *)
(* Goal: @eq nat (Nat.sub size n) (Nat.add (S O) (Nat.sub size (S n))) *)
(* Goal: @eq nat O (Nat.sub (Nat.sub size (S n)) (Nat.sub size (S O))) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
rewrite (app_v_nil bool). unfold truncbv in H.
(* Goal: le (S O) (S (Nat.sub m t)) *)
(* Goal: le t m *)
(* Goal: @eq (list bool) (trunc bool (strip bool (R1 t) O) (Nat.sub size t)) (strip bool V1 t) *)
rewrite H. rewrite (strip_strip bool). rewrite plus_comm. simpl in |- *. auto with arith.
(* Goal: le n size *)
apply le_Sn_le; exact H0.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))) (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (BV_to_nat (consbv (lowbit v) nilbv)) (power2 n)) (PeanoNat.Nat.mul (Nat.mul (power2 (lengthbv (consbv (lowbit v) nilbv))) (BV_to_nat (highs v))) (power2 n))) *)
(* Goal: @eq nat (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v))) (BV_to_nat v) *)
simpl in |- *. rewrite minus_Sn_m. simpl in |- *. trivial with arith.
(* Goal: le n size *)
exact H0.
(* Goal: le (S O) (S (Nat.sub m t)) *)
(* Goal: le t m *)
(* Goal: @eq (list bool) (trunc bool (strip bool (R1 t) O) (Nat.sub size t)) (strip bool V1 t) *)
symmetry  in |- *. apply minus_le_O. apply le_minus_minus. auto with arith.
(* Goal: le n size *)
apply le_Sn_le; exact H0.
(* Goal: le (S O) (@length bool (R1 n)) *)
rewrite length_R1. apply le_SO_size. apply le_Sn_le; exact H0.
Qed.

(*
Lemma R1_lem2 : (t,i:nat) (* R1(t)[i]=B[t+i] *)
	(le t size) -> (lt i size)  ->
	(abit (R1 t) i) = (abit v1 (plus t i)).
*)


Lemma R1_lem3 :
 forall t : nat, (* R1(t)[0]=B[t] *)
 t < size -> abit (R1 t) 0 = abit V1 t.
(* Goal: forall (v : BV) (n : nat) (_ : not (@eq nat (lengthbv v) O)), @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (Nat.mul (power2 (S n)) (BV_to_nat (highs v)))) (Nat.mul (power2 n) (BV_to_nat v)) *)
intros. unfold abit in |- *. unfold elemlist in |- *.
(* Goal: @eq BV (trunc bool (strip bool (R1 t) O) (S O)) (trunc bool (strip bool V1 t) (S O)) *)
apply (trunc_plus_petit bool) with (size - t).
(* Goal: le (S O) (S (Nat.sub m t)) *)
(* Goal: le t m *)
(* Goal: @eq (list bool) (trunc bool (strip bool (R1 t) O) (Nat.sub size t)) (strip bool V1 t) *)
unfold lt in H. inversion H. rewrite <- minus_Sn_m. auto with arith. auto with arith.
(* Goal: le (S O) (S (Nat.sub m t)) *)
(* Goal: le t m *)
(* Goal: @eq (list bool) (trunc bool (strip bool (R1 t) O) (Nat.sub size t)) (strip bool V1 t) *)
rewrite <- minus_Sn_m. auto with arith. apply le_Sn_le; auto with arith.
(* Goal: @eq (list bool) (trunc bool (strip bool (R1 t) O) (Nat.sub size t)) (strip bool V1 t) *)
rewrite (strip_O bool). apply R1_lem. apply lt_le_weak. exact H.
Qed.

(****************************************************************)

Lemma lem_le_minus_v1_Sn :
 forall n : nat,
 S n <= size ->
 n <= size ->
 size - S n <= lengthbv (appbv (highs (R1 n)) (consbv (lowbit (R2 n)) nilbv)).

(* Goal: forall (v : BV) (n : nat) (_ : not (@eq nat (lengthbv v) O)), @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (Nat.mul (power2 (S n)) (BV_to_nat (highs v)))) (Nat.mul (power2 n) (BV_to_nat v)) *)
intros. rewrite (length_app bool).
(* Goal: @eq nat (BV_to_nat v) (Nat.add (BV_to_nat (truncbv v (S O))) (Nat.mul (power2 (S O)) (BV_to_nat (highs v)))) *)
(* Goal: not (@eq BV v nilbv) *)
rewrite highs_is_strip. rewrite (length_strip bool). rewrite length_R1.
(* Goal: le (Nat.sub size (S n)) (Nat.add (Nat.sub size (S O)) (S O)) *)
(* Goal: le n size *)
(* Goal: le (S O) (@length bool (R1 n)) *)
simpl in |- *. rewrite plus_comm. rewrite <- le_plus_minus. apply minus_le_lem2.
(* Goal: le (S O) (@length bool (R1 n)) *)
exact le_SO_size. exact H0. rewrite length_R1. exact le_SO_size. exact H0.
Qed.

Lemma BV_to_nat_lem0 :
 forall v : BV,
 lengthbv v <> 0 ->
 BV_to_nat v =
 BV_to_nat (consbv (lowbit v) nilbv) + power2 1 * BV_to_nat (highs v).

(* Goal: forall (v : BV) (n : nat) (_ : not (@eq nat (lengthbv v) O)), @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (Nat.mul (power2 (S n)) (BV_to_nat (highs v)))) (Nat.mul (power2 n) (BV_to_nat v)) *)
intros. rewrite lowbit_is_trunc. rewrite highs_is_strip.
(* Goal: @eq nat (BV_to_nat v) (Nat.add (BV_to_nat (truncbv v (S O))) (Nat.mul (power2 (S O)) (BV_to_nat (stripbv v (S O))))) *)
(* Goal: not (@eq BV v nilbv) *)
replace (power2 1) with (power2 (length (trunc bool v 1))).
(* Goal: @eq nat (BV_to_nat v) (BV_to_nat v) *)
(* Goal: not (@eq BV v nilbv) *)
rewrite <- BV_to_nat_app2. rewrite (app_trunc_strip bool). trivial with arith.
(* Goal: @eq nat (BV_to_nat v) (BV_to_nat v) *)
(* Goal: not (@eq BV v nilbv) *)
rewrite (length_trunc bool). trivial with arith.
(* Goal: not (@eq nat (@length bool v) O) *)
apply (le_SO_length_v bool). exact H. apply (not_nil bool). exact H.
Qed.

Lemma BV_nat_lem1 :
 forall (v : BV) (n : nat),
 lengthbv v <> 0 ->
 power2 n * BV_to_nat (consbv (lowbit v) nilbv) +
 power2 (S n) * BV_to_nat (highs v) = power2 n * BV_to_nat v.

(* Goal: forall (v : BV) (n : nat) (_ : not (@eq nat (lengthbv v) O)), @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (Nat.mul (power2 (S n)) (BV_to_nat (highs v)))) (Nat.mul (power2 n) (BV_to_nat v)) *)
intros. rewrite power2_eq2. rewrite mult_plus_distr_r.
replace (BV_to_nat v) with
 (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v))).
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))) (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))))) (Nat.mul (power2 n) (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v)))) *)
(* Goal: @eq nat (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v))) (BV_to_nat v) *)
rewrite BV_to_nat_app2.
rewrite
 (mult_sym (power2 n)
    (BV_to_nat (consbv (lowbit v) nilbv) +
     power2 (lengthbv (consbv (lowbit v) nilbv)) * BV_to_nat (highs v)))
 .
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (bool_to_nat (lowbit v))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))) (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (bool_to_nat (lowbit v)) (power2 n)) (PeanoNat.Nat.mul (Nat.add (BV_to_nat (highs v)) (BV_to_nat (highs v))) (power2 n))) *)
(* Goal: @eq nat (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v))) (BV_to_nat v) *)
rewrite mult_plus_distr_r.
(* Goal: @eq nat (Nat.add (Nat.mul (power2 n) (BV_to_nat (consbv (lowbit v) nilbv))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))) (PeanoNat.Nat.mul (power2 n) (BV_to_nat (highs v))))) (PeanoNat.Nat.add (PeanoNat.Nat.mul (BV_to_nat (consbv (lowbit v) nilbv)) (power2 n)) (PeanoNat.Nat.mul (Nat.mul (power2 (lengthbv (consbv (lowbit v) nilbv))) (BV_to_nat (highs v))) (power2 n))) *)
(* Goal: @eq nat (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v))) (BV_to_nat v) *)
simpl in |- *. elim plus_n_O. elim plus_n_O. rewrite mult_plus_distr_r.
(* Goal: @eq nat (BV_to_nat v) (BV_to_nat v) *)
(* Goal: not (@eq BV v nilbv) *)
rewrite (mult_sym (power2 n)). rewrite (mult_sym (power2 n)). trivial with arith.
(* Goal: @eq nat (BV_to_nat v) (BV_to_nat v) *)
(* Goal: not (@eq BV v nilbv) *)
rewrite app_lowbit_highs. trivial with arith.
(* Goal: not (@eq nat (@length bool v) O) *)
apply (not_nil bool). exact H.
Qed.
