(* 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)                    *)

(*                     --- shift.v ---                                      *)

(*                                                                          *)
(* Author: Pierre Casteran.                                                 *)
(*    LABRI, URA CNRS 1304,                                                 *)
(*    Departement d'Informatique, Universite Bordeaux I,                    *)
(*    33405 Talence CEDEX,                                                  *)
(*    e-mail:  casteran@labri.u-bordeaux.fr                                 *)

(* 
  Many programmers use left and right shifts in their code;
  so we found useful to provide some definitions and lemmas
  about these operations.
*)

Require Import Arith.
Require Import Peano_dec.
Require Import Constants.
Require Import Mult_compl.
Require Import Wf_nat. 
Require Import euclid.
Require Import Le_lt_compl.
Require Import Euclid.
Require Import Compare_dec.

Lemma plus_n_1 : forall n : nat, S n = n + 1.
Proof.
(* Goal: forall n : nat, @eq nat (S n) (Init.Nat.add n (S O)) *)
 intro n; rewrite <- (plus_n_Sm n 0); auto with arith.
Qed.


(* machine arithmetics *)

(* Left shift *)

Definition shift (n : nat) := two * n.
(************************************)

(* Right shift (and information on parity) *)

Lemma Unshift :
 forall n : nat, {m : nat &  {n = shift m} + {n = S (shift m)}}.
(*************************************************************)
Proof.
refine
 (fun n => match eucl_dev two _ n with
           | divex q r g e => existS _ q _
           end).
(* Goal: gt two O *)
(* Goal: sumbool (@eq nat n (shift q)) (@eq nat n (S (shift q))) *)
unfold two in |- *; auto.
(* Goal: sumbool (@eq nat n (shift q)) (@eq nat n (S (shift q))) *)
elim (zerop r); intro e0; [ left | right ].
(*
 Realizer [n:nat]<nat*bool>let (q,r:nat)=(eucl_dev two n)
                in (q,(zerop r)).
 Program_all.
 *)
 rewrite e; rewrite e0; rewrite <- plus_n_O; unfold shift in |- *;
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
  auto with arith.
(* Goal: @eq nat n (S (shift q)) *)
 cut (r = 1).
(* Goal: forall _ : @eq nat r (S O), @eq nat n (S (shift q)) *)
(* Goal: @eq nat r (S O) *)
 intro eq1.
(* Goal: @eq nat n (S (shift q)) *)
(* Goal: @eq nat r (S O) *)
 rewrite e; rewrite eq1.
(* Goal: lt a (Init.Nat.add (shift a) (S O)) *)
(* Goal: lt a b *)
 unfold shift in |- *.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul q two) (S O)) (S (Init.Nat.mul two q)) *)
(* Goal: @eq nat r (S O) *)
 rewrite <- plus_n_1; auto with arith.
(* Goal: @eq nat r (S O) *)
 case (enum1 r).
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
 auto with arith.
(* Goal: forall _ : @eq nat r O, @eq nat r (S O) *)
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
 intro e'; absurd (0 < r); [ elim e'; auto with arith | auto with arith ].
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
 auto with arith.
Qed.


Lemma half_lt :
 forall a b : nat, 0 < b -> b = shift a \/ b = S (shift a) -> a < b.
(********************************************************)
Proof.
(* Goal: forall (a b : nat) (_ : lt O b) (_ : or (@eq nat b (shift a)) (@eq nat b (S (shift a)))), lt a b *)
 intros; case (lt_or_Zero a); intro.
(* Goal: lt a b *)
(* Goal: lt a b *)
 case H0; intro.
(* Goal: lt a b *)
(* Goal: lt a b *)
 rewrite H2.
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
 unfold shift in |- *; apply mult_p_lt_qp; auto with arith.
(* Goal: lt a b *)
(* Goal: lt a b *)
 rewrite H2.
(* Goal: lt a (S (shift a)) *)
(* Goal: lt a b *)
 rewrite plus_n_1.
(* Goal: lt a (Init.Nat.add (shift a) (S O)) *)
(* Goal: lt a b *)
 unfold shift in |- *.
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
 rewrite mult_comm; apply lt_q_qbr; auto with arith.
(* Goal: forall _ : @eq nat r (S O), @eq nat r (S O) *)
 rewrite H1; auto with arith.
Qed.
Hint Resolve half_lt: arith.









