From 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 17 Oct 2006 12:53:34 +0000 Subject: Mise en forme des theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 272 ++++++++++++++++++++++++------------------------ theories/Bool/Bvector.v | 194 +++++++++++++++++----------------- theories/Bool/DecBool.v | 18 ++-- theories/Bool/Sumbool.v | 47 ++++----- theories/Bool/Zerob.v | 16 +-- 5 files changed, 272 insertions(+), 275 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0c0e2f9ef..85fcde905 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -8,42 +8,40 @@ (*i $Id$ i*) -(** ** Booleans *) - (** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) (** Interpretation of booleans as propositions *) Definition Is_true (b:bool) := match b with - | true => True - | false => False + | true => True + | false => False end. -(*****************) -(** Decidability *) -(*****************) +(*******************) +(** * Decidability *) +(*******************) Lemma bool_dec : forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}. Proof. decide equality. Defined. -(*******************) -(** Discrimination *) -(*******************) +(*********************) +(** * Discrimination *) +(*********************) Lemma diff_true_false : true <> false. Proof. -unfold not in |- *; intro contr; change (Is_true false) in |- *. -elim contr; simpl in |- *; trivial. + unfold not in |- *; intro contr; change (Is_true false) in |- *. + elim contr; simpl in |- *; trivial. Qed. Hint Resolve diff_true_false : bool v62. Lemma diff_false_true : false <> true. Proof. -red in |- *; intros H; apply diff_true_false. -symmetry in |- *. + red in |- *; intros H; apply diff_true_false. + symmetry in |- *. assumption. Qed. Hint Resolve diff_false_true : bool v62. @@ -51,92 +49,92 @@ Hint Extern 1 (false <> true) => exact diff_false_true. Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. Proof. -intros b H; rewrite H; auto with bool. + intros b H; rewrite H; auto with bool. Qed. Lemma not_true_is_false : forall b:bool, b <> true -> b = false. Proof. -destruct b. -intros. -red in H; elim H. -reflexivity. -intros abs. -reflexivity. + destruct b. + intros. + red in H; elim H. + reflexivity. + intros abs. + reflexivity. Qed. Lemma not_false_is_true : forall b:bool, b <> false -> b = true. Proof. -destruct b. -intros. -reflexivity. -intro H; red in H; elim H. -reflexivity. + destruct b. + intros. + reflexivity. + intro H; red in H; elim H. + reflexivity. Qed. (**********************) -(** Order on booleans *) +(** * Order on booleans *) (**********************) Definition leb (b1 b2:bool) := match b1 with - | true => b2 = true - | false => True + | true => b2 = true + | false => True end. Hint Unfold leb: bool v62. (* Infix "<=" := leb : bool_scope. *) (*************) -(** Equality *) +(** * Equality *) (*************) Definition eqb (b1 b2:bool) : bool := match b1, b2 with - | true, true => true - | true, false => false - | false, true => false - | false, false => true + | true, true => true + | true, false => false + | false, true => false + | false, false => true end. Lemma eqb_subst : - forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. -Proof. -unfold eqb in |- *. -intros P b1. -intros b2. -case b1. -case b2. -trivial with bool. -intros H. -inversion_clear H. -case b2. -intros H. -inversion_clear H. -trivial with bool. + forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. +Proof. + unfold eqb in |- *. + intros P b1. + intros b2. + case b1. + case b2. + trivial with bool. + intros H. + inversion_clear H. + case b2. + intros H. + inversion_clear H. + trivial with bool. Qed. Lemma eqb_reflx : forall b:bool, eqb b b = true. Proof. -intro b. -case b. -trivial with bool. -trivial with bool. + intro b. + case b. + trivial with bool. + trivial with bool. Qed. Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b. Proof. -destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity. + destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity. Qed. (************************) -(** Logical combinators *) +(** * Logical combinators *) (************************) Definition ifb (b1 b2 b3:bool) : bool := match b1 with - | true => b2 - | false => b3 + | true => b2 + | false => b3 end. Definition andb (b1 b2:bool) : bool := ifb b1 b2 false. @@ -147,10 +145,10 @@ Definition implb (b1 b2:bool) : bool := ifb b1 b2 true. Definition xorb (b1 b2:bool) : bool := match b1, b2 with - | true, true => false - | true, false => true - | false, true => true - | false, false => false + | true, true => false + | true, false => true + | false, true => true + | false, false => false end. Definition negb (b:bool) := if b then false else true. @@ -165,7 +163,7 @@ Delimit Scope bool_scope with bool. Bind Scope bool_scope with bool. (****************************) -(** De Morgan laws *) +(** * De Morgan laws *) (****************************) Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2. @@ -179,17 +177,17 @@ Proof. Qed. (********************************) -(** *** Properties of [negb] *) +(** * Properties of [negb] *) (********************************) Lemma negb_involutive : forall b:bool, negb (negb b) = b. Proof. -destruct b; reflexivity. + destruct b; reflexivity. Qed. Lemma negb_involutive_reverse : forall b:bool, b = negb (negb b). Proof. -destruct b; reflexivity. + destruct b; reflexivity. Qed. Notation negb_elim := negb_involutive (only parsing). @@ -197,68 +195,68 @@ Notation negb_intro := negb_involutive_reverse (only parsing). Lemma negb_sym : forall b b':bool, b' = negb b -> b = negb b'. Proof. -destruct b; destruct b'; intros; simpl in |- *; trivial with bool. + destruct b; destruct b'; intros; simpl in |- *; trivial with bool. Qed. Lemma no_fixpoint_negb : forall b:bool, negb b <> b. Proof. -destruct b; simpl in |- *; intro; apply diff_true_false; - auto with bool. + destruct b; simpl in |- *; intro; apply diff_true_false; + auto with bool. Qed. Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false. Proof. -destruct b. -trivial with bool. -trivial with bool. + destruct b. + trivial with bool. + trivial with bool. Qed. Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false. Proof. -destruct b. -trivial with bool. -trivial with bool. + destruct b. + trivial with bool. + trivial with bool. Qed. Lemma if_negb : - forall (A:Set) (b:bool) (x y:A), - (if negb b then x else y) = (if b then y else x). + forall (A:Set) (b:bool) (x y:A), + (if negb b then x else y) = (if b then y else x). Proof. destruct b; trivial. Qed. (********************************) -(** *** Properties of [orb] *) +(** * Properties of [orb] *) (********************************) Lemma orb_true_elim : forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. Proof. -destruct b1; simpl in |- *; auto with bool. + destruct b1; simpl in |- *; auto with bool. Defined. Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true. Proof. -destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. + destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); + auto with bool. Qed. Lemma orb_true_intro : - forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true. + forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true. Proof. -destruct b1; auto with bool. -destruct 1; intros. -elim diff_true_false; auto with bool. -rewrite H; trivial with bool. + destruct b1; auto with bool. + destruct 1; intros. + elim diff_true_false; auto with bool. + rewrite H; trivial with bool. Qed. Hint Resolve orb_true_intro: bool v62. Lemma orb_false_intro : - forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. + forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. Proof. -intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool. + intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool. Qed. Hint Resolve orb_false_intro: bool v62. @@ -266,13 +264,13 @@ Hint Resolve orb_false_intro: bool v62. Lemma orb_true_r : forall b:bool, b || true = true. Proof. -auto with bool. + auto with bool. Qed. Hint Resolve orb_true_r: bool v62. Lemma orb_true_l : forall b:bool, true || b = true. Proof. -trivial with bool. + trivial with bool. Qed. Notation orb_b_true := orb_true_r (only parsing). @@ -296,7 +294,7 @@ Notation orb_b_false := orb_false_r (only parsing). Notation orb_false_b := orb_false_l (only parsing). Lemma orb_false_elim : - forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false. + forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false. Proof. destruct b1. intros; elim diff_true_false; auto with bool. @@ -319,7 +317,7 @@ Notation orb_neg_b := orb_negb_r (only parsing). Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1. Proof. -destruct b1; destruct b2; reflexivity. + destruct b1; destruct b2; reflexivity. Qed. (** Associativity *) @@ -330,14 +328,14 @@ Proof. Qed. Hint Resolve orb_comm orb_assoc: bool v62. -(*********************************) -(** *** Properties of [andb] *) -(*********************************) +(*******************************) +(** * Properties of [andb] *) +(*******************************) Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true. Proof. destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. + auto with bool. Qed. Hint Resolve andb_prop: bool v62. @@ -348,7 +346,7 @@ Proof. Defined. Lemma andb_true_intro : - forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. + forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. Proof. destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. @@ -356,24 +354,24 @@ Hint Resolve andb_true_intro: bool v62. Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false. Proof. -destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false. Proof. -destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. (** [false] is a zero for [andb] *) Lemma andb_false_r : forall b:bool, b && false = false. Proof. -destruct b; auto with bool. + destruct b; auto with bool. Qed. Lemma andb_false_l : forall b:bool, false && b = false. Proof. -trivial with bool. + trivial with bool. Qed. Notation andb_b_false := andb_false_r (only parsing). @@ -383,12 +381,12 @@ Notation andb_false_b := andb_false_l (only parsing). Lemma andb_true_r : forall b:bool, b && true = b. Proof. -destruct b; auto with bool. + destruct b; auto with bool. Qed. Lemma andb_true_l : forall b:bool, true && b = b. Proof. -trivial with bool. + trivial with bool. Qed. Notation andb_b_true := andb_true_r (only parsing). @@ -397,7 +395,7 @@ Notation andb_true_b := andb_true_l (only parsing). Lemma andb_false_elim : forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}. Proof. -destruct b1; simpl in |- *; auto with bool. + destruct b1; simpl in |- *; auto with bool. Defined. Hint Resolve andb_false_elim: bool v62. @@ -405,7 +403,7 @@ Hint Resolve andb_false_elim: bool v62. Lemma andb_negb_r : forall b:bool, b && negb b = false. Proof. -destruct b; reflexivity. + destruct b; reflexivity. Qed. Hint Resolve andb_negb_r: bool v62. @@ -415,46 +413,46 @@ Notation andb_neg_b := andb_negb_r (only parsing). Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1. Proof. -destruct b1; destruct b2; reflexivity. + destruct b1; destruct b2; reflexivity. Qed. (** Associativity *) Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3. Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Hint Resolve andb_comm andb_assoc: bool v62. (*******************************************) -(** *** Properties mixing [andb] and [orb] *) +(** * Properties mixing [andb] and [orb] *) (*******************************************) (** Distributivity *) Lemma andb_orb_distrib_r : - forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. + forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Lemma andb_orb_distrib_l : forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3. Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Lemma orb_andb_distrib_r : - forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). + forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Lemma orb_andb_distrib_l : - forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3). + forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3). Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. (* Compatibility *) @@ -475,9 +473,9 @@ Proof. destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. -(***********************************) -(** *** Properties of [xorb] *) -(***********************************) +(*********************************) +(** * Properties of [xorb] *) +(*********************************) Lemma xorb_false : forall b:bool, xorb b false = b. Proof. @@ -510,7 +508,7 @@ Proof. Qed. Lemma xorb_assoc : - forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b''). + forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b''). Proof. destruct b; destruct b'; destruct b''; trivial. Qed. @@ -522,26 +520,26 @@ Proof. Qed. Lemma xorb_move_l_r_1 : - forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''. + forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''. Proof. intros. rewrite <- (false_xorb b'). rewrite <- (xorb_nilpotent b). rewrite xorb_assoc. rewrite H. reflexivity. Qed. Lemma xorb_move_l_r_2 : - forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'. + forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'. Proof. intros. rewrite xorb_comm in H. rewrite (xorb_move_l_r_1 b' b b'' H). apply xorb_comm. Qed. Lemma xorb_move_r_l_1 : - forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''. + forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''. Proof. intros. rewrite H. rewrite <- xorb_assoc. rewrite xorb_nilpotent. apply false_xorb. Qed. Lemma xorb_move_r_l_2 : - forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'. + forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'. Proof. intros. rewrite H. rewrite xorb_assoc. rewrite xorb_nilpotent. apply xorb_false. Qed. @@ -550,7 +548,7 @@ Qed. Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. Proof. - intros b1 b2; case b1; case b2; intuition. + intros b1 b2; case b1; case b2; intuition. Qed. Notation bool_1 := eq_true_iff_eq. (* Compatibility *) @@ -596,7 +594,7 @@ Qed. Hint Resolve trans_eq_bool. (*****************************************) -(** *** Reflection of [bool] into [Prop] *) +(** * Reflection of [bool] into [Prop] *) (*****************************************) (** [Is_true] and equality *) @@ -605,9 +603,9 @@ Hint Unfold Is_true: bool. Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true. Proof. -destruct x; simpl in |- *; tauto. + destruct x; simpl in |- *; tauto. Qed. - + Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x. Proof. intros; rewrite H; auto with bool. @@ -635,7 +633,7 @@ Qed. (** [Is_true] and connectives *) Lemma orb_prop_elim : - forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. + forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. Proof. destruct a; destruct b; simpl; tauto. Qed. @@ -643,13 +641,13 @@ Qed. Notation orb_prop2 := orb_prop_elim (only parsing). Lemma orb_prop_intro : - forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b). + forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b). Proof. destruct a; destruct b; simpl; tauto. Qed. Lemma andb_prop_intro : - forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2). + forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2). Proof. destruct b1; destruct b2; simpl in |- *; tauto. Qed. @@ -660,42 +658,42 @@ Notation andb_true_intro2 := (only parsing). Lemma andb_prop_elim : - forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b. + forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b. Proof. destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. + auto with bool. Qed. 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. + forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. Proof. - destruct b1; destruct b2; simpl in *; intuition. + 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. - intros b1 b2; case b1; case b2; intuition. + intros b1 b2; case b1; case b2; intuition. Qed. Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b. Proof. - destruct b; intuition. + destruct b; intuition. Qed. Lemma negb_prop_intro : forall b, ~ Is_true b -> Is_true (negb b). Proof. - destruct b; simpl in *; intuition. + destruct b; simpl in *; intuition. Qed. Lemma negb_prop_classical : forall b, ~ Is_true (negb b) -> Is_true b. Proof. - destruct b; intuition. + destruct b; intuition. Qed. Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b). Proof. - destruct b; intuition. + destruct b; intuition. Qed. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 1c965c7e0..d4d8386c4 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -16,34 +16,34 @@ 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 +La dimension du vecteur est un paramètre trop important pour se contenter de la fonction "length". -La première idée est de faire un record avec la liste et la longueur. +La première idée est de faire un record avec la liste et la longueur. Malheureusement, cette verification a posteriori amene a faire de nombreux lemmes pour gerer les longueurs. -La seconde idée est de faire un type dépendant dans lequel la -longueur est un paramètre de construction. Cela complique un -peu les inductions structurelles, la solution qui a ma préférence -est alors d'utiliser un terme de preuve comme définition, car le -mécanisme d'inférence du type du filtrage n'est pas aussi puissant que -celui implanté par les tactiques d'élimination. +La seconde idée est de faire un type dépendant dans lequel la +longueur est un paramètre de construction. Cela complique un +peu les inductions structurelles, la solution qui a ma préférence +est alors d'utiliser un terme de preuve comme définition, car le +mécanisme d'inférence du type du filtrage n'est pas 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 -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 couple de vecteurs -de taille n dans les vecteurs de taille n en appliquant f terme à terme. +(** +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 +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 +de taille n dans les vecteurs de taille n en appliquant f terme à terme. *) Variable A : Type. @@ -54,129 +54,129 @@ Inductive vector : nat -> Type := Definition Vhead : forall n:nat, vector (S n) -> A. Proof. - intros n v; inversion v; exact a. + intros n v; inversion v; exact a. Defined. Definition Vtail : forall n:nat, vector (S n) -> vector n. Proof. - intros n v; inversion v as [|_ n0 H0 H1]; exact H0. + intros n v; inversion v as [|_ n0 H0 H1]; exact H0. Defined. 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). + induction n as [| n f]; intro v. + inversion v. + exact a. + + inversion v as [| n0 a H0 H1]. + exact (f H0). Defined. Definition Vconst : forall (a:A) (n:nat), vector n. Proof. - induction n as [| n v]. - exact Vnil. + induction n as [| n v]. + exact Vnil. - exact (Vcons a n v). + exact (Vcons a n v). Defined. 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)). + 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)). + 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)). + 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 *. + 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. Lemma Vextend : forall n p:nat, vector n -> vector p -> vector (n + p). Proof. - induction n as [| n f]; intros p v v0. - simpl in |- *; exact v0. - - inversion v as [| a n0 H0 H1]. - simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). + induction n as [| n f]; intros p v v0. + simpl in |- *; exact v0. + + inversion v as [| a n0 H0 H1]. + simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). Defined. Variable f : A -> A. Lemma Vunary : forall n:nat, vector n -> vector n. Proof. - induction n as [| n g]; intro v. - exact Vnil. - - inversion v as [| a n0 H0 H1]. - exact (Vcons (f a) n (g H0)). + induction n as [| n g]; intro v. + exact Vnil. + + inversion v as [| a n0 H0 H1]. + exact (Vcons (f a) n (g H0)). Defined. 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)). + 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. Definition Vid : forall n:nat, vector n -> vector n. Proof. -destruct n; intro X. -exact Vnil. -exact (Vcons (Vhead _ X) _ (Vtail _ X)). + destruct n; intro X. + exact Vnil. + exact (Vcons (Vhead _ X) _ (Vtail _ X)). Defined. Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v). Proof. -destruct v; auto. + 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). + intros. + exact (Vid_eq _ v). Qed. Lemma V0_eq : forall (v : vector 0), v = Vnil. Proof. -intros. -exact (Vid_eq _ v). + intros. + exact (Vid_eq _ v). Qed. End VECTORS. @@ -188,15 +188,15 @@ Implicit Arguments Vcons [A n]. Section BOOLEAN_VECTORS. -(* -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. +(** +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 +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 -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 +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). *) @@ -234,24 +234,24 @@ Definition BshiftRa (n:nat) (bv:Bvector (S n)) := Bhigh (S n) (Vshiftrepeat bool n bv). Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : - Bvector (S n) := + Bvector (S n) := match p with - | O => bv - | S p' => BshiftL n (BshiftL_iter n bv p') false + | O => bv + | S p' => BshiftL n (BshiftL_iter n bv p') false end. Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : - Bvector (S n) := + Bvector (S n) := match p with - | O => bv - | S p' => BshiftRl n (BshiftRl_iter n bv p') false + | O => bv + | S p' => BshiftRl n (BshiftRl_iter n bv p') false end. Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : - Bvector (S n) := + Bvector (S n) := match p with - | O => bv - | S p' => BshiftRa n (BshiftRa_iter n bv p') + | O => bv + | S p' => BshiftRa n (BshiftRa_iter n bv p') end. End BOOLEAN_VECTORS. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 82363fff7..90f7ee662 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -15,17 +15,19 @@ Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C := Theorem ifdec_left : - forall (A B:Prop) (C:Set) (H:{A} + {B}), - ~ B -> forall x y:C, ifdec H x y = x. -intros; case H; auto. -intro; absurd B; trivial. + forall (A B:Prop) (C:Set) (H:{A} + {B}), + ~ B -> forall x y:C, ifdec H x y = x. +Proof. + intros; case H; auto. + intro; absurd B; trivial. Qed. Theorem ifdec_right : - forall (A B:Prop) (C:Set) (H:{A} + {B}), - ~ A -> forall x y:C, ifdec H x y = y. -intros; case H; auto. -intro; absurd A; trivial. + forall (A B:Prop) (C:Set) (H:{A} + {B}), + ~ A -> forall x y:C, ifdec H x y = y. +Proof. + intros; case H; auto. + intro; absurd A; trivial. Qed. Unset Implicit Arguments. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 1beb45f13..03aa8baeb 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -16,7 +16,6 @@ (** A boolean is either [true] or [false], and this is decidable *) Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}. -Proof. destruct b; auto. Defined. @@ -25,41 +24,36 @@ Hint Resolve sumbool_of_bool: bool. Definition bool_eq_rec : forall (b:bool) (P:bool -> Set), (b = true -> P true) -> (b = false -> P false) -> P b. -destruct b; auto. + destruct b; auto. Defined. Definition bool_eq_ind : forall (b:bool) (P:bool -> Prop), (b = true -> P true) -> (b = false -> P false) -> P b. -destruct b; auto. + destruct b; auto. Defined. -(*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ? Papageno i*) - (** Logic connectives on type [sumbool] *) Section connectives. -Variables A B C D : Prop. - -Hypothesis H1 : {A} + {B}. -Hypothesis H2 : {C} + {D}. - -Definition sumbool_and : {A /\ C} + {B \/ D}. -Proof. -case H1; case H2; auto. -Defined. - -Definition sumbool_or : {A \/ C} + {B /\ D}. -Proof. -case H1; case H2; auto. -Defined. - -Definition sumbool_not : {B} + {A}. -Proof. -case H1; auto. -Defined. + 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. End connectives. @@ -71,8 +65,7 @@ Hint Immediate sumbool_not : core. Definition bool_of_sumbool : forall A B:Prop, {A} + {B} -> {b : bool | if b then A else B}. -Proof. -intros A B H. -elim H; [ intro; exists true; assumption | intro; exists false; assumption ]. + intros A B H. + elim H; intro; [exists true | exists false]; assumption. Defined. Implicit Arguments bool_of_sumbool. \ No newline at end of file diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index eac13569a..5e9d4afa6 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -15,24 +15,28 @@ Open Local Scope nat_scope. Definition zerob (n:nat) : bool := match n with - | O => true - | S _ => false + | O => true + | S _ => false end. Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. -destruct n; [ trivial with bool | inversion 1 ]. +Proof. + destruct n; [ trivial with bool | inversion 1 ]. Qed. Hint Resolve zerob_true_intro: bool. Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. -destruct n; [ trivial with bool | inversion 1 ]. +Proof. + destruct n; [ trivial with bool | inversion 1 ]. Qed. Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. -destruct n; [ destruct 1; auto with bool | trivial with bool ]. +Proof. + destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. Hint Resolve zerob_false_intro: bool. Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. -destruct n; [ intro H; inversion H | auto with bool ]. +Proof. + destruct n; [ inversion 1 | auto with bool ]. Qed. \ No newline at end of file -- cgit v1.2.3