diff options
-rw-r--r-- | interp/implicit_quantifiers.ml | 6 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 4 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 12 | ||||
-rw-r--r-- | theories/Classes/SetoidClass.v | 89 | ||||
-rw-r--r-- | theories/Classes/SetoidTactics.v | 28 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 13 |
6 files changed, 140 insertions, 12 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index c029550a1..4799eb7b3 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -99,7 +99,7 @@ let combine_params avoid applied needed = match app, need with [], need -> let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in - List.rev ids @ (List.map mkIdentC need'), avoid + List.rev ids @ (List.rev_map mkIdentC need'), avoid | _, (true, (id, _, _)) :: need -> let id' = next_ident_away_from id avoid in aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need @@ -130,7 +130,9 @@ let full_class_binders env l = (try let c = class_info (snd id) in let args, avoid = combine_params avoid l - (List.rev_map (fun x -> false, x) c.cl_context @ List.rev_map (fun x -> true, x) c.cl_super @ List.rev_map (fun x -> false, x) c.cl_params) + (List.rev_map (fun x -> false, x) c.cl_context @ + List.rev_map (fun x -> true, x) c.cl_super @ + List.rev_map (fun x -> false, x) c.cl_params) in (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid with Not_found -> unbound_class (Global.env ()) id) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 3b9d98652..d687fe640 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -49,3 +49,7 @@ val nf_named_context : evar_map -> named_context -> named_context val nf_rel_context : evar_map -> rel_context -> rel_context val nf_env : evar_map -> env -> env + +val ids_of_named_context_avoiding : Names.Idset.t -> + Sign.named_context -> Names.Idset.elt list * Names.Idset.t + diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b0e7cb147..306ef3a19 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -209,11 +209,9 @@ let instances r = let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) let resolve_typeclass env ev evi (evd, defined as acc) = - if evi.evar_body = Evar_empty then - try - !solve_instanciation_problem env evd ev evi - with Exit -> acc - else acc + try + !solve_instanciation_problem env evd ev evi + with Exit -> acc let resolve_one_typeclass env types = try @@ -280,7 +278,9 @@ let resolve_typeclasses ?(check=true) env sigma evd = let (evars', progress) = Evd.fold (fun ev evi acc -> - if Evd.mem tc_evars ev then resolve_typeclass env ev evi acc else acc) + if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then + resolve_typeclass env ev evi acc + else acc) (Evd.evars_of evars) (evars, false) in if not progress then evars' diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 851579e12..7963a307b 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -29,18 +29,28 @@ Require Export Coq.Relations.Relations. Class Setoid (carrier : Type) (equiv : relation carrier) := equiv_prf : equivalence carrier equiv. -(** Overloaded notation for setoid equivalence. Not to be confused with [eq] and [=]. *) +(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) Definition equiv [ Setoid A R ] : _ := R. Infix "==" := equiv (at level 70, no associativity) : type_scope. +Notation " x =!= y " := (~ x == y) (at level 70, no associativity). + Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf. Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf. Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf. +Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =!= y -> y =!= x. +Proof. + intros ; red ; intros. + apply equiv_sym in H0... + apply (H H0). +Qed. -Ltac refl := +(** Tactics to do some progress on the goal, called by the user. *) + +Ltac do_setoid_refl := match goal with | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X) | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X) @@ -49,16 +59,21 @@ Ltac refl := | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X) end. -Ltac sym := +Ltac refl := do_setoid_refl. + +Ltac do_setoid_sym := match goal with | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y)) + | [ |- not (@equiv ?A ?R ?s ?X ?Y) ] => apply (nequiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y)) | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X)) | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X)) | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X)) | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X)) end. -Ltac trans Y := +Ltac sym := do_setoid_sym. + +Ltac do_setoid_trans Y := match goal with | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z)) | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z)) @@ -67,6 +82,72 @@ Ltac trans Y := | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z)) end. +Ltac trans y := do_setoid_trans y. + +(** Tactics to immediately solve the goal without user help. *) + +Ltac setoid_refl := + match goal with + | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X) + | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X) + | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X) + | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X) + | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X) + end. + +Ltac setoid_sym := + match goal with + | [ H : ?X == ?Y |- ?Y == ?X ] => apply (equiv_sym (x:=X) (y:=Y) H) + | [ H : ?X =!= ?Y |- ?Y =!= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H) + end. + +Ltac setoid_trans := + match goal with + | [ H : ?X == ?Y, H' : ?Y == ?Z |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z) H H') + end. + +(** To immediatly solve a goal on setoid equality. *) + +Ltac setoid_tac := setoid_refl || setoid_sym || setoid_trans. + +Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =!= y -> y == z -> x =!= z. +Proof. + intros; intro. + assert(z == y) by setoid_sym. + assert(x == y) by setoid_trans. + contradiction. +Qed. + +Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =!= z -> x =!= z. +Proof. + intros; intro. + assert(y == x) by setoid_sym. + assert(y == z) by setoid_trans. + contradiction. +Qed. + +Open Scope type_scope. + +Ltac setoid_sat := + let add H t := let name := fresh H in add_hypothesis name t in + match goal with + | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add name (equiv_sym H) + | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" y x in add name (nequiv_sym H) + | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add name (equiv_trans H H') + | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" x z in add name (equiv_nequiv H H') + | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add name (nequiv_equiv H H') + end. + +Ltac setoid_saturate := repeat setoid_sat. + +Ltac setoidify_tac := + match goal with + | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H + | [ s : Setoid ?A ?R |- ?R ?x ?y ] => change R with (@equiv A R s) + end. + +Ltac setoidify := repeat setoidify_tac. + Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop := forall x y, eqa x y -> eqb (m x) (m y). diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 4832f1d72..7be514169 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -35,3 +35,31 @@ Ltac setoideq := [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y) end. +Ltac setoid_tactic := + match goal with + | [ H : ?eq ?x ?y |- ?eq ?y ?x ] => sym ; apply H + | [ |- ?eq ?x ?x ] => refl + | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ apply H | apply H' ] + | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ apply H | sym ; apply H' ] + | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ] + | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | apply H' ] + + | [ H : ?eq ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H + | [ |- @equiv _ _ _ ?x ?x ] => refl + | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ] + | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ] + | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ] + | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ] + + | [ H : @equiv ?A ?R ?s ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H + | [ |- @equiv _ _ _ ?x ?x ] => refl + | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ] + | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ] + | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ] + | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ] + + | [ H : not (@equiv ?A ?R ?s ?X ?X) |- _ ] => elim H ; refl + | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : @equiv ?A ?R ?s ?Y ?X |- _ ] => elim H ; sym ; apply H + | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : ?R ?Y ?X |- _ ] => elim H ; sym ; apply H + | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tac + end. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index b7b62f394..c3870e6bd 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -154,6 +154,19 @@ Ltac bang := Tactic Notation "contradiction" "by" constr(t) := let H := fresh in assert t as H by auto with * ; contradiction. +(** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal. + Useful to do saturation using tactics. *) + +Ltac add_hypothesis H' p := + match type of p with + ?X => + match goal with + | [ H : X |- _ ] => fail 1 + | _ => set (H':=p) ; try (change p with H') ; clearbody H' + end + end. + + (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *] is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, possibly using [program_simplify] to use standard goal-cleaning tactics. *) |