diff options
Diffstat (limited to 'contrib/subtac/Utils.v')
-rw-r--r-- | contrib/subtac/Utils.v | 100 |
1 files changed, 45 insertions, 55 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 4a2208ce..76f49dd3 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -1,75 +1,65 @@ +Require Export Coq.subtac.SubtacTactics. + Set Implicit Arguments. -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). +(** Wrap a proposition inside a subset. *) -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. +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 _ _). -Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. -intros. -induction t. -exact x. -Defined. +(** 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. *) -Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P), - P (ex_pi1 t). -intros A P. -dependent inversion t. -simpl. -exact p. -Defined. +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 "` t" := (proj1_sig t) (at level 100) : core_scope. Notation "'forall' { x : A | P } , Q" := (forall x:{x:A|P}, Q) (at level 200, x ident, right associativity). -Lemma subset_simpl : forall (A : Set) (P : A -> Prop) - (t : sig P), P (` t). -Proof. -intros. -induction t. - simpl ; auto. -Qed. - -Ltac destruct_one_pair := - match goal with - | [H : (ex _) |- _] => destruct H - | [H : (ex2 _) |- _] => destruct H - | [H : (sig _) |- _] => destruct H - | [H : (_ /\ _) |- _] => destruct H -end. - -Ltac destruct_exists := repeat (destruct_one_pair) . - -Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto with arith. - -(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) -Ltac destruct_call f := - match goal with - | H : ?T |- _ => - match T with - context [f ?x ?y ?z] => destruct (f x y z) - | context [f ?x ?y] => destruct (f x y) - | context [f ?x] => destruct (f x) - end - | |- ?T => - match T with - context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n - | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n - | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n - end - end. +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 _ _ _). + +(** Default simplification tactic. *) + +Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; + try (solve [ red ; intros ; discriminate ]) ; auto with *. + +(** 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 => "pair" [ "" ]. -Extract Inductive sigT => "pair" [ "" ]. +(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) +(* Extract Inductive sigT => "prod" [ "" ]. *) Require Export ProofIrrelevance. +Require Export Coq.subtac.Heq. + +Delimit Scope program_scope with program. |