diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-07 18:36:25 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-07 18:36:25 +0000 |
commit | 2de683db51b44b8051ead6d89be67f0185e7e87d (patch) | |
tree | adc23d9d0d2258efafae705563142ac35196039c /theories/Program/Utils.v | |
parent | 2fded684878073f1f028ebb856a455a0dc568caf (diff) |
Move Program tactics into a proper theories/ directory as they are general purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Utils.v')
-rw-r--r-- | theories/Program/Utils.v | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v new file mode 100644 index 000000000..a87eda0a2 --- /dev/null +++ b/theories/Program/Utils.v @@ -0,0 +1,70 @@ +(************************************************************************) +(* 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$ i*) + +Require Export Coq.Program.Tactics. + +Set Implicit Arguments. + +(** Wrap a proposition inside a subset. *) + +Notation " {{ x }} " := (tt : { y : unit | x }). + +(** A simpler notation for subsets defined on a cartesian product. *) + +Notation "{ ( x , y ) : A | P }" := + (sig (fun anonymous : A => let (x,y) := anonymous in P)) + (x ident, y ident) : type_scope. + +(** Generates an obligation to prove False. *) + +Notation " ! " := (False_rect _ _). + +(** Abbreviation for first projection and hiding of proofs of subset objects. *) + +Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. +Notation "( x & ? )" := (@exist _ _ x _) : core_scope. + +(** Coerces objects to their support before comparing them. *) + +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). + +(** Quantifying over subsets. *) + +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). + +Notation "'forall' { x : A | P } , Q" := + (forall x:{x:A|P}, Q) + (at level 200, x ident, right associativity). + +Require Import Coq.Bool.Sumbool. + +(** Construct a dependent disjunction from a boolean. *) + +Notation "'dec'" := (sumbool_of_bool) (at level 0). + +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) + +Notation in_right := (@right _ _ _). +Notation in_left := (@left _ _ _). + +(** Extraction directives *) + +Extraction Inline proj1_sig. +Extract Inductive unit => "unit" [ "()" ]. +Extract Inductive bool => "bool" [ "true" "false" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. +(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) +(* Extract Inductive sigT => "prod" [ "" ]. *) + +(** The scope in which programs are typed (not their types). *) + +Delimit Scope program_scope with prg. |