diff options
Diffstat (limited to 'theories7/Bool')
-rwxr-xr-x | theories7/Bool/Bool.v | 544 | ||||
-rw-r--r-- | theories7/Bool/BoolEq.v | 72 | ||||
-rw-r--r-- | theories7/Bool/Bvector.v | 266 | ||||
-rwxr-xr-x | theories7/Bool/DecBool.v | 27 | ||||
-rwxr-xr-x | theories7/Bool/IfProp.v | 49 | ||||
-rw-r--r-- | theories7/Bool/Sumbool.v | 77 | ||||
-rwxr-xr-x | theories7/Bool/Zerob.v | 36 |
7 files changed, 0 insertions, 1071 deletions
diff --git a/theories7/Bool/Bool.v b/theories7/Bool/Bool.v deleted file mode 100755 index cd75cf30..00000000 --- a/theories7/Bool/Bool.v +++ /dev/null @@ -1,544 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Bool.v,v 1.2.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) - -(** Booleans *) - -(** The type [bool] is defined in the prelude as - [Inductive bool : Set := true : bool | false : bool] *) - -(** Interpretation of booleans as Proposition *) -Definition Is_true := [b:bool](Cases b of - true => True - | false => False - end). -Hints Unfold Is_true : bool. - -Lemma Is_true_eq_left : (x:bool)x=true -> (Is_true x). -Proof. - Intros; Rewrite H; Auto with bool. -Qed. - -Lemma Is_true_eq_right : (x:bool)true=x -> (Is_true x). -Proof. - Intros; Rewrite <- H; Auto with bool. -Qed. - -Hints Immediate Is_true_eq_right Is_true_eq_left : bool. - -(*******************) -(** Discrimination *) -(*******************) - -Lemma diff_true_false : ~true=false. -Proof. -Unfold not; Intro contr; Change (Is_true false). -Elim contr; Simpl; Trivial with bool. -Qed. -Hints Resolve diff_true_false : bool v62. - -Lemma diff_false_true : ~false=true. -Proof. -Red; Intros H; Apply diff_true_false. -Symmetry. -Assumption. -Qed. -Hints Resolve diff_false_true : bool v62. - -Lemma eq_true_false_abs : (b:bool)(b=true)->(b=false)->False. -Intros b H; Rewrite H; Auto with bool. -Qed. -Hints Resolve eq_true_false_abs : bool. - -Lemma not_true_is_false : (b:bool)~b=true->b=false. -NewDestruct b. -Intros. -Red in H; Elim H. -Reflexivity. -Intros abs. -Reflexivity. -Qed. - -Lemma not_false_is_true : (b:bool)~b=false->b=true. -NewDestruct b. -Intros. -Reflexivity. -Intro H; Red in H; Elim H. -Reflexivity. -Qed. - -(**********************) -(** Order on booleans *) -(**********************) - -Definition leb := [b1,b2:bool] - Cases b1 of - | true => b2=true - | false => True - end. -Hints Unfold leb : bool v62. - -(*************) -(** Equality *) -(*************) - -Definition eqb : bool->bool->bool := - [b1,b2:bool] - Cases b1 b2 of - true true => true - | true false => false - | false true => false - | false false => true - end. - -Lemma eqb_refl : (x:bool)(Is_true (eqb x x)). -NewDestruct x; Simpl; Auto with bool. -Qed. - -Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y. -NewDestruct x; NewDestruct y; Simpl; Tauto. -Qed. - -Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true. -NewDestruct x; Simpl; Tauto. -Qed. - -Lemma Is_true_eq_true2 : (x:bool) x=true -> (Is_true x). -NewDestruct x; Simpl; Auto with bool. -Qed. - -Lemma eqb_subst : - (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2). -Unfold eqb . -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 : (b:bool)(eqb b b)=true. -Intro b. -Case b. -Trivial with bool. -Trivial with bool. -Qed. - -Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b. -NewDestruct a; NewDestruct b; Simpl; Intro; - Discriminate H Orelse Reflexivity. -Qed. - - -(************************) -(** Logical combinators *) -(************************) - -Definition ifb : bool -> bool -> bool -> bool - := [b1,b2,b3:bool](Cases b1 of true => b2 | false => b3 end). - -Definition andb : bool -> bool -> bool - := [b1,b2:bool](ifb b1 b2 false). - -Definition orb : bool -> bool -> bool - := [b1,b2:bool](ifb b1 true b2). - -Definition implb : bool -> bool -> bool - := [b1,b2:bool](ifb b1 b2 true). - -Definition xorb : bool -> bool -> bool - := [b1,b2:bool] - Cases b1 b2 of - true true => false - | true false => true - | false true => true - | false false => false - end. - -Definition negb := [b:bool]Cases b of - true => false - | false => true - end. - -Infix "||" orb (at level 4, left associativity) : bool_scope. -Infix "&&" andb (at level 3, no associativity) : bool_scope - V8only (at level 40, left associativity). - -Open Scope bool_scope. - -Delimits Scope bool_scope with bool. - -Bind Scope bool_scope with bool. - -(**************************) -(** Lemmas about [negb] *) -(**************************) - -Lemma negb_intro : (b:bool)b=(negb (negb b)). -Proof. -NewDestruct b; Reflexivity. -Qed. - -Lemma negb_elim : (b:bool)(negb (negb b))=b. -Proof. -NewDestruct b; Reflexivity. -Qed. - -Lemma negb_orb : (b1,b2:bool) - (negb (orb b1 b2)) = (andb (negb b1) (negb b2)). -Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. -Qed. - -Lemma negb_andb : (b1,b2:bool) - (negb (andb b1 b2)) = (orb (negb b1) (negb b2)). -Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. -Qed. - -Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')). -Proof. -NewDestruct b; NewDestruct b'; Intros; Simpl; Trivial with bool. -Qed. - -Lemma no_fixpoint_negb : (b:bool)~(negb b)=b. -Proof. -NewDestruct b; Simpl; Intro; Apply diff_true_false; Auto with bool. -Qed. - -Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false. -NewDestruct b. -Trivial with bool. -Trivial with bool. -Qed. - -Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false. -NewDestruct b. -Trivial with bool. -Trivial with bool. -Qed. - - -Lemma if_negb : (A:Set) (b:bool) (x,y:A) (if (negb b) then x else y)=(if b then y else x). -Proof. - NewDestruct b;Trivial. -Qed. - - -(****************************) -(** A few lemmas about [or] *) -(****************************) - -Lemma orb_prop : - (a,b:bool)(orb a b)=true -> (a = true)\/(b = true). -NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool. -Qed. - -Lemma orb_prop2 : - (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b). -NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool. -Qed. - -Lemma orb_true_intro - : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true. -NewDestruct b1; Auto with bool. -NewDestruct 1; Intros. -Elim diff_true_false; Auto with bool. -Rewrite H; Trivial with bool. -Qed. -Hints Resolve orb_true_intro : bool v62. - -Lemma orb_b_true : (b:bool)(orb b true)=true. -Auto with bool. -Qed. -Hints Resolve orb_b_true : bool v62. - -Lemma orb_true_b : (b:bool)(orb true b)=true. -Trivial with bool. -Qed. - -Definition orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}. -NewDestruct b1; Simpl; Auto with bool. -Defined. - -Lemma orb_false_intro - : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false. -Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool. -Qed. -Hints Resolve orb_false_intro : bool v62. - -Lemma orb_b_false : (b:bool)(orb b false)=b. -Proof. - NewDestruct b; Trivial with bool. -Qed. -Hints Resolve orb_b_false : bool v62. - -Lemma orb_false_b : (b:bool)(orb false b)=b. -Proof. - NewDestruct b; Trivial with bool. -Qed. -Hints Resolve orb_false_b : bool v62. - -Lemma orb_false_elim : - (b1,b2:bool)(orb b1 b2)=false -> (b1=false)/\(b2=false). -Proof. - NewDestruct b1. - Intros; Elim diff_true_false; Auto with bool. - NewDestruct b2. - Intros; Elim diff_true_false; Auto with bool. - Auto with bool. -Qed. - -Lemma orb_neg_b : - (b:bool)(orb b (negb b))=true. -Proof. - NewDestruct b; Reflexivity. -Qed. -Hints Resolve orb_neg_b : bool v62. - -Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1). -NewDestruct b1; NewDestruct b2; Reflexivity. -Qed. - -Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3). -Proof. - NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Qed. - -Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62. - -(*****************************) -(** A few lemmas about [and] *) -(*****************************) - -Lemma andb_prop : - (a,b:bool)(andb a b) = true -> (a = true)/\(b = true). - -Proof. - NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); - Auto with bool. -Qed. -Hints Resolve andb_prop : bool v62. - -Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b. -Proof. - NewDestruct a; NewDestruct b; Auto. -Defined. - -Lemma andb_prop2 : - (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b). -Proof. - NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); - Auto with bool. -Qed. -Hints Resolve andb_prop2 : bool v62. - -Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true. -Proof. - NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. -Qed. -Hints Resolve andb_true_intro : bool v62. - -Lemma andb_true_intro2 : - (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)). -Proof. - NewDestruct b1; NewDestruct b2; Simpl; Tauto. -Qed. -Hints Resolve andb_true_intro2 : bool v62. - -Lemma andb_false_intro1 - : (b1,b2:bool)(b1=false)->(andb b1 b2)=false. -NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. -Qed. - -Lemma andb_false_intro2 - : (b1,b2:bool)(b2=false)->(andb b1 b2)=false. -NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. -Qed. - -Lemma andb_b_false : (b:bool)(andb b false)=false. -NewDestruct b; Auto with bool. -Qed. - -Lemma andb_false_b : (b:bool)(andb false b)=false. -Trivial with bool. -Qed. - -Lemma andb_b_true : (b:bool)(andb b true)=b. -NewDestruct b; Auto with bool. -Qed. - -Lemma andb_true_b : (b:bool)(andb true b)=b. -Trivial with bool. -Qed. - -Definition andb_false_elim : - (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}. -NewDestruct b1; Simpl; Auto with bool. -Defined. -Hints Resolve andb_false_elim : bool v62. - -Lemma andb_neg_b : - (b:bool)(andb b (negb b))=false. -NewDestruct b; Reflexivity. -Qed. -Hints Resolve andb_neg_b : bool v62. - -Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1). -NewDestruct b1; NewDestruct b2; Reflexivity. -Qed. - -Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Qed. - -Hints Resolve andb_sym andb_assoc : bool v62. - -(*******************************) -(** Properties of [xorb] *) -(*******************************) - -Lemma xorb_false : (b:bool) (xorb b false)=b. -Proof. - NewDestruct b; Trivial. -Qed. - -Lemma false_xorb : (b:bool) (xorb false b)=b. -Proof. - NewDestruct b; Trivial. -Qed. - -Lemma xorb_true : (b:bool) (xorb b true)=(negb b). -Proof. - Trivial. -Qed. - -Lemma true_xorb : (b:bool) (xorb true b)=(negb b). -Proof. - NewDestruct b; Trivial. -Qed. - -Lemma xorb_nilpotent : (b:bool) (xorb b b)=false. -Proof. - NewDestruct b; Trivial. -Qed. - -Lemma xorb_comm : (b,b':bool) (xorb b b')=(xorb b' b). -Proof. - NewDestruct b; NewDestruct b'; Trivial. -Qed. - -Lemma xorb_assoc : (b,b',b'':bool) (xorb (xorb b b') b'')=(xorb b (xorb b' b'')). -Proof. - NewDestruct b; NewDestruct b'; NewDestruct b''; Trivial. -Qed. - -Lemma xorb_eq : (b,b':bool) (xorb b b')=false -> b=b'. -Proof. - NewDestruct b; NewDestruct b'; Trivial. - Unfold xorb. Intros. Rewrite H. Reflexivity. -Qed. - -Lemma xorb_move_l_r_1 : (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 : (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 : (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 : (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. - -(*******************************) -(** De Morgan's law *) -(*******************************) - -Lemma demorgan1 : (b1,b2,b3:bool) - (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Qed. - -Lemma demorgan2 : (b1,b2,b3:bool) - (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Qed. - -Lemma demorgan3 : (b1,b2,b3:bool) - (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Qed. - -Lemma demorgan4 : (b1,b2,b3:bool) - (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Qed. - -Lemma absoption_andb : (b1,b2:bool) - (andb b1 (orb b1 b2)) = b1. -Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. -Qed. - -Lemma absoption_orb : (b1,b2:bool) - (orb b1 (andb b1 b2)) = b1. -Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. -Qed. - - -(** Misc. equalities between booleans (to be used by Auto) *) - -Lemma bool_1 : (b1,b2:bool)(b1=true <-> b2=true) -> b1=b2. -Proof. - Intros b1 b2; Case b1; Case b2; Intuition. -Qed. - -Lemma bool_2 : (b1,b2:bool)b1=b2 -> b1=true -> b2=true. -Proof. - Intros b1 b2; Case b1; Case b2; Intuition. -Qed. - -Lemma bool_3 : (b:bool) ~(negb b)=true -> b=true. -Proof. - NewDestruct b; Intuition. -Qed. - -Lemma bool_4 : (b:bool) b=true -> ~(negb b)=true. -Proof. - NewDestruct b; Intuition. -Qed. - -Lemma bool_5 : (b:bool) (negb b)=true -> ~b=true. -Proof. - NewDestruct b; Intuition. -Qed. - -Lemma bool_6 : (b:bool) ~b=true -> (negb b)=true. -Proof. - NewDestruct b; Intuition. -Qed. - -Hints Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6. diff --git a/theories7/Bool/BoolEq.v b/theories7/Bool/BoolEq.v deleted file mode 100644 index b670dbdd..00000000 --- a/theories7/Bool/BoolEq.v +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: BoolEq.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) -(* Cuihtlauac Alvarado - octobre 2000 *) - -(** Properties of a boolean equality *) - - -Require Export Bool. - -Section Bool_eq_dec. - - Variable A : Set. - - Variable beq : A -> A -> bool. - - Variable beq_refl : (x:A)true=(beq x x). - - Variable beq_eq : (x,y:A)true=(beq x y)->x=y. - - Definition beq_eq_true : (x,y:A)x=y->true=(beq x y). - Proof. - Intros x y H. - Case H. - Apply beq_refl. - Defined. - - Definition beq_eq_not_false : (x,y:A)x=y->~false=(beq x y). - Proof. - Intros x y e. - Rewrite <- beq_eq_true; Trivial; Discriminate. - Defined. - - Definition beq_false_not_eq : (x,y:A)false=(beq x y)->~x=y. - Proof. - Exact [x,y:A; H:(false=(beq x y)); e:(x=y)](beq_eq_not_false x y e H). - Defined. - - Definition exists_beq_eq : (x,y:A){b:bool | b=(beq x y)}. - Proof. - Intros. - Exists (beq x y). - Constructor. - Defined. - - Definition not_eq_false_beq : (x,y:A)~x=y->false=(beq x y). - Proof. - Intros x y H. - Symmetry. - Apply not_true_is_false. - Intro. - Apply H. - Apply beq_eq. - Symmetry. - Assumption. - Defined. - - Definition eq_dec : (x,y:A){x=y}+{~x=y}. - Proof. - Intros x y; Case (exists_beq_eq x y). - Intros b; Case b; Intro H. - Left; Apply beq_eq; Assumption. - Right; Apply beq_false_not_eq; Assumption. - Defined. - -End Bool_eq_dec. diff --git a/theories7/Bool/Bvector.v b/theories7/Bool/Bvector.v deleted file mode 100644 index e6545381..00000000 --- a/theories7/Bool/Bvector.v +++ /dev/null @@ -1,266 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Bvector.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) - -(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) - -Require Export Bool. -Require Export Sumbool. -Require Arith. - -V7only [Import nat_scope.]. -Open Local Scope nat_scope. - -(* -On s'inspire de PolyList pour fabriquer les vecteurs de bits. -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. -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. - -(En effet une définition comme : -Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) := -Cases v of - | Vnil => Vnil - | (Vcons a p v') => (Vcons (f a) p (Vunaire p v')) -end. -provoque ce message d'erreur : -Coq < Error: Inference of annotation not yet implemented in this case). - - - Inductive list [A : Set] : Set := - nil : (list A) | cons : A->(list A)->(list A). - head = [A:Set; l:(list A)] Cases l of - | nil => Error - | (cons x _) => (Value x) - end - : (A:Set)(list A)->(option A). - tail = [A:Set; l:(list A)]Cases l of - | nil => (nil A) - | (cons _ m) => m - end - : (A:Set)(list A)->(list A). - length = [A:Set] Fix length {length [l:(list A)] : nat := - Cases l of - | nil => O - | (cons _ m) => (S (length m)) - end} - : (A:Set)(list A)->nat. - map = [A,B:Set; f:(A->B)] Fix map {map [l:(list A)] : (list B) := - Cases l of - | nil => (nil B) - | (cons a t) => (cons (f a) (map t)) - end} - : (A,B:Set)(A->B)->(list A)->(list B) -*) - -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. -*) - -Variable A : Set. - -Inductive vector: nat -> Set := - | Vnil : (vector O) - | Vcons : (a:A) (n:nat) (vector n) -> (vector (S n)). - -Definition Vhead : (n:nat) (vector (S n)) -> A. -Proof. - Intros n v; Inversion v; Exact a. -Defined. - -Definition Vtail : (n:nat) (vector (S n)) -> (vector n). -Proof. - Intros n v; Inversion v; Exact H0. -Defined. - -Definition Vlast : (n:nat) (vector (S n)) -> A. -Proof. - NewInduction n as [|n f]; Intro v. - Inversion v. - Exact a. - - Inversion v. - Exact (f H0). -Defined. - -Definition Vconst : (a:A) (n:nat) (vector n). -Proof. - NewInduction n as [|n v]. - Exact Vnil. - - Exact (Vcons a n v). -Defined. - -Lemma Vshiftout : (n:nat) (vector (S n)) -> (vector n). -Proof. - NewInduction n as [|n f]; Intro v. - Exact Vnil. - - Inversion v. - Exact (Vcons a n (f H0)). -Defined. - -Lemma Vshiftin : (n:nat) A -> (vector n) -> (vector (S n)). -Proof. - NewInduction n as [|n f]; Intros a v. - Exact (Vcons a O v). - - Inversion v. - Exact (Vcons a (S n) (f a H0)). -Defined. - -Lemma Vshiftrepeat : (n:nat) (vector (S n)) -> (vector (S (S n))). -Proof. - NewInduction n as [|n f]; Intro v. - Inversion v. - Exact (Vcons a (1) v). - - Inversion v. - Exact (Vcons a (S (S n)) (f H0)). -Defined. - -(* -Lemma S_minus_S : (n,p:nat) (gt n (S p)) -> (S (minus n (S p)))=(minus n p). -Proof. - Intros. -Save. -*) - -Lemma Vtrunc : (n,p:nat) (gt n p) -> (vector n) -> (vector (minus n p)). -Proof. - NewInduction p as [|p f]; Intros H v. - Rewrite <- minus_n_O. - Exact v. - - Apply (Vshiftout (minus n (S p))). - -Rewrite minus_Sn_m. -Apply f. -Auto with *. -Exact v. -Auto with *. -Defined. - -Lemma Vextend : (n,p:nat) (vector n) -> (vector p) -> (vector (plus n p)). -Proof. - NewInduction n as [|n f]; Intros p v v0. - Simpl; Exact v0. - - Inversion v. - Simpl; Exact (Vcons a (plus n p) (f p H0 v0)). -Defined. - -Variable f : A -> A. - -Lemma Vunary : (n:nat)(vector n)->(vector n). -Proof. - NewInduction n as [|n g]; Intro v. - Exact Vnil. - - Inversion v. - Exact (Vcons (f a) n (g H0)). -Defined. - -Variable g : A -> A -> A. - -Lemma Vbinary : (n:nat)(vector n)->(vector n)->(vector n). -Proof. - NewInduction n as [|n h]; Intros v v0. - Exact Vnil. - - Inversion v; Inversion v0. - Exact (Vcons (g a a0) n (h H0 H2)). -Defined. - -End VECTORS. - -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. -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 -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). -*) - -Definition Bvector := (vector bool). - -Definition Bnil := (Vnil bool). - -Definition Bcons := (Vcons bool). - -Definition Bvect_true := (Vconst bool true). - -Definition Bvect_false := (Vconst bool false). - -Definition Blow := (Vhead bool). - -Definition Bhigh := (Vtail bool). - -Definition Bsign := (Vlast bool). - -Definition Bneg := (Vunary bool negb). - -Definition BVand := (Vbinary bool andb). - -Definition BVor := (Vbinary bool orb). - -Definition BVxor := (Vbinary bool xorb). - -Definition BshiftL := [n:nat; bv : (Bvector (S n)); carry:bool] - (Bcons carry n (Vshiftout bool n bv)). - -Definition BshiftRl := [n:nat; bv : (Bvector (S n)); carry:bool] - (Bhigh (S n) (Vshiftin bool (S n) carry bv)). - -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]:(Bvector (S n)) := -Cases p of - | O => bv - | (S p') => (BshiftL n (BshiftL_iter n bv p') false) -end. - -Fixpoint BshiftRl_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := -Cases p of - | O => bv - | (S p') => (BshiftRl n (BshiftRl_iter n bv p') false) -end. - -Fixpoint BshiftRa_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := -Cases p of - | O => bv - | (S p') => (BshiftRa n (BshiftRa_iter n bv p')) -end. - -End BOOLEAN_VECTORS. - diff --git a/theories7/Bool/DecBool.v b/theories7/Bool/DecBool.v deleted file mode 100755 index c22cd032..00000000 --- a/theories7/Bool/DecBool.v +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: DecBool.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) - -Set Implicit Arguments. - -Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C - := [A,B,C,H,x,y]if H then [_]x else [_]y. - - -Theorem ifdec_left : (A,B:Prop)(C:Set)(H:{A}+{B})~B->(x,y:C)(ifdec H x y)=x. -Intros; Case H; Auto. -Intro; Absurd B; Trivial. -Qed. - -Theorem ifdec_right : (A,B:Prop)(C:Set)(H:{A}+{B})~A->(x,y:C)(ifdec H x y)=y. -Intros; Case H; Auto. -Intro; Absurd A; Trivial. -Qed. - -Unset Implicit Arguments. diff --git a/theories7/Bool/IfProp.v b/theories7/Bool/IfProp.v deleted file mode 100755 index bcfa4be3..00000000 --- a/theories7/Bool/IfProp.v +++ /dev/null @@ -1,49 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: IfProp.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) - -Require Bool. - -Inductive IfProp [A,B:Prop] : bool-> Prop - := Iftrue : A -> (IfProp A B true) - | Iffalse : B -> (IfProp A B false). - -Hints Resolve Iftrue Iffalse : bool v62. - -Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Auto with bool. -Qed. - -Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Trivial with bool. -Qed. - -Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A. -Intros. -Inversion H. -Assumption. -Qed. - -Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B. -Intros. -Inversion H. -Assumption. -Qed. - -Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B. -NewDestruct 1; Auto with bool. -Qed. - -Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}. -NewDestruct b; Intro H. -Left; Inversion H; Auto with bool. -Right; Inversion H; Auto with bool. -Qed. diff --git a/theories7/Bool/Sumbool.v b/theories7/Bool/Sumbool.v deleted file mode 100644 index 8d55cbb6..00000000 --- a/theories7/Bool/Sumbool.v +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Sumbool.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ 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. - Its extraction is isomorphic to the type of booleans. *) - -(** A boolean is either [true] or [false], and this is decidable *) - -Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}. -Proof. - NewDestruct b; Auto. -Defined. - -Hints Resolve sumbool_of_bool : bool. - -Definition bool_eq_rec : (b:bool)(P:bool->Set) - ((b=true)->(P true))->((b=false)->(P false))->(P b). -NewDestruct b; Auto. -Defined. - -Definition bool_eq_ind : (b:bool)(P:bool->Prop) - ((b=true)->(P true))->((b=false)->(P false))->(P b). -NewDestruct 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. - -End connectives. - -Hints Resolve sumbool_and sumbool_or sumbool_not : core. - - -(** Any decidability function in type [sumbool] can be turned into a function - returning a boolean with the corresponding specification: *) - -Definition bool_of_sumbool : - (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 ]. -Defined. -Implicits bool_of_sumbool. diff --git a/theories7/Bool/Zerob.v b/theories7/Bool/Zerob.v deleted file mode 100755 index 24e48c28..00000000 --- a/theories7/Bool/Zerob.v +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Zerob.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) - -Require Arith. -Require Bool. - -V7only [Import nat_scope.]. -Open Local Scope nat_scope. - -Definition zerob : nat->bool - := [n:nat]Cases n of O => true | (S _) => false end. - -Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true. -NewDestruct n; [Trivial with bool | Inversion 1]. -Qed. -Hints Resolve zerob_true_intro : bool. - -Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O). -NewDestruct n; [Trivial with bool | Inversion 1]. -Qed. - -Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false. -NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool]. -Qed. -Hints Resolve zerob_false_intro : bool. - -Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O). -NewDestruct n; [Intro H; Inversion H | Auto with bool]. -Qed. |