From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 42 +++++++++++++++++++++--------------------- theories/Bool/Bvector.v | 28 ++++++++++++++-------------- theories/Bool/Sumbool.v | 8 ++++---- 3 files changed, 39 insertions(+), 39 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index dcb10f3cf..bc42c6564 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -39,7 +39,7 @@ Qed. Hint Resolve diff_true_false : bool v62. Lemma diff_false_true : false <> true. -Proof. +Proof. red in |- *; intros H; apply diff_true_false. symmetry in |- *. assumption. @@ -129,7 +129,7 @@ Qed. (************************) (** * A synonym of [if] on [bool] *) (************************) - + Definition ifb (b1 b2 b3:bool) : bool := match b1 with | true => b2 @@ -186,7 +186,7 @@ Proof. trivial with bool. trivial with bool. Qed. - + Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false. Proof. destruct b. @@ -318,7 +318,7 @@ Hint Resolve orb_comm orb_assoc: bool v62. (** * Properties of [andb] *) (*******************************) -Lemma andb_true_iff : +Lemma andb_true_iff : forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true. Proof. destruct b1; destruct b2; intuition. @@ -382,7 +382,7 @@ Hint Resolve andb_false_elim: bool v62. Lemma andb_negb_r : forall b:bool, b && negb b = false. Proof. destruct b; reflexivity. -Qed. +Qed. Hint Resolve andb_negb_r: bool v62. Notation andb_neg_b := andb_negb_r (only parsing). @@ -542,8 +542,8 @@ Qed. (** Lemmas about the [b = true] embedding of [bool] to [Prop] *) -Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. -Proof. +Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. +Proof. intros b1 b2; case b1; case b2; intuition. Qed. @@ -556,7 +556,7 @@ Qed. Notation bool_3 := eq_true_negb_classical (only parsing). (* Compatibility *) -Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true. +Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true. Proof. destruct b; intuition. Qed. @@ -628,7 +628,7 @@ Qed. (** [Is_true] and connectives *) -Lemma orb_prop_elim : +Lemma orb_prop_elim : forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. Proof. destruct a; destruct b; simpl; tauto. @@ -636,7 +636,7 @@ Qed. Notation orb_prop2 := orb_prop_elim (only parsing). -Lemma orb_prop_intro : +Lemma orb_prop_intro : forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b). Proof. destruct a; destruct b; simpl; tauto. @@ -663,16 +663,16 @@ Hint Resolve andb_prop_elim: bool v62. Notation andb_prop2 := andb_prop_elim (only parsing). -Lemma eq_bool_prop_intro : - forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. -Proof. +Lemma eq_bool_prop_intro : + forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. +Proof. destruct b1; destruct b2; simpl in *; intuition. Qed. Lemma eq_bool_prop_elim : forall b1 b2, b1 = b2 -> (Is_true b1 <-> Is_true b2). -Proof. +Proof. intros b1 b2; case b1; case b2; intuition. -Qed. +Qed. Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b. Proof. @@ -696,26 +696,26 @@ Qed. (** Rewrite rules about andb, orb and if (used in romega) *) -Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), - (if b && b' then a else a') = +Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), + (if b && b' then a else a') = (if b then if b' then a else a' else a'). Proof. destruct b; destruct b'; auto. Qed. -Lemma negb_if : forall (A:Type)(a a':A)(b:bool), - (if negb b then a else a') = +Lemma negb_if : forall (A:Type)(a a':A)(b:bool), + (if negb b then a else a') = (if b then a' else a). Proof. destruct b; auto. Qed. (*****************************************) -(** * Alternative versions of [andb] and [orb] +(** * Alternative versions of [andb] and [orb] with lazy behavior (for vm_compute) *) (*****************************************) -Notation "a &&& b" := (if a then b else false) +Notation "a &&& b" := (if a then b else false) (at level 40, left associativity) : lazy_bool_scope. Notation "a ||| b" := (if a then true else b) (at level 50, left associativity) : lazy_bool_scope. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 9dbd90f05..2682a8848 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -16,7 +16,7 @@ Require Import Arith. Open Local Scope nat_scope. -(** +(** On s'inspire de List.v pour fabriquer les vecteurs de bits. La dimension du vecteur est un paramètre trop important pour se contenter de la fonction "length". @@ -27,22 +27,22 @@ La seconde id longueur est un paramètre de construction. Cela complique un peu les inductions structurelles et dans certains cas on utilisera un terme de preuve comme définition, car le -mécanisme d'inférence du type du filtrage n'est pas toujours +mécanisme d'inférence du type du filtrage n'est pas toujours aussi puissant que celui implanté par les tactiques d'élimination. *) Section VECTORS. -(** +(** Un vecteur est une liste de taille n d'éléments d'un ensemble A. -Si la taille est non nulle, on peut extraire la première composante et -le reste du vecteur, la dernière composante ou rajouter ou enlever +Si la taille est non nulle, on peut extraire la première composante et +le reste du vecteur, la dernière composante ou rajouter ou enlever une composante (carry) ou repeter la dernière composante en fin de vecteur. On peut aussi tronquer le vecteur de ses p dernières composantes ou au contraire l'étendre (concaténer) d'un vecteur de longueur p. Une fonction unaire sur A génère une fonction des vecteurs de taille n dans les vecteurs de taille n en appliquant f terme à terme. -Une fonction binaire sur A génère une fonction des couples de vecteurs +Une fonction binaire sur A génère une fonction des couples de vecteurs de taille n dans les vecteurs de taille n en appliquant f terme à terme. *) @@ -93,7 +93,7 @@ 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. @@ -103,7 +103,7 @@ 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. @@ -113,9 +113,9 @@ 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 *. @@ -147,7 +147,7 @@ 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. @@ -180,7 +180,7 @@ Qed. End VECTORS. -(* suppressed: incompatible with Coq-Art book +(* suppressed: incompatible with Coq-Art book Implicit Arguments Vnil [A]. Implicit Arguments Vcons [A n]. *) @@ -188,12 +188,12 @@ Implicit Arguments Vcons [A n]. Section BOOLEAN_VECTORS. (** -Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. +Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. ATTENTION : le stockage s'effectue poids FAIBLE en tête. On en extrait le bit de poids faible (head) et la fin du vecteur (tail). On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs. On calcule les décalages d'une position vers la gauche (vers les poids forts, on -utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en +utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique). ATTENTION : Tous les décalages prennent la taille moins un comme paramètre (ils ne travaillent que sur des vecteurs au moins de longueur un). diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 03aa8baeb..06ab77cfb 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -39,18 +39,18 @@ Defined. Section connectives. Variables A B C D : Prop. - + Hypothesis H1 : {A} + {B}. Hypothesis H2 : {C} + {D}. - + Definition sumbool_and : {A /\ C} + {B \/ D}. case H1; case H2; auto. Defined. - + Definition sumbool_or : {A \/ C} + {B /\ D}. case H1; case H2; auto. Defined. - + Definition sumbool_not : {B} + {A}. case H1; auto. Defined. -- cgit v1.2.3