diff options
Diffstat (limited to 'contrib/correctness/ProgBool.v')
-rw-r--r-- | contrib/correctness/ProgBool.v | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v deleted file mode 100644 index 38448efc..00000000 --- a/contrib/correctness/ProgBool.v +++ /dev/null @@ -1,66 +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 *) -(************************************************************************) - -(* Certification of Imperative Programs / Jean-Christophe Filliātre *) - -(* $Id: ProgBool.v 5920 2004-07-16 20:01:26Z herbelin $ *) - -Require Import ZArith. -Require Export Bool_nat. -Require Export Sumbool. - -Definition annot_bool : - forall b:bool, {b' : bool | if b' then b = true else b = false}. -Proof. -intro b. -exists b. case b; trivial. -Qed. - - -(* Logical connectives *) - -Definition spec_and (A B C D:Prop) (b:bool) := if b then A /\ C else B \/ D. - -Definition prog_bool_and : - forall Q1 Q2:bool -> Prop, - sig Q1 -> - sig Q2 -> - {b : bool | if b then Q1 true /\ Q2 true else Q1 false \/ Q2 false}. -Proof. -intros Q1 Q2 H1 H2. -elim H1. intro b1. elim H2. intro b2. -case b1; case b2; intros. -exists true; auto. -exists false; auto. exists false; auto. exists false; auto. -Qed. - -Definition spec_or (A B C D:Prop) (b:bool) := if b then A \/ C else B /\ D. - -Definition prog_bool_or : - forall Q1 Q2:bool -> Prop, - sig Q1 -> - sig Q2 -> - {b : bool | if b then Q1 true \/ Q2 true else Q1 false /\ Q2 false}. -Proof. -intros Q1 Q2 H1 H2. -elim H1. intro b1. elim H2. intro b2. -case b1; case b2; intros. -exists true; auto. exists true; auto. exists true; auto. -exists false; auto. -Qed. - -Definition spec_not (A B:Prop) (b:bool) := if b then B else A. - -Definition prog_bool_not : - forall Q:bool -> Prop, sig Q -> {b : bool | if b then Q false else Q true}. -Proof. -intros Q H. -elim H. intro b. -case b; intro. -exists false; auto. exists true; auto. -Qed. |