diff options
| -rw-r--r-- | Makefile.common | 1 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 8 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 223 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 123 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 288 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 131 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 47 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 226 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetFacts.v | 4 | ||||
| -rw-r--r-- | theories/Lists/List.v | 4 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 2 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 2 | ||||
| -rw-r--r-- | theories/Setoids/Setoid.v | 20 | ||||
| -rw-r--r-- | toplevel/classes.ml | 5 |
17 files changed, 648 insertions, 442 deletions
diff --git a/Makefile.common b/Makefile.common index 11a7cbd0f..8421d397e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -744,6 +744,7 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories UNICODEVO:= theories/Unicode/Utf8.vo CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \ + theories/Classes/Morphisms_Prop.vo theories/Classes/Morphisms_Relations.vo \ theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \ theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/EquivDec.vo \ theories/Classes/SetoidDec.vo diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index cefdcf52b..4c542ffdd 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -257,7 +257,7 @@ Section ALMOST_RING. (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Setoid_Theory R (@eq R). - Proof. constructor;intros;subst;trivial. Qed. + Proof. constructor;red;intros;subst;trivial. Qed. Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R). Proof. constructor;intros;subst;trivial. Qed. diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 7cf642ce7..c80b37d91 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -527,7 +527,7 @@ let ring_equality (r,add,mul,opp,req) = (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) r req in - let signature = [Some (r,req);Some (r,req)],Some(r,req) in + let signature = [Some (r,req);Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in let add_m, add_m_lem = try Class_tactics.default_morphism signature add with Not_found -> @@ -540,7 +540,7 @@ let ring_equality (r,add,mul,opp,req) = match opp with | Some opp -> (let opp_m,opp_m_lem = - try Class_tactics.default_morphism ([Some(r,req)],Some(r,req)) opp + try Class_tactics.default_morphism ([Some(r,req)],Some(Lazy.lazy_from_val (r,req))) opp with Not_found -> error "ring opposite should be declared as a morphism" in let op_morph = @@ -830,7 +830,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr) "[" constr(t) "]" ] -> - [ring_lookup (fst f) lH lr t] + [ring_lookup (fst f) lH lr t] END @@ -1037,7 +1037,7 @@ let field_equality r inv req = mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) | _ -> let _setoid = setoid_of_relation (Global.env ()) r req in - let signature = [Some (r,req)],Some(r,req) in + let signature = [Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in let inv_m, inv_m_lem = try Class_tactics.default_morphism signature inv with Not_found -> diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 075077048..bbd29e665 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -130,6 +130,7 @@ type search_state = { tacres : goal list sigma * validation; pri : int; last_tactic : std_ppcmds; +(* filter : constr -> constr -> bool; *) dblist : Auto.Hint_db.t list; localdb : Auto.Hint_db.t list } @@ -148,23 +149,23 @@ module SearchProblem = struct prlist (pr_ev evars) (sig_it gls) let filter_tactics (glls,v) l = - if !debug then - (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")); +(* if !debug then *) +(* (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,pri,pptac) :: tacl -> try - if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); +(* if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *) let (lgls,ptl) = apply_tac_list tac glls in let v' p = v (ptl p) in - if !debug then - begin - let evars = Evarutil.nf_evars (Refiner.project glls) in - msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); - msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) - end; +(* if !debug then *) +(* begin *) +(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) +(* msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) +(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *) +(* end; *) ((lgls,v'),pri,pptac) :: aux tacl with e when Logic.catchable_exception e -> (* if !debug then msg (str"failed\n"); *) @@ -195,31 +196,33 @@ module SearchProblem = struct let nbgl = List.length (sig_it lg) in assert (nbgl > 0); let g = find_first_goal lg in +(* let filt = s.filter (pf_concl g) in *) let assumption_tacs = let l = filter_tactics s.tacres (List.map (fun id -> (Eauto.e_give_exact_constr (mkVar id), 0, (str "exact" ++ spc () ++ pr_id id))) - (pf_ids_of_hyps g)) +(* (List.filter (fun id -> filt (pf_get_hyp_typ g id)) *) + (pf_ids_of_hyps g)) in List.map (fun (res,pri,pp) -> { s with tacres = res; pri = 0; last_tactic = pp; localdb = List.tl s.localdb }) l in - let intro_tac = - List.map - (fun ((lgls,_) as res,pri,pp) -> - let g' = first_goal lgls in - let hintl = - make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in - let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in - { s with tacres = res; - last_tactic = pp; - pri = pri; - localdb = ldb :: List.tl s.localdb }) - (filter_tactics s.tacres [Tactics.intro,1,(str "intro")]) - in +(* let intro_tac = *) +(* List.map *) +(* (fun ((lgls,_) as res,pri,pp) -> *) +(* let g' = first_goal lgls in *) +(* let hintl = *) +(* make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') *) +(* in *) +(* let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in *) +(* { s with tacres = res; *) +(* last_tactic = pp; *) +(* pri = pri; *) +(* localdb = ldb :: List.tl s.localdb }) *) +(* (filter_tactics s.tacres [Tactics.intro,1,(str "intro")]) *) +(* in *) let possible_resolve ((lgls,_) as res, pri, pp) = let nbgl' = List.length (sig_it lgls) in if nbgl' < nbgl then @@ -232,17 +235,13 @@ module SearchProblem = struct localdb = list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb } in -(* let custom_tac = *) -(* List.map possible_resolve *) -(* (filter_tactics s.tacres [s.custom_tactic,(str "custom_tactic")]) *) -(* in *) let rec_tacs = let l = filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) in List.map possible_resolve l in - List.sort compare (assumption_tacs @ intro_tac (* @ custom_tac *) @ rec_tacs) + List.sort compare (assumption_tacs (* @intro_tac @ custom_tac *) @ rec_tacs) let pp s = msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ @@ -252,10 +251,48 @@ end module Search = Explore.Make(SearchProblem) + +let filter_pat c = + try + let morg = Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")) in + let morc = constr_of_global morg in + match kind_of_term c with + | App(morph, [| t; r; m |]) when eq_constr morph morc -> + (fun y -> + (match y.pat with + Some (PApp (PRef mor, [| t'; r'; m' |])) when mor = morg -> + (match m' with + | PRef c -> if isConst m then eq_constr (constr_of_global c) m else false + | _ -> true) + | _ -> true)) + | _ -> fun _ -> true + with _ -> fun _ -> true + +let morphism_class = + lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")))) + +let filter c = + try let morc = constr_of_global (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))) in + match kind_of_term c with + | App(morph, [| t; r; m |]) when eq_constr morph morc -> + (fun y -> + let (_, r) = decompose_prod y in + (match kind_of_term r with + App (morph', [| t'; r'; m' |]) when eq_constr morph' morc -> + (match kind_of_term m' with + | Rel n -> true + | Const c -> eq_constr m m' + | App _ -> true + | _ -> false) + | _ -> false)) + | _ -> fun _ -> true + with _ -> fun _ -> true + let make_initial_state n gls dblist localdbs = { depth = n; tacres = gls; pri = 0; +(* filter = filter; *) last_tactic = (mt ()); dblist = dblist; localdb = localdbs } @@ -422,9 +459,6 @@ END (** Typeclass-based rewriting. *) -let morphism_class = - lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")))) - let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs)) let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) @@ -499,7 +533,7 @@ let split_head = function hd :: tl -> hd, tl | [] -> assert(false) -let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a option) (f : 'a -> constr) = +let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) = let new_evar isevars env t = Evarutil.e_new_evar isevars env (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t @@ -527,7 +561,8 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a optio let t = Reductionops.nf_betaiota t in let rel = mk_relty t None in t, rel, [t, rel] - | Some (t, rel) -> t, rel, [t, rel]) + | Some codom -> let (t, rel) = Lazy.force codom in + t, rel, [t, rel]) in aux m cstrs let reflexivity_proof_evar env evars carrier relation x = @@ -554,26 +589,17 @@ let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env let transitive_proof env = find_class_proof transitive_type transitive_proof env +exception FoundInt of int + +let array_find (arr: 'a array) (pred: int -> 'a -> bool): int = + try + for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (FoundInt i) done; + raise Not_found + with FoundInt i -> i + let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars = let morph_instance, proj, sigargs, m', args, args' = -(* if is_equiv env sigma m then *) -(* let params, rest = array_chop 3 args in *) -(* let a, r, s = params.(0), params.(1), params.(2) in *) -(* let params', rest' = array_chop 3 args' in *) -(* let inst = mkApp (Lazy.force setoid_morphism, params) in *) -(* (* Equiv gives a binary morphism *) *) -(* let (cl, proj) = Lazy.force class_two in *) -(* let ctxargs = [ a; r; s; a; r; s; mkProp; Lazy.force iff; Lazy.force iff_setoid; ] in *) -(* let m' = mkApp (m, [| a; r; s |]) in *) -(* inst, proj, ctxargs, m', rest, rest' *) -(* else *) - let first = - let first = ref (-1) in - for i = 0 to Array.length args' - 1 do - if !first = -1 && args'.(i) <> None then first := i - done; - !first - in + let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in let morphargs, morphobjs = array_chop first args in let morphargs', morphobjs' = array_chop first args' in let appm = mkApp(m, morphargs) in @@ -736,9 +762,47 @@ let unfold_all t = | _ -> assert false) | _ -> assert false -type rewrite_flags = { under_lambdas : bool } +(* let lift_cstr env sigma evars args cstr = *) +(* let codom = *) +(* match cstr with *) +(* | Some c -> c *) +(* | None -> *) +(* let ty = Evarutil.e_new_evar evars env (new_Type ()) in *) +(* let rel = Evarutil.e_new_evar evars env (mk_relation ty) in *) +(* (ty, rel) *) +(* in *) +(* Array.fold_right *) +(* (fun arg (car, rel) -> *) +(* let ty = Typing.type_of env sigma arg in *) +(* let car' = mkProd (Anonymous, ty, car) in *) +(* let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in *) +(* (car', rel')) *) +(* args codom *) + +let rec decomp_pointwise n c = + if n = 0 then c + else + match kind_of_term c with + | App (pointwise, [| a; b; relb |]) -> decomp_pointwise (pred n) relb + | _ -> raise Not_found + +let lift_cstr env sigma evars args cstr = + match cstr with + | Some codom -> + let cstr () = + Array.fold_right + (fun arg (car, rel) -> + let ty = Typing.type_of env sigma arg in + let car' = mkProd (Anonymous, ty, car) in + let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in + (car', rel')) + args (Lazy.force codom) + in Some (Lazy.lazy_from_fun cstr) + | None -> None + +type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } -let default_flags = { under_lambdas = true } +let default_flags = { under_lambdas = true; on_morphisms = true; } let build_new gl env sigma flags occs hypinfo concl cstr evars = let is_occ occ = occs = [] || List.mem occ occs in @@ -763,19 +827,36 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars = | None -> match kind_of_term t with | App (m, args) -> - let args', occ = - Array.fold_left - (fun (acc, occ) arg -> let res, occ = aux env arg occ None in (res :: acc, occ)) - ([], occ) args + let rewrite_args () = + let args', occ = + Array.fold_left + (fun (acc, occ) arg -> let res, occ = aux env arg occ None in (res :: acc, occ)) + ([], occ) args + in + let res = + if List.for_all (fun x -> x = None) args' then None + else + let args' = Array.of_list (List.rev args') in + (try Some (resolve_morphism env sigma t m args args' cstr evars) + with Not_found -> None) + in res, occ in - let res = - if List.for_all (fun x -> x = None) args' then None - else - let args' = Array.of_list (List.rev args') in - (try Some (resolve_morphism env sigma t m args args' cstr evars) - with Not_found -> None) - in res, occ - + if flags.on_morphisms then + let m', occ = aux env m occ (lift_cstr env sigma evars args cstr) in + match m' with + None -> rewrite_args () (* Standard path, try rewrite on arguments *) + | Some (prf, (car, rel, c1, c2)) -> + (* We rewrote the function and get a proof of pointwise rel for the arguments. + We just apply it. *) + let nargs = Array.length args in + let decompprod c = snd (Reductionops.decomp_n_prod env (Evd.evars_of !evars) nargs c) in + let res = + try Some (mkApp (prf, args), + (decompprod car, decomp_pointwise nargs rel, mkApp(c1, args), mkApp(c2, args))) + with Not_found -> None + in res, occ + else rewrite_args () + | Prod (_, x, b) when not (dependent (mkRel 1) b) -> let x', occ = aux env x occ None in let b', occ = aux env b occ None in @@ -832,8 +913,6 @@ let resolve_typeclass_evars d p env evd onlyargs = (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None) in resolve_all_evars d p env pred evd -let cl_rewrite_tactic = lazy (Tacinterp.interp <:tactic<setoid_rewrite_tac>>) - let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl = let concl, is_hyp = match clause with @@ -848,7 +927,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g let evars = ref (Evd.create_evar_defs Evd.empty) in let env = pf_env gl in let sigma = project gl in - let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some cstr) evars in + let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars in match eq with Some (p, (_, _, oldt, newt)) -> (try @@ -1322,7 +1401,7 @@ let get_hyp gl c clause l2r = unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r -let general_rewrite_flags = { under_lambdas = false } +let general_rewrite_flags = { under_lambdas = false; on_morphisms = false } let general_s_rewrite l2r c ~new_goals gl = let meta = Evarutil.new_meta() in diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 0ec6c11f9..d7774a2d7 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,23 +35,25 @@ Instance [ Equivalence A R ] => Definition equiv [ Equivalence A R ] : relation A := R. -(** Shortcuts to make proof search possible (unification won't unfold equiv). *) +Typeclasses unfold @equiv. -Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. +(* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *) -Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. +(* Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. *) - Next Obligation. - Proof. - symmetry ; auto. - Qed. +(* Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. *) -Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. +(* Next Obligation. *) +(* Proof. *) +(* symmetry ; auto. *) +(* Qed. *) - Next Obligation. - Proof. - transitivity y ; auto. - Qed. +(* Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. *) + +(* Next Obligation. *) +(* Proof. *) +(* transitivity y ; auto. *) +(* Qed. *) (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -64,23 +66,6 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : Open Local Scope equiv_scope. -(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) - -Ltac setoid_subst H := - match type of H with - ?x === ?y => substitute H ; clear H x - end. - -Ltac setoid_subst_nofail := - match goal with - | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail - | _ => idtac - end. - -(** [subst*] will try its best at substituting every equality in the goal. *) - -Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail. - Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z. Proof with auto. intros; intro. @@ -97,6 +82,23 @@ Proof. contradiction. Qed. +(** Use the [substitute] command which substitutes an applied relation in every hypothesis. *) + +Ltac setoid_subst H := + match type of H with + ?x === ?y => substitute H ; clear H x + end. + +Ltac setoid_subst_nofail := + match goal with + | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail + | _ => idtac + end. + +(** [subst*] will try its best at substituting every equality in the goal. *) + +Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail. + Ltac equiv_simplify_one := match goal with | [ H : ?x === ?x |- _ ] => clear H @@ -117,34 +119,28 @@ Ltac equivify := repeat equivify_tac. (** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *) -Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := - respect := respect. - -(** The partial application too as it is Reflexive. *) +(* Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := *) +(* respect := respect. *) -Instance [ sa : Equivalence A ] (x : A) => - equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := - respect := respect. +(* (** The partial application too as it is Reflexive. *) *) -Definition type_eq : relation Type := - fun x y => x = y. +(* Instance [ sa : Equivalence A ] (x : A) => *) +(* equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := *) +(* respect := respect. *) -Program Instance type_equivalence : Equivalence Type type_eq. +(** Instance not exported by default, as comparing types for equivalence may be unintentional. *) - Solve Obligations using constructor ; unfold type_eq ; program_simpl. +Section Type_Equivalence. -Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. - -Ltac obligations_tactic ::= morphism_tac. - -(** These are morphisms used to rewrite at the top level of a proof, - using [iff_impl_id_morphism] if the proof is in [Prop] and - [eq_arrow_id_morphism] if it is in Type. *) - -Program Instance iff_impl_id_morphism : - Morphism (iff ++> impl) id. + Definition type_eq : relation Type := + fun x y => x = y. + + Program Instance type_equivalence : Equivalence Type type_eq. + + Next Obligation. + Proof. unfold type_eq in *. subst. reflexivity. Qed. -(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *) +End Type_Equivalence. (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *) @@ -152,11 +148,32 @@ Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) := pequiv_prf :> PER carrier pequiv. Definition pequiv [ PartialEquivalence A R ] : relation A := R. +Typeclasses unfold @pequiv. (** Overloaded notation for partial equiv equivalence. *) Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope. -(** Reset the default Program tactic. *) +Section Respecting. + + (** Here we build an equivalence instance for functions which relates respectful ones only, + we do not export it. *) + + Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := + { morph : A -> B | respectful R R' morph morph }. + + Program Instance [ Equivalence A R, Equivalence B R' ] => + respecting_equiv : Equivalence respecting + (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). + + Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl. + + Next Obligation. + Proof. + unfold respecting in *. program_simpl. red in H2,H3,H4. + transitivity (y x0) ; auto. + transitivity (y y0) ; auto. + symmetry. auto. + Qed. -Ltac obligations_tactic ::= program_simpl. +End Respecting.
\ No newline at end of file diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index d10cb9724..7cabc836d 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) +(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based morphisms with standard instances for equivalence relations. +(* Typeclass-based morphism definition and standard, minimal instances. Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud @@ -26,7 +26,7 @@ Unset Strict Implicit. (** * Morphisms. We now turn to the definition of [Morphism] and declare standard instances. - These will be used by the [clrewrite] tactic later. *) + These will be used by the [setoid_rewrite] tactic later. *) (** Respectful morphisms. *) @@ -71,49 +71,6 @@ Class Morphism A (R : relation A) (m : A) : Prop := Arguments Scope Morphism [type_scope signature_scope]. -(** Here we build an equivalence instance for functions which relates respectful ones only. *) - -Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := - { morph : A -> B | respectful R R' morph morph }. - -Ltac obligations_tactic ::= program_simpl. - -Program Instance [ Equivalence A R, Equivalence B R' ] => - respecting_equiv : Equivalence respecting - (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). - - Next Obligation. - Proof. - red ; intros. - destruct x ; simpl. - apply r ; auto. - Qed. - - Next Obligation. - Proof. - red ; intros. - symmetry ; apply H. - symmetry ; auto. - Qed. - - Next Obligation. - Proof. - red ; intros. - transitivity (proj1_sig y y0). - apply H ; auto. - apply H0. reflexivity. - Qed. - -(** Can't use the definition [notT] as it gives a universe inconsistency. *) - -Ltac obligations_tactic ::= program_simpl ; simpl_relation. - -Program Instance not_impl_morphism : - Morphism (Prop -> Prop) (impl --> impl) not. - -Program Instance not_iff_morphism : - Morphism (Prop -> Prop) (iff ++> iff) not. - (** We make the type implicit, it can be infered from the relations. *) Implicit Arguments Morphism [A]. @@ -139,41 +96,41 @@ Proof. firstorder. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism [ subrelation A R₁ R₂, ! Morphism R₁ m ] : Morphism R₂ m. +Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m. Proof. - intros. apply* H. apply H0. + intros. apply sub. apply mor. Qed. Instance morphism_subrelation_morphism : Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A). Proof. reduce. subst. firstorder. Qed. -Inductive done : nat -> Type := - did : forall n : nat, done n. +(** We use an external tactic to manage the application of subrelation, which is otherwise + always applicable. We allow its use only once per branch. *) + +Inductive subrelation_done : Prop := + did_subrelation : subrelation_done. Ltac subrelation_tac := match goal with - | [ H : done 1 |- @Morphism _ _ _ ] => fail + | [ H : subrelation_done |- _ ] => fail | [ |- @Morphism _ _ _ ] => let H := fresh "H" in - set(H:=did 1) ; eapply @subrelation_morphism + set(H:=did_subrelation) ; eapply @subrelation_morphism end. -(* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *) - Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. -(** Logical implication [impl] is a morphism for logical equivalence. *) +(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) -Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl. +Instance iff_impl_subrelation : subrelation iff impl. +Proof. firstorder. Qed. -(* Typeclasses eauto := debug. *) +Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). +Proof. firstorder. Qed. -Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m. - - Next Obligation. - Proof. - split ; apply respect ; [ auto | symmetry ] ; auto. - Qed. +Instance [ subrelation A R R' ] => pointwise_subrelation : + subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. +Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed. (** The complement of a relation conserves its morphisms. *) @@ -183,28 +140,26 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] => Next Obligation. Proof. unfold complement. - pose (respect). - pose (r x y H). - pose (r0 x0 y0 H0). + pose (mR x y H x0 y0 H0). intuition. Qed. (** The inverse too. *) -Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => +Program Instance [ mor : Morphism (A -> _) (RA ==> RA ==> iff) R ] => inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R). Next Obligation. Proof. - apply respect ; auto. + apply mor ; auto. Qed. -Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => +Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. - apply respect ; auto. + apply mor ; auto. Qed. (** Every Transitive relation gives rise to a binary morphism on [impl], @@ -229,18 +184,6 @@ Program Instance [ Transitive A R ] => apply* trans_contra_co_morphism ; eauto. eauto. Qed. -(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *) -(* trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* trans y... *) -(* sym... *) -(* trans y0... *) -(* sym... *) -(* Qed. *) - - (** Morphism declarations for partial applications. *) Program Instance [ Transitive A R ] (x : A) => @@ -286,18 +229,6 @@ Program Instance [ Equivalence A R ] (x : A) => symmetry... Qed. -(** With Symmetric relations, variance is no issue ! *) - -(* Program Instance (A B : Type) (R : relation A) (R' : relation B) *) -(* [ Morphism _ (R ==> R') m ] [ Symmetric A R ] => *) -(* sym_contra_morphism : Morphism (R --> R') m. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* repeat (red ; intros). apply respect. *) -(* sym... *) -(* Qed. *) - (** [R] is Reflexive, hence we can build the needed proof. *) Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) => @@ -360,57 +291,9 @@ Program Instance iff_impl_id : Program Instance inverse_iff_impl_id : Morphism (iff --> impl) id. -(** Standard instances for [iff] and [impl]. *) - -(** Logical conjunction. *) - -Program Instance and_impl_iff_morphism : - Morphism (impl ==> iff ==> impl) and. - -Program Instance and_iff_impl_morphism : - Morphism (iff ==> impl ==> impl) and. - -Program Instance and_inverse_impl_iff_morphism : - Morphism (inverse impl ==> iff ==> inverse impl) and. - -Program Instance and_iff_inverse_impl_morphism : - Morphism (iff ==> inverse impl ==> inverse impl) and. - -Program Instance and_iff_morphism : - Morphism (iff ==> iff ==> iff) and. - -(** Logical disjunction. *) - -Program Instance or_impl_iff_morphism : - Morphism (impl ==> iff ==> impl) or. - -Program Instance or_iff_impl_morphism : - Morphism (iff ==> impl ==> impl) or. - -Program Instance or_inverse_impl_iff_morphism : - Morphism (inverse impl ==> iff ==> inverse impl) or. - -Program Instance or_iff_inverse_impl_morphism : - Morphism (iff ==> inverse impl ==> inverse impl) or. - -Program Instance or_iff_morphism : - Morphism (iff ==> iff ==> iff) or. - (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) -(* Instance {A B : Type} (m : A -> B) => *) -(* any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. *) -(* Proof. *) -(* red ; intros. subst ; reflexivity. *) -(* Qed. *) - -(* Instance {A : Type} (m : A -> Prop) => *) -(* any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. *) -(* Proof. *) -(* red ; intros. subst ; split; trivial. *) -(* Qed. *) - Instance (A : Type) [ Reflexive B R ] (m : A -> B) => eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. Proof. simpl_relation. Qed. @@ -419,18 +302,13 @@ Instance (A : Type) [ Reflexive B R' ] => Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. -Instance [ Morphism (A -> B) (inverse R ==> R') m ] => - Morphism (R ==> inverse R') m | 10. -Proof. firstorder. Qed. - (** [respectful] is a morphism for relation equivalence. *) Instance respectful_morphism : Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - do 2 red ; intros. - unfold respectful, relation_equivalence in *. - red ; intros. + reduce. + unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. split ; intros. rewrite <- H0. @@ -452,21 +330,18 @@ Proof. split ; intros ; intuition. Qed. + Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop := normalizes : R m m'. Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) => - Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) . -Proof. - reduce. - symmetry ; apply inverse_respectful. -Qed. + Normalizes subrelation (inverse R ==> inverse R') (inverse (R ==> R')) . +Proof. simpl_relation. Qed. Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] => ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) . -Proof. - red. - pose normalizes. +Proof. red ; intros. + pose normalizes as r. setoid_rewrite r. setoid_rewrite inverse_respectful. reflexivity. @@ -479,23 +354,23 @@ Program Instance [ Morphism A R m ] => Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A). Proof. - simpl_relation. - unfold relation_equivalence in H. + simpl_relation. + reduce in H. split ; red ; intros. setoid_rewrite <- H. - apply respect. + apply H0. setoid_rewrite H. - apply respect. + apply H0. Qed. - + Lemma morphism_releq_morphism [ Normalizes (relation A) relation_equivalence R R', Morphism _ R' m ] : Morphism R m. Proof. intros. - pose respect. - assert(n:=normalizes). - setoid_rewrite n. + pose respect as r. + pose normalizes as norm. + setoid_rewrite norm. assumption. Qed. @@ -510,86 +385,3 @@ Ltac morphism_normalization := Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances. -(** Morphisms for relations *) - -Instance [ PartialOrder A eqA R ] => - partial_order_morphism : Morphism (eqA ==> eqA ==> iff) R. -Proof with auto. - intros. rewrite partial_order_equivalence. - simpl_relation. firstorder. - transitivity x... transitivity x0... - transitivity y... transitivity y0... -Qed. - -Instance Morphism (relation_equivalence (A:=A) ==> - relation_equivalence ==> relation_equivalence) relation_conjunction. - Proof. firstorder. Qed. - -Instance Morphism (relation_equivalence (A:=A) ==> - relation_equivalence ==> relation_equivalence) relation_disjunction. - Proof. firstorder. Qed. - - -(** Morphisms for quantifiers *) - -Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). - - Next Obligation. - Proof. - unfold pointwise_relation in H. - split ; intros. - destruct H0 as [x₁ H₁]. - exists x₁. rewrite H in H₁. assumption. - - destruct H0 as [x₁ H₁]. - exists x₁. rewrite H. assumption. - Qed. - -Program Instance {A : Type} => ex_impl_morphism : - Morphism (pointwise_relation impl ==> impl) (@ex A). - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance {A : Type} => ex_inverse_impl_morphism : - Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance {A : Type} => all_iff_morphism : - Morphism (pointwise_relation iff ==> iff) (@all A). - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Program Instance {A : Type} => all_impl_morphism : - Morphism (pointwise_relation impl ==> impl) (@all A). - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Program Instance {A : Type} => all_inverse_impl_morphism : - Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Lemma inverse_pointwise_relation A (R : relation A) : - relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). -Proof. reflexivity. Qed. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v new file mode 100644 index 000000000..d22ab06cb --- /dev/null +++ b/theories/Classes/Morphisms_Prop.v @@ -0,0 +1,131 @@ +(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Morphism instances for propositional connectives. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +Require Import Coq.Classes.Morphisms. +Require Import Coq.Program.Program. + +(** Standard instances for [not], [iff] and [impl]. *) + +(** Logical negation. *) + +Program Instance not_impl_morphism : + Morphism (impl --> impl) not. + +Program Instance not_iff_morphism : + Morphism (iff ++> iff) not. + +(** Logical conjunction. *) + +Program Instance and_impl_iff_morphism : + Morphism (impl ==> impl ==> impl) and. + +(* Program Instance and_impl_iff_morphism : *) +(* Morphism (impl ==> iff ==> impl) and. *) + +(* Program Instance and_iff_impl_morphism : *) +(* Morphism (iff ==> impl ==> impl) and. *) + +(* Program Instance and_inverse_impl_iff_morphism : *) +(* Morphism (inverse impl ==> iff ==> inverse impl) and. *) + +(* Program Instance and_iff_inverse_impl_morphism : *) +(* Morphism (iff ==> inverse impl ==> inverse impl) and. *) + +Program Instance and_iff_morphism : + Morphism (iff ==> iff ==> iff) and. + +(** Logical disjunction. *) + +Program Instance or_impl_iff_morphism : + Morphism (impl ==> impl ==> impl) or. + +(* Program Instance or_impl_iff_morphism : *) +(* Morphism (impl ==> iff ==> impl) or. *) + +(* Program Instance or_iff_impl_morphism : *) +(* Morphism (iff ==> impl ==> impl) or. *) + +(* Program Instance or_inverse_impl_iff_morphism : *) +(* Morphism (inverse impl ==> iff ==> inverse impl) or. *) + +(* Program Instance or_iff_inverse_impl_morphism : *) +(* Morphism (iff ==> inverse impl ==> inverse impl) or. *) + +Program Instance or_iff_morphism : + Morphism (iff ==> iff ==> iff) or. + +(** Logical implication [impl] is a morphism for logical equivalence. *) + +Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl. + +(** Morphisms for quantifiers *) + +Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). + + Next Obligation. + Proof. + unfold pointwise_relation in H. + split ; intros. + destruct H0 as [x₁ H₁]. + exists x₁. rewrite H in H₁. assumption. + + destruct H0 as [x₁ H₁]. + exists x₁. rewrite H. assumption. + Qed. + +Program Instance {A : Type} => ex_impl_morphism : + Morphism (pointwise_relation impl ==> impl) (@ex A). + + Next Obligation. + Proof. + unfold pointwise_relation in H. + exists H0. apply H. assumption. + Qed. + +Program Instance {A : Type} => ex_inverse_impl_morphism : + Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). + + Next Obligation. + Proof. + unfold pointwise_relation in H. + exists H0. apply H. assumption. + Qed. + +Program Instance {A : Type} => all_iff_morphism : + Morphism (pointwise_relation iff ==> iff) (@all A). + + Next Obligation. + Proof. + unfold pointwise_relation, all in *. + intuition ; specialize (H x0) ; intuition. + Qed. + +Program Instance {A : Type} => all_impl_morphism : + Morphism (pointwise_relation impl ==> impl) (@all A). + + Next Obligation. + Proof. + unfold pointwise_relation, all in *. + intuition ; specialize (H x0) ; intuition. + Qed. + +Program Instance {A : Type} => all_inverse_impl_morphism : + Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). + + Next Obligation. + Proof. + unfold pointwise_relation, all in *. + intuition ; specialize (H x0) ; intuition. + Qed. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v new file mode 100644 index 000000000..284810e94 --- /dev/null +++ b/theories/Classes/Morphisms_Relations.v @@ -0,0 +1,47 @@ +(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Morphism instances for relations. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +(** Morphisms for relations *) + +Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==> + relation_equivalence ==> relation_equivalence) relation_conjunction. + Proof. firstorder. Qed. + +Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==> + relation_equivalence ==> relation_equivalence) relation_disjunction. + Proof. firstorder. Qed. + +(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *) + +Require Import List. + +Lemma predicate_equivalence_pointwise (l : list Type) : + Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id. +Proof. do 2 red. unfold predicate_equivalence. auto. Qed. + +Lemma predicate_implication_pointwise (l : list Type) : + Morphism (@predicate_implication l ==> lift_pointwise l impl) id. +Proof. do 2 red. unfold predicate_implication. auto. Qed. + +(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *) +(* when [R] and [R'] are in [relation_equivalence]. *) + +Instance relation_equivalence_pointwise : + Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id. +Proof. apply (predicate_equivalence_pointwise (l:=(cons A (cons A nil)))). Qed. + +Instance subrelation_pointwise : + Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id. +Proof. apply (predicate_implication_pointwise (l:=(cons A (cons A nil)))). Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index f5d3cc1c4..8dfb662b2 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -21,9 +21,6 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Export Coq.Relations.Relation_Definitions. -Set Implicit Arguments. -Unset Strict Implicit. - (** Default relation on a given support. *) Class DefaultRelation A (R : relation A). @@ -50,6 +47,9 @@ Proof. reflexivity. Qed. (** We rebind relations in separate classes to be able to overload each proof. *) +Set Implicit Arguments. +Unset Strict Implicit. + Class Reflexive A (R : relation A) := reflexivity : forall x, R x x. @@ -73,6 +73,8 @@ Implicit Arguments Transitive [A]. Hint Resolve @irreflexivity : ord. +Unset Implicit Arguments. + (** We can already dualize all these properties. *) Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) := @@ -115,12 +117,20 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symm (** * Standard instances. *) +Ltac reduce_hyp H := + match type of H with + | context [ _ <-> _ ] => fail 1 + | _ => red in H ; try reduce_hyp H + end. + Ltac reduce_goal := match goal with | [ |- _ <-> _ ] => fail 1 | _ => red ; intros ; try reduce_goal end. +Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid. + Ltac reduce := reduce_goal. Tactic Notation "apply" "*" constr(t) := @@ -203,52 +213,187 @@ Program Instance eq_equivalence : Equivalence A (@eq A) | 10. Program Instance iff_equivalence : Equivalence Prop iff. -(** The following is not definable. *) -(* -Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid : - Equivalence (a -> b) - (fun f g => forall (x y : a), R x y -> R' (f x) (g y)). -*) +(** We now develop a generalization of results on relations for arbitrary predicates. + The resulting theory can be applied to homogeneous binary relations but also to + arbitrary n-ary predicates. *) +Require Import List. -(** We define the various operations which define the algebra on relations. - They are essentially liftings of the logical operations. *) +(* Notation " [ ] " := nil : list_scope. *) +(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) -Definition relation_equivalence {A : Type} : relation (relation A) := - fun (R R' : relation A) => forall x y, R x y <-> R' x y. +(* Open Local Scope list_scope. *) -Class subrelation {A:Type} (R R' : relation A) := - is_subrelation : forall x y, R x y -> R' x y. +(** A compact representation of non-dependent arities, with the codomain singled-out. *) -Implicit Arguments subrelation [[A]]. +Fixpoint arrows (l : list Type) (r : Type) : Type := + match l with + | nil => r + | A :: l' => A -> arrows l' r + end. +(** We can define abbreviations for operation and relation types based on [arrows]. *) -Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := - fun x y => R x y /\ R' x y. +Definition unary_operation A := arrows (cons A nil) A. +Definition binary_operation A := arrows (cons A (cons A nil)) A. +Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A. -Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := - fun x y => R x y \/ R' x y. +(** We define n-ary [predicate]s as functions into [Prop]. *) -(* Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. *) -(* Infix "-R>" := subrelation (at level 70) : relation_scope. *) -(* Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. *) -(* Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. *) +Definition predicate (l : list Type) := arrows l Prop. -(* Open Local Scope relation_scope. *) +(** Unary predicates, or sets. *) -(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) +Definition unary_predicate A := predicate (cons A nil). -Program Instance relation_equivalence_equivalence : - Equivalence (relation A) relation_equivalence. +(** Homogenous binary relations, equivalent to [relation A]. *) + +Definition binary_relation A := predicate (cons A (cons A nil)). + +(** We can close a predicate by universal or existential quantification. *) + +Fixpoint predicate_all (l : list Type) : predicate l -> Prop := + match l with + | nil => fun f => f + | A :: tl => fun f => forall x : A, predicate_all tl (f x) + end. + +Fixpoint predicate_exists (l : list Type) : predicate l -> Prop := + match l with + | nil => fun f => f + | A :: tl => fun f => exists x : A, predicate_exists tl (f x) + end. + +(** Pointwise extension of a binary operation on [T] to a binary operation + on functions whose codomain is [T]. *) + +Fixpoint pointwise_extension {l : list Type} {T : Type} + (op : binary_operation T) : binary_operation (arrows l T) := + match l with + | nil => fun R R' => op R R' + | A :: tl => fun R R' => + fun x => pointwise_extension op (R x) (R' x) + end. + +(** For an operator on [Prop] this lifts the operator to a binary operation. *) + +Definition pointwise_relation_extension (l : list Type) (op : binary_relation Prop) : + binary_operation (predicate l) := pointwise_extension op. + +(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *) + +Fixpoint lift_pointwise (l : list Type) (op : binary_relation Prop) : binary_relation (predicate l) := + match l with + | nil => fun R R' => op R R' + | A :: tl => fun R R' => + forall x, lift_pointwise tl op (R x) (R' x) + end. + +(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *) + +Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) := + lift_pointwise l iff. + +(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *) + +Definition predicate_implication {l : list Type} := + lift_pointwise l impl. + +(** Notations for pointwise equivalence and implication of predicates. *) + +Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. +Infix "-∙>" := predicate_implication (at level 70) : predicate_scope. + +Open Local Scope predicate_scope. + +(** The pointwise liftings of conjunction and disjunctions. + Note that these are [binary_operation]s, building new relations out of old ones. *) + +Definition predicate_intersection {l : list Type} : binary_operation (predicate l) := + pointwise_relation_extension l and. + +Definition predicate_union {l : list Type} : binary_operation (predicate l) := + pointwise_relation_extension l or. + +Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope. +Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope. + +(** The always [True] and always [False] predicates. *) + +Fixpoint true_predicate {l : list Type} : predicate l := + match l with + | nil => True + | A :: tl => fun _ => @true_predicate tl + end. + +Fixpoint false_predicate {l : list Type} : predicate l := + match l with + | nil => False + | A :: tl => fun _ => @false_predicate tl + end. + +Notation "∙⊤∙" := true_predicate : predicate_scope. +Notation "∙⊥∙" := false_predicate : predicate_scope. + +(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) + +Program Instance predicate_equivalence_equivalence : + Equivalence (predicate l) predicate_equivalence. Next Obligation. - Proof. - unfold relation_equivalence in *. - apply transitivity with (y x0 y0) ; [ apply H | apply H0 ]. + induction l ; firstorder. + Qed. + + Next Obligation. + induction l ; firstorder. + Qed. + + Next Obligation. + fold lift_pointwise. + induction l. firstorder. + intros. simpl in *. intro. pose (IHl (x x0) (y x0) (z x0)). + firstorder. + Qed. + +Program Instance predicate_implication_preorder : + PreOrder (predicate l) predicate_implication. + + Next Obligation. + induction l ; firstorder. Qed. -Program Instance subrelation_preorder : - PreOrder (relation A) subrelation. + Next Obligation. + fold lift_pointwise. + induction l. firstorder. + unfold predicate_implication in *. simpl in *. + intro. pose (IHl (x x0) (y x0) (z x0)). firstorder. + Qed. + +(** We define the various operations which define the algebra on binary relations, + from the general ones. *) + +Definition relation_equivalence {A : Type} : relation (relation A) := + @predicate_equivalence (cons _ (cons _ nil)). + +Class subrelation {A:Type} (R R' : relation A) : Prop := + is_subrelation : @predicate_implication (cons A (cons A nil)) R R'. + +Implicit Arguments subrelation [[A]]. + +Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := + @predicate_intersection (cons A (cons A nil)) R R'. + +Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := + @predicate_union (cons A (cons A nil)) R R'. + +(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + +Instance (A : Type) => relation_equivalence_equivalence : + Equivalence (relation A) relation_equivalence. +Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. + +Instance relation_implication_preorder : PreOrder (relation A) subrelation. +Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. (** *** Partial Order. A partial order is a preorder which is additionally antisymmetric. @@ -256,8 +401,7 @@ Program Instance subrelation_preorder : on the carrier. *) Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := - partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)). - + partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). (** The equivalence proof is sufficient for proving that [R] must be a morphism for equivalence (see Morphisms). @@ -265,8 +409,8 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := Instance [ PartialOrder A eqA R ] => partial_order_antisym : ! Antisymmetric A eqA R. Proof with auto. - reduce_goal. pose partial_order_equivalence. red in r. - apply <- r. firstorder. + reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. + apply <- poe. firstorder. Qed. (** The partial order defined by subrelation and relation equivalence. *) @@ -279,8 +423,6 @@ Program Instance subrelation_partial_order : unfold relation_equivalence in *. firstorder. Qed. -Instance iff_impl_subrelation : subrelation iff impl. -Proof. firstorder. Qed. - -Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). -Proof. firstorder. Qed. +Lemma inverse_pointwise_relation A (R : relation A) : + relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). +Proof. reflexivity. Qed. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 38bdc0bc9..9d3648fef 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -17,6 +17,7 @@ Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. +Require Export Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.Equivalence. Require Export Coq.Relations.Relation_Definitions. @@ -89,6 +90,7 @@ Ltac reverse_arrows x := end. Ltac default_add_morphism_tactic := + intros ; (try destruct_morphism) ; match goal with | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y) diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 6d77a6a0c..617ea6f4f 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -651,7 +651,7 @@ Proof. unfold Equal; congruence. Qed. Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _). Proof. -constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans]. +constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans]. Qed. Add Relation key E.eq diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 0c19176f8..6afb8fcb7 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -295,12 +295,12 @@ End BoolSpec. Definition E_ST : Setoid_Theory elt E.eq. Proof. -constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. +constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. Qed. Definition Equal_ST : Setoid_Theory t Equal. Proof. -constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. +constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans]. Qed. Add Relation elt E.eq diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 6b30f6351..5ab27cfc7 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -9,7 +9,6 @@ (*i $Id$ i*) Require Import Le Gt Minus Min Bool. -Require Import Coq.Setoids.Setoid. Set Implicit Arguments. @@ -554,8 +553,7 @@ Section Elts. simpl; intros; split; [destruct 1 | apply gt_irrefl]. simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq]. rewrite Heq; intuition. - rewrite <- (IHl x). - tauto. + pose (IHl x). intuition. Qed. Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index a518faa57..6158e88f7 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -44,7 +44,7 @@ Implicit Arguments cons [[A]]. Notation " [] " := nil. Notation " [ x ] " := (cons x nil). -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..). +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1). (** n-ary exists ! *) diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 26638893a..2265715b7 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -121,7 +121,7 @@ Defined. Definition Q_Setoid : Setoid_Theory Q Qeq. Proof. - split; unfold Qeq in |- *; auto; apply Qeq_trans. + split; red; unfold Qeq in |- *; auto; apply Qeq_trans. Qed. Add Setoid Q Qeq Q_Setoid as Qsetoid. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 983c651ab..8f59c048f 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -8,22 +8,18 @@ (*i $Id$: i*) -Set Implicit Arguments. - Require Export Coq.Classes.SetoidTactics. (** For backward compatibility *) -Record Setoid_Theory (A: Type) (Aeq: relation A) : Prop := - { Seq_refl : forall x:A, Aeq x x; - Seq_sym : forall x y:A, Aeq x y -> Aeq y x; - Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z }. - -Implicit Arguments Setoid_Theory []. -Implicit Arguments Seq_refl []. -Implicit Arguments Seq_sym []. -Implicit Arguments Seq_trans []. - +Definition Setoid_Theory := @Equivalence. +Definition Build_Setoid_Theory := @Build_Equivalence. +Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x := + Eval compute in reflexivity. +Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x := + Eval compute in symmetry. +Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z := + Eval compute in transitivity. (** Some tactics for manipulating Setoid Theory not officially declared as Setoid. *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index bc627a283..203fe118d 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -552,8 +552,9 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false); - Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) - (!refine_ref (evm, term)); + if props <> [] then + Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) + (!refine_ref (evm, term)); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); id |