diff options
-rw-r--r-- | tactics/class_setoid.ml4 | 9 | ||||
-rw-r--r-- | tactics/eauto.ml4 | 11 | ||||
-rw-r--r-- | theories/Classes/Relations.v | 22 | ||||
-rw-r--r-- | theories/Program/Basics.v | 32 |
4 files changed, 55 insertions, 19 deletions
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index 5939f840f..6569afc14 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -88,9 +88,12 @@ let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morp let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl") let arrow_morphism a b = - mkLambda (Name (id_of_string "A"), a, - mkLambda (Name (id_of_string "B"), b, - mkProd (Anonymous, mkRel 2, mkRel 2))) + if isprop a && isprop b then + Lazy.force impl + else + mkLambda (Name (id_of_string "A"), a, + mkLambda (Name (id_of_string "B"), b, + mkProd (Anonymous, mkRel 2, mkRel 2))) let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index da477f2a3..effebf331 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -241,15 +241,24 @@ module SearchProblem = struct let success s = (sig_it (fst s.tacres)) = [] + let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) + + let pr_goals gls = + let evars = Evarutil.nf_evars (Refiner.project gls) in + prlist (pr_ev evars) (sig_it gls) + let filter_tactics (glls,v) l = (* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) +(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) +(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) let rec aux = function | [] -> [] | (tac,pptac) :: tacl -> try let (lgls,ptl) = apply_tac_list tac glls in let v' p = v (ptl p) in -(* msg (hov 0 (pptac ++ str"\n")); *) +(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) +(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) ((lgls,v'),pptac) :: aux tacl with e when Logic.catchable_exception e -> aux tacl diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v index 9cc78a970..c05a4b1e1 100644 --- a/theories/Classes/Relations.v +++ b/theories/Classes/Relations.v @@ -184,6 +184,12 @@ Ltac relation_refl := | [ |- ?R ?A ?B ?C ?D ?X ?X ] => apply (reflexive (R:=R A B C D) X) | [ H : ?R ?A ?B ?C ?D ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D) H) + + | [ |- ?R ?A ?B ?C ?D ?E ?X ?X ] => apply (reflexive (R:=R A B C D E) X) + | [ H : ?R ?A ?B ?C ?D ?E ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E) H) + + | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?X ] => apply (reflexive (R:=R A B C D E F) X) + | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F) H) end. Ltac refl := relation_refl. @@ -200,6 +206,9 @@ Ltac relation_sym := | [ H : ?R ?A ?B ?C ?D ?X ?Y |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y) H) + | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y) H) end. Ltac relation_symmetric := @@ -213,6 +222,10 @@ Ltac relation_symmetric := | [ |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y)) | [ |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y)) end. Ltac sym := relation_symmetric. @@ -236,6 +249,9 @@ Ltac relation_trans := | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?F ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => + apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z) H H') end. Ltac relation_transitive Y := @@ -254,6 +270,12 @@ Ltac relation_transitive Y := | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => + apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => + apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z)) end. Ltac trans Y := relation_transitive Y. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 014ff3a01..3040dd04b 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -9,7 +8,7 @@ (* Standard functions and proofs about them. * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud * 91405 Orsay, France *) (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) @@ -19,28 +18,26 @@ Unset Strict Implicit. Require Export Coq.Program.FunctionalExtensionality. -Definition compose `A B C` (g : B -> C) (f : A -> B) := fun x : A => g (f x). +Notation "'λ' x : T , y" := (fun x:T => y) (at level 1, x,T,y at level 10) : program_scope. -Definition arrow (A B : Type) := A -> B. +Open Scope program_scope. -Definition impl (A B : Prop) : Prop := A -> B. +Definition id `A` := λ x : A, x. -Definition id `A` := fun x : A => x. +Definition compose `A B C` (g : B -> C) (f : A -> B) := λ x : A , g (f x). Hint Unfold compose. -Notation " g 'o' f " := (compose g f) (at level 50, left associativity) : program_scope. - -Open Scope program_scope. +Notation " g ∘ f " := (compose g f) (at level 50, left associativity) : program_scope. -Lemma compose_id_left : forall A B (f : A -> B), id o f = f. +Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. Proof. intros. unfold id, compose. symmetry ; apply eta_expansion. Qed. -Lemma compose_id_right : forall A B (f : A -> B), f o id = f. +Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. Proof. intros. unfold id, compose. @@ -48,13 +45,18 @@ Proof. Qed. Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), - h o (g o f) = h o g o f. + h ∘ (g ∘ f) = h ∘ g ∘ f. Proof. + intros. reflexivity. Qed. Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. +Definition arrow (A B : Type) := A -> B. + +Definition impl (A B : Prop) : Prop := A -> B. + Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing). Definition const `A B` (a : A) := fun x : B => a. @@ -126,13 +128,13 @@ Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..). (** n-ary exists ! *) -Notation "'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) +Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) (at level 200, x ident, y ident, right associativity) : type_scope. -Notation "'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))))) +Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))))) (at level 200, x ident, y ident, z ident, right associativity) : type_scope. -Notation "'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p)))))))) +Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p)))))))) (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope. Tactic Notation "exist" constr(x) := exists x. |