diff options
Diffstat (limited to 'theories/Bool')
| -rw-r--r-- | theories/Bool/Bool.v | 33 | ||||
| -rw-r--r-- | theories/Bool/BoolEq.v | 3 | ||||
| -rw-r--r-- | theories/Bool/Bvector.v | 197 | ||||
| -rw-r--r-- | theories/Bool/DecBool.v | 4 | ||||
| -rw-r--r-- | theories/Bool/IfProp.v | 6 | ||||
| -rw-r--r-- | theories/Bool/Sumbool.v | 6 | ||||
| -rw-r--r-- | theories/Bool/Zerob.v | 6 |
7 files changed, 57 insertions, 198 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 9509d9fd..d5d11cea 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Bool.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) @@ -259,6 +257,11 @@ Proof. intros. apply orb_false_iff; trivial. Qed. +Lemma orb_diag : forall b, b || b = b. +Proof. + destr_bool. +Qed. + (** [true] is a zero for [orb] *) Lemma orb_true_r : forall b:bool, b || true = true. @@ -364,6 +367,11 @@ Qed. Notation andb_b_false := andb_false_r (only parsing). Notation andb_false_b := andb_false_l (only parsing). +Lemma andb_diag : forall b, b && b = b. +Proof. + destr_bool. +Qed. + (** [true] is neutral for [andb] *) Lemma andb_true_r : forall b:bool, b && true = b. @@ -547,6 +555,21 @@ Proof. destr_bool. Qed. +Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'. +Proof. + destruct b,b'; trivial. +Qed. + +Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b'). +Proof. + destruct b,b'; trivial. +Qed. + +Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'. +Proof. + destruct b,b'; trivial. +Qed. + (** Lemmas about the [b = true] embedding of [bool] to [Prop] *) Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true). @@ -768,7 +791,7 @@ Qed. Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b. Proof. destr_bool; intuition. -Qed. +Defined. (** It would be nice to join [reflect_iff] and [iff_reflect] in a unique [iff] statement, but this isn't allowed since @@ -779,7 +802,7 @@ Qed. Lemma reflect_dec : forall P b, reflect P b -> {P}+{~P}. Proof. destruct 1; auto. -Qed. +Defined. (** Reciprocally, from a decidability, we could state a [reflect] as soon as we have a [bool_of_sumbool]. *) diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index ee82caf1..d40e56bf 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BoolEq.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Cuihtlauac Alvarado - octobre 2000 *) (** Properties of a boolean equality *) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index daf3a9fb..0c218163 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -1,18 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Bvector.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) -Require Export Bool. -Require Export Sumbool. -Require Import Arith. +Require Export Bool Sumbool. +Require Vector. +Export Vector.VectorNotations. +Require Import Minus. Open Local Scope nat_scope. @@ -30,161 +29,6 @@ as definition, since the type inference mechanism for pattern-matching is sometimes weaker that the one implemented for elimination tactiques. *) -Section VECTORS. - -(** -A vector is a list of size n whose elements belongs to a set A. -If the size is non-zero, we can extract the first component and the -rest of the vector, as well as the last component, or adding or -removing a component (carry) or repeating the last component at the -end of the vector. -We can also truncate the vector and remove its p last components or -reciprocally extend the vector by concatenation. -A unary function over A generates a function on vectors of size n by -applying f pointwise. -A binary function over A generates a function on pairs of vectors of -size n by applying f pointwise. -*) - -Variable A : Type. - -Inductive vector : nat -> Type := - | Vnil : vector 0 - | Vcons : forall (a:A) (n:nat), vector n -> vector (S n). - -Definition Vhead (n:nat) (v:vector (S n)) := - match v with - | Vcons a _ _ => a - end. - -Definition Vtail (n:nat) (v:vector (S n)) := - match v with - | Vcons _ _ v => v - end. - -Definition Vlast : forall n:nat, vector (S n) -> A. -Proof. - induction n as [| n f]; intro v. - inversion v. - exact a. - - inversion v as [| n0 a H0 H1]. - exact (f H0). -Defined. - -Fixpoint Vconst (a:A) (n:nat) := - match n return vector n with - | O => Vnil - | S n => Vcons a _ (Vconst a n) - end. - -(** Shifting and truncating *) - -Lemma Vshiftout : forall n:nat, vector (S n) -> vector n. -Proof. - induction n as [| n f]; intro v. - exact Vnil. - - inversion v as [| a n0 H0 H1]. - exact (Vcons a n (f H0)). -Defined. - -Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n). -Proof. - induction n as [| n f]; intros a v. - exact (Vcons a 0 v). - - inversion v as [| a0 n0 H0 H1 ]. - exact (Vcons a (S n) (f a H0)). -Defined. - -Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)). -Proof. - induction n as [| n f]; intro v. - inversion v. - exact (Vcons a 1 v). - - inversion v as [| a n0 H0 H1 ]. - exact (Vcons a (S (S n)) (f H0)). -Defined. - -Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p). -Proof. - induction p as [| p f]; intros H v. - rewrite <- minus_n_O. - exact v. - - apply (Vshiftout (n - S p)). - - rewrite minus_Sn_m. - apply f. - auto with *. - exact v. - auto with *. -Defined. - -(** Concatenation of two vectors *) - -Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) := - match v with - | Vnil => w - | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w) - end. - -(** Uniform application on the arguments of the vector *) - -Variable f : A -> A. - -Fixpoint Vunary n (v:vector n) : vector n := - match v with - | Vnil => Vnil - | Vcons a n' v' => Vcons (f a) n' (Vunary n' v') - end. - -Variable g : A -> A -> A. - -Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n. -Proof. - induction n as [| n h]; intros v v0. - exact Vnil. - - inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3]. - exact (Vcons (g a a0) n (h H0 H2)). -Defined. - -(** Eta-expansion of a vector *) - -Definition Vid n : vector n -> vector n := - match n with - | O => fun _ => Vnil - | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v) - end. - -Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v. -Proof. - destruct v; auto. -Qed. - -Lemma VSn_eq : - forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v). -Proof. - intros. - exact (Vid_eq _ v). -Qed. - -Lemma V0_eq : forall (v : vector 0), v = Vnil. -Proof. - intros. - exact (Vid_eq _ v). -Qed. - -End VECTORS. - -(* suppressed: incompatible with Coq-Art book -Implicit Arguments Vnil [A]. -Implicit Arguments Vcons [A n]. -*) - Section BOOLEAN_VECTORS. (** @@ -200,38 +44,38 @@ NOTA BENE: all shift operations expect predecessor of size as parameter (they only work on non-empty vectors). *) -Definition Bvector := vector bool. +Definition Bvector := Vector.t bool. -Definition Bnil := @Vnil bool. +Definition Bnil := @Vector.nil bool. -Definition Bcons := @Vcons bool. +Definition Bcons := @Vector.cons bool. -Definition Bvect_true := Vconst bool true. +Definition Bvect_true := Vector.const true. -Definition Bvect_false := Vconst bool false. +Definition Bvect_false := Vector.const false. -Definition Blow := Vhead bool. +Definition Blow := @Vector.hd bool. -Definition Bhigh := Vtail bool. +Definition Bhigh := @Vector.tl bool. -Definition Bsign := Vlast bool. +Definition Bsign := @Vector.last bool. -Definition Bneg := Vunary bool negb. +Definition Bneg n (v : Bvector n) := Vector.map negb v. -Definition BVand := Vbinary bool andb. +Definition BVand n (v : Bvector n) := Vector.map2 andb v. -Definition BVor := Vbinary bool orb. +Definition BVor n (v : Bvector n) := Vector.map2 orb v. -Definition BVxor := Vbinary bool xorb. +Definition BVxor n (v : Bvector n) := Vector.map2 xorb v. Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) := - Bcons carry n (Vshiftout bool n bv). + Bcons carry n (Vector.shiftout bv). Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) := - Bhigh (S n) (Vshiftin bool (S n) carry bv). + Bhigh (S n) (Vector.shiftin carry bv). Definition BshiftRa (n:nat) (bv:Bvector (S n)) := - Bhigh (S n) (Vshiftrepeat bool n bv). + Bhigh (S n) (Vector.shiftrepeat bv). Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with @@ -252,3 +96,4 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := end. End BOOLEAN_VECTORS. + diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index e49d1f97..3f03d2c1 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: DecBool.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C := diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 9cca05d4..6872eaea 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: IfProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Bool. Inductive IfProp (A B:Prop) : bool -> Prop := @@ -47,4 +45,4 @@ Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. destruct b; intro H. left; inversion H; auto with bool. right; inversion H; auto with bool. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 5b1822be..24b6a776 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sumbool.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Here are collected some results about the type sumbool (see INIT/Specif.v) [sumbool A B], which is written [{A}+{B}], is the informative disjunction "A or B", where A and B are logical propositions. @@ -68,4 +66,4 @@ Definition bool_of_sumbool : intros A B H. elim H; intro; [exists true | exists false]; assumption. Defined. -Implicit Arguments bool_of_sumbool.
\ No newline at end of file +Arguments bool_of_sumbool : default implicits. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index e67ba677..bac4c0d6 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zerob.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Arith. Require Import Bool. @@ -39,4 +37,4 @@ Hint Resolve zerob_false_intro: bool. Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. Proof. destruct n; [ inversion 1 | auto with bool ]. -Qed.
\ No newline at end of file +Qed. |