diff options
| -rw-r--r-- | Makefile.common | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 | ||||
| -rw-r--r-- | tactics/class_setoid.ml4 | 279 | ||||
| -rw-r--r-- | theories/Classes/Relations.v | 569 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 322 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 32 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 26 | ||||
| -rw-r--r-- | theories/Program/Basics.v | 143 | ||||
| -rw-r--r-- | theories/Program/Program.v | 1 |
9 files changed, 1008 insertions, 376 deletions
diff --git a/Makefile.common b/Makefile.common index 0e6c3925c6..4a60b251a2 100644 --- a/Makefile.common +++ b/Makefile.common @@ -708,8 +708,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor UNICODEVO:= theories/Unicode/Utf8.vo -CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo \ - theories/Classes/SetoidDec.vo +CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/SetoidClass.vo \ + theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ @@ -766,7 +766,7 @@ DPVO:=contrib/dp/Dp.vo SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \ theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \ - theories/Program/FunctionalExtensionality.vo + theories/Program/FunctionalExtensionality.vo theories/Program/Basics.vo RTAUTOVO:= \ contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 4a2dad8cab..a58125dc09 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1608,7 +1608,7 @@ defined in the same file: \begin{Variants} \item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots - {\ident$_n$}}\tacindex{dependent induction ... generalizing} + {\ident$_n$}}\tacindex{dependent induction \dots\ generalizing} Does dependent induction on the hypothesis {\ident} but first generalizes the goal by the given variables so that they are @@ -1616,9 +1616,9 @@ defined in the same file: to do with the variables that are inside some constructors in the induction hypothesis. The other ones need not be further generalized. -\item {\tt dependent destruction}\tacindex{dependent destruction} +\item {\tt dependent destruction {\ident}}\tacindex{dependent destruction} - Does the generalization of the instance but uses {\tt destruct} + Does the generalization of the instance {\ident} but uses {\tt destruct} instead of {\tt induction} on the generalized hypothesis. This gives results equivalent to {\tt inversion} or {\tt dependent inversion} if the hypothesis is dependent. diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4 index 66324158dd..dcc3ffbd24 100644 --- a/tactics/class_setoid.ml4 +++ b/tactics/class_setoid.ml4 @@ -42,22 +42,45 @@ let e_give_exact c gl = let assumption id = e_give_exact (mkVar id) let morphism_class = lazy (class_info (id_of_string "Morphism")) -let morphism2_class = lazy (class_info (id_of_string "BinaryMorphism")) -let morphism3_class = lazy (class_info (id_of_string "TernaryMorphism")) let get_respect cl = Option.get (List.hd (Recordops.lookup_projections cl.cl_impl)) let respect_proj = lazy (get_respect (Lazy.force morphism_class)) -let respect2_proj = lazy (get_respect (Lazy.force morphism2_class)) -let respect3_proj = lazy (get_respect (Lazy.force morphism3_class)) let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") let iff = lazy (gen_constant ["Init"; "Logic"] "iff") +let impl = lazy (gen_constant ["Program"; "Basics"] "impl") +let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") + +let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive") +let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive") + +let symmetric_type = lazy (gen_constant ["Classes"; "Relations"] "Symmetric") +let symmetric_proof = lazy (gen_constant ["Classes"; "Relations"] "symmetric") + +let transitive_type = lazy (gen_constant ["Classes"; "Relations"] "Transitive") +let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive") + +let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse") + +let respectful_dep = lazy (gen_constant ["Classes"; "Relations"] "respectful_dep") +let respectful = lazy (gen_constant ["Classes"; "Relations"] "respectful") + +let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence") +let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence") + +(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *) +let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") +let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") + +let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl") let iff_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "iff_setoid") +let eq_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_setoid") + let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv") let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism") let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl") @@ -70,12 +93,10 @@ let arrow_morphism a b = let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) -let class_one = lazy (Lazy.force morphism_class, Lazy.force respect_proj) -let class_two = lazy (Lazy.force morphism2_class, Lazy.force respect2_proj) -let class_three = lazy (Lazy.force morphism3_class, Lazy.force respect3_proj) +let morphism_class = lazy (Lazy.force morphism_class, Lazy.force respect_proj) -exception Found of (constr * constant * constr list * constr * constr array * - (constr * (constr * constr * constr * constr * constr)) option array) +exception Found of (constr * constr * (types * types) list * constr * constr array * + (constr * (constr * constr * constr * constr)) option array) let resolve_morphism_evd env evd app = let ev = Evarutil.e_new_evar evd env app in @@ -88,79 +109,123 @@ let resolve_morphism_evd env evd app = let is_equiv env sigma t = isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t -let resolve_morphism env sigma direction oldt m args args' = - let evars = ref (Evd.create_evar_defs Evd.empty) in - let morph_instance, proj, subst, 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 cls = +let split_head = function + hd :: tl -> hd, tl + | [] -> assert(false) + +let build_signature isevars env m cstrs finalcstr = + let new_evar isevars env t = + Evarutil.e_new_evar isevars env + (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t + in + let mk_relty ty obj = + let relty = mkApp (Lazy.force coq_relation, [| ty |]) in + match obj with + | None -> new_evar isevars env relty + | Some (p, (a, r, oldt, newt)) -> r + in + let rec aux t l = + let t = Reductionops.whd_betadelta env (Evd.evars_of !isevars) t in + match kind_of_term t, l with + | Prod (na, ty, b), obj :: cstrs -> + let (arg, evars) = aux b cstrs in + let relty = mk_relty ty obj in + let arg' = mkApp (Lazy.force respectful, [| ty ; relty ; b ; arg |]) in + arg', (ty, relty) :: evars + | _, _ -> + (match finalcstr with + None -> + let rel = mk_relty t None in + rel, [t, rel] + | Some (t, rel) -> rel, [t, rel]) + | _, _ -> assert false + in aux m cstrs + +let reflexivity_proof env carrier relation x = + let goal = + mkApp (Lazy.force reflexive_type, [| carrier ; relation |]) + in + try let inst = resolve_one_typeclass env goal in + mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |]) + with Not_found -> + let meta = Evarutil.new_meta() in + mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) + +let resolve_morphism env sigma direction oldt m args args' cstr = + let (morphism_cl, morphism_proj) = Lazy.force morphism_class in + 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 evars = ref (Evd.create_evar_defs Evd.empty) in + let pars = match Array.length args with - 1 -> [Lazy.force class_one, 1] - | 2 -> [Lazy.force class_two, 2; Lazy.force class_one, 1] - | n -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1] + 1 -> [1] + | 2 -> [2;1] + | 3 -> [3;2;1] + | _ -> [4;3;2;1] in try - List.iter (fun ((cl, proj), n) -> + List.iter (fun n -> evars := Evd.create_evar_defs Evd.empty; - let cl_param, cl_context = match cl.cl_context with hd :: tl -> hd, tl | [] -> assert false in - let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] (List.map snd cl_context) in let morphargs, morphobjs = array_chop (Array.length args - n) args in let morphargs', morphobjs' = array_chop (Array.length args - n) args' in - let args = List.rev_map (fun (_, c) -> c) ctxevs in let appm = mkApp(m, morphargs) in let appmtype = Typing.type_of env sigma appm in - let app = applistc (mkInd cl.cl_impl) (args @ [appm]) in - let mtype = replace_vars ctxevs (pi3 (snd cl_param)) in + let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in + let cl_args = [| appmtype ; signature ; appm |] in + let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in try - evars := Evarconv.the_conv_x env appmtype mtype !evars; - evars := Evarutil.nf_evar_defs !evars; - let app = Evarutil.nf_isevar !evars app in - raise (Found (resolve_morphism_evd env evars app, proj, args, appm, morphobjs, morphobjs')) + let morph = resolve_morphism_evd env evars app in + let evm = Evd.evars_of !evars in + let sigargs = List.map + (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y) + sigargs + in + let appm = Reductionops.nf_evar evm appm in + let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in + let proj = + mkApp (mkConst morphism_proj, + Array.append cl_args [|morph|]) + in + raise (Found (morph, proj, sigargs, appm, morphobjs, morphobjs')) with Not_found -> () | Reduction.NotConvertible -> () | Stdpp.Exc_located (_, Pretype_errors.PretypeError _) | Pretype_errors.PretypeError _ -> ()) - cls; + pars; raise Not_found with Found x -> x in - evars := Evarutil.nf_evar_defs !evars; - let evm = Evd.evars_of !evars in - let ctxargs = List.map (Reductionops.nf_evar evm) subst in - let m' = Reductionops.nf_evar evm m' in - let appproj = applistc (mkConst proj) (ctxargs @ [m' ; morph_instance]) in let projargs, respars, typeargs = array_fold_left2 - (fun (acc, ctxargs, typeargs') x y -> - let par, ctx = list_chop 3 ctxargs in + (fun (acc, sigargs, typeargs') x y -> + let (carrier, relation), sigargs = split_head sigargs in match y with None -> - let refl_proof = setoid_refl par x in - [ refl_proof ; x ; x ] @ acc, ctx, x :: typeargs' - | Some (p, (_, _, _, _, t')) -> - if direction then - [ p ; t'; x ] @ acc, ctx, t' :: typeargs' - else [ p ; x; t' ] @ acc, ctx, t' :: typeargs') - ([], ctxargs, []) args args' + let refl_proof = reflexivity_proof env carrier relation x in + [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs' + | Some (p, (_, _, _, t')) -> + [ p ; t'; x ] @ acc, sigargs, t' :: typeargs') + ([], sigargs, []) args args' in - let proof = applistc appproj (List.rev projargs) in + let proof = applistc proj (List.rev projargs) in let newt = applistc m' (List.rev typeargs) in match respars with - [ a ; r ; s ] -> (proof, (a, r, s, oldt, newt)) + [ a, r ] -> (proof, (a, r, oldt, newt)) | _ -> assert(false) - -let build_new gl env setoid direction occs origt newt hyp hypinfo concl = + +let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr = let is_occ occ = occs = [] || List.mem occ occs in - let rec aux t occ = + let rec aux t occ cstr = match kind_of_term t with | _ when eq_constr t origt -> if is_occ occ then @@ -170,70 +235,82 @@ let build_new gl env setoid direction occs origt newt hyp hypinfo concl = | App (m, args) -> let args', occ = Array.fold_left - (fun (acc, occ) arg -> let res, occ = aux arg occ in (res :: acc, occ)) + (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ)) ([], occ) args in - let res = + 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 (project gl) direction t m args args') + (try Some (resolve_morphism env sigma direction t m args args' cstr) with Not_found -> None) in res, occ | Prod (_, x, b) -> - let x', occ = aux x occ in - let b', occ = aux b occ in + let x', occ = aux x occ None in + let b', occ = aux b occ None in let res = if x' = None && b' = None then None else - (try Some (resolve_morphism env (project gl) direction t (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |]) + (try Some (resolve_morphism env sigma direction t + (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |] + cstr) with Not_found -> None) in res, occ | _ -> None, occ - in aux concl 1 - -let decompose_setoid_eqhyp env sigma c dir t = - match kind_of_term t with - | App (equiv, [| a; r; s; x; y |]) -> - if dir then (c, (a, r, s, x, y)) - else (c, (a, r, s, y, x)) - | App (r, args) when Array.length args >= 2 -> - (try - let (p, (a, r, s, _, _)) = resolve_morphism env sigma dir t r args (Array.map (fun _ -> None) args) in - let _, args = array_chop (Array.length args - 2) args in - if dir then (c, (a, r, s, args.(0), args.(1))) - else (c, (a, r, s, args.(1), args.(0))) - with Not_found -> error "Not a (declared) setoid equality") - | _ -> error "Not a setoid equality" + in aux concl 1 cstr + +let decompose_setoid_eqhyp gl env sigma c left2right t = + let (c, (car, rel, x, y) as res) = + match kind_of_term t with + (* | App (equiv, [| a; r; s; x; y |]) -> *) + (* if dir then (c, (a, r, s, x, y)) *) + (* else (c, (a, r, s, y, x)) *) + | App (r, args) when Array.length args >= 2 -> + let relargs, args = array_chop (Array.length args - 2) args in + let rel = mkApp (r, relargs) in + let typ = pf_type_of gl rel in + (match kind_of_term typ with + | App (relation, [| carrier |]) when eq_constr relation (Lazy.force coq_relation) + || eq_constr relation (Lazy.force coq_relationT) -> + (c, (carrier, rel, args.(0), args.(1))) + | _ when isArity typ -> + let (ctx, ar) = destArity typ in + (match ctx with + [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> + (c, (sx, rel, args.(0), args.(1))) + | _ -> error "Only binary relations are supported") + | _ -> error "Not a relation") + | _ -> error "Not a relation" + in + if left2right then res + else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x)) let cl_rewrite_clause c left2right occs clause gl = let env = pf_env gl in let sigma = project gl in let hyp = pf_type_of gl c in - let hypt, (typ, rel, setoid, origt, newt as hypinfo) = decompose_setoid_eqhyp env sigma c left2right hyp in + let hypt, (typ, rel, origt, newt as hypinfo) = decompose_setoid_eqhyp gl env sigma c left2right hyp in let concl, is_hyp = match clause with Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id | None -> pf_concl gl, None in - let eq, _ = build_new gl env setoid left2right occs origt newt hypt hypinfo concl in + let cstr = + match is_hyp with + None -> (mkProp, mkApp (Lazy.force inverse, [| mkProp; Lazy.force impl |])) + | Some _ -> (mkProp, Lazy.force impl) + in + let eq, _ = build_new gl env sigma left2right occs origt newt hypt hypinfo concl (Some cstr) in match eq with - Some (p, (_, _, _, _, t)) -> - let proj = - if left2right then - let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in - applistc (Lazy.force proj) - [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] - else - let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in - applistc (Lazy.force proj) - [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] - in - (match is_hyp with - | Some id -> Tactics.apply_in true id [proj,NoBindings] - | None -> Tactics.apply proj) gl + Some (p, (_, _, oldt, newt)) -> + (match is_hyp with + | Some id -> Tactics.apply_in true id [p,NoBindings] + | None -> + let meta = Evarutil.new_meta() in + let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in + refine term) gl | None -> tclIDTAC gl open Extraargs @@ -258,3 +335,17 @@ let clsubstitute o c = TACTIC EXTEND map_tac | [ "clsubstitute" orient(o) constr(c) ] -> [ clsubstitute o c ] END + + +(* + let proj = + if left2right then + let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in + applistc (Lazy.force proj) + [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] + else + let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in + applistc (Lazy.force proj) + [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] + in +*) diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v new file mode 100644 index 0000000000..6ecd4ac3c7 --- /dev/null +++ b/theories/Classes/Relations.v @@ -0,0 +1,569 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Typeclass-based setoids, tactics and standard instances. + TODO: explain clrewrite, clsubstitute and so on. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) + +Require Import Coq.Program.Program. +Require Import Coq.Classes.Init. + +Set Implicit Arguments. +Unset Strict Implicit. + +Definition relationT A := A -> A -> Type. +Definition relation A := A -> A -> Prop. + +Definition inverse A (R : relation A) : relation A := flip R. + +Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R. +Proof. intros ; unfold inverse. apply (flip_flip R). Qed. + +Definition complementT A (R : relationT A) := fun x y => ! R x y. + +Definition complement A (R : relation A) := fun x y => ~ R x y. + +(** These are convertible. *) + +Lemma complementT_flip : forall A (R : relationT A), complementT (flip R) = flip (complementT R). +Proof. reflexivity. Qed. + +Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). +Proof. reflexivity. Qed. + +(** We rebind relations in separate classes to be able to overload each proof. *) + +Class Reflexive A (R : relationT A) := + reflexive : forall x, R x x. + +Class Irreflexive A (R : relationT A) := + irreflexive : forall x, R x x -> False. + +Class Symmetric A (R : relationT A) := + symmetric : forall x y, R x y -> R y x. + +Class Asymmetric A (R : relationT A) := + asymmetric : forall x y, R x y -> R y x -> False. + +Class Transitive A (R : relationT A) := + transitive : forall x y z, R x y -> R y z -> R x z. + +Implicit Arguments Reflexive [A]. +Implicit Arguments Irreflexive [A]. +Implicit Arguments Symmetric [A]. +Implicit Arguments Asymmetric [A]. +Implicit Arguments Transitive [A]. + +Hint Resolve @irreflexive : ord. + +(** We can already dualize all these properties. *) + +Program Instance [ Reflexive A R ] => flip_reflexive : Reflexive A (flip R) := + reflexive := reflexive (R:=R). + +Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R) := + irreflexive := irreflexive (R:=R). + +Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R). + + Solve Obligations using unfold flip ; program_simpl ; eapply symmetric ; eauto. + +Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R). + + Solve Obligations using program_simpl ; unfold flip in * ; intros ; eapply asymmetric ; eauto. + +Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R). + + Solve Obligations using unfold flip ; program_simpl ; eapply transitive ; eauto. + +(** Have to do it again for Prop. *) + +Program Instance [ Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive A (inverse R) := + reflexive := reflexive (R:=R). + +Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive A (inverse R) := + irreflexive := irreflexive (R:=R). + +Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R). + + Solve Obligations using unfold inverse, flip ; program_simpl ; eapply symmetric ; eauto. + +Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R). + + Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; eapply asymmetric ; eauto. + +Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R). + + Solve Obligations using unfold inverse, flip ; program_simpl ; eapply transitive ; eauto. + +Program Instance [ Reflexive A (R : relation A) ] => + reflexive_complement_irreflexive : Irreflexive A (complement R). + + Next Obligation. + Proof. + unfold complement in * ; intros. + apply H. + apply reflexive. + Qed. + +Program Instance [ Irreflexive A (R : relation A) ] => + irreflexive_complement_reflexive : Reflexive A (complement R). + + Next Obligation. + Proof. + unfold complement in * ; intros. + red ; intros. + apply (irreflexive H). + Qed. + +Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R). + + Next Obligation. + Proof. + unfold complement in *. + red ; intros H'. + apply (H (symmetric H')). + Qed. + +(** Tactics to solve goals. Each tactic comes in two flavors: + - a tactic to immediately solve a goal without user intervention + - a tactic taking input from the user to make progress on a goal *) + +Definition relate A (R : relationT A) : relationT A := R. + +Ltac relationify_relation R R' := + match goal with + | [ H : context [ R ?x ?y ] |- _ ] => change (R x y) with (R' x y) in H + | [ |- context [ R ?x ?y ] ] => change (R x y) with (R' x y) + end. + +Ltac relationify R := + set (R' := relate R) ; progress (repeat (relationify_relation R R')). + +Ltac relation_refl := + match goal with + | [ |- ?R ?X ?X ] => apply (reflexive (R:=R) X) + | [ H : ?R ?X ?X |- _ ] => apply (irreflexive (R:=R) H) + + | [ |- ?R ?A ?X ?X ] => apply (reflexive (R:=R A) X) + | [ H : ?R ?A ?X ?X |- _ ] => apply (irreflexive (R:=R A) H) + + | [ |- ?R ?A ?B ?X ?X ] => apply (reflexive (R:=R A B) X) + | [ H : ?R ?A ?B ?X ?X |- _ ] => apply (irreflexive (R:=R A B) H) + + | [ |- ?R ?A ?B ?C ?X ?X ] => apply (reflexive (R:=R A B C) X) + | [ H : ?R ?A ?B ?C ?X ?X |- _ ] => apply (irreflexive (R:=R A B C) H) + + | [ |- ?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) + end. + +Ltac refl := relation_refl. + +Ltac relation_sym := + match goal with + | [ H : ?R ?X ?Y |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?X ?Y |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?X ?Y |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?C ?X ?Y |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y) H) + + | [ 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) + + end. + +Ltac relation_symmetric := + match goal with + | [ |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y)) + + | [ |- ?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)) + end. + +Ltac sym := relation_symmetric. + +Ltac relation_trans := + match goal with + | [ H : ?R ?X ?Y, H' : ?R ?Y ?Z |- ?R ?X ?Z ] => + apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?X ?Y, H' : ?R ?A ?Y ?Z |- ?R ?A ?X ?Z ] => + apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?X ?Y, H' : ?R ?A ?B ?Y ?Z |- ?R ?A ?B ?X ?Z ] => + apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?X ?Y, H' : ?R ?A ?B ?C ?Y ?Z |- ?R ?A ?B ?C ?X ?Z ] => + apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => + apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H') + end. + +Ltac relation_transitive Y := + match goal with + | [ |- ?R ?X ?Z ] => + apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?X ?Z ] => + apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?X ?Z ] => + apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?X ?Z ] => + apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => + apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z)) + end. + +Ltac trans Y := relation_transitive Y. + +(** To immediatly solve a goal on setoid equality. *) + +Ltac relation_tac := relation_refl || relation_sym || relation_trans. + +(** * Morphisms. + + We now turn to the definition of [Morphism] and declare standard instances. + These will be used by the [clrewrite] tactic later. *) + +(** Respectful morphisms. *) + +Definition respectful_depT (A : Type) (R : relationT A) + (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := + fun f g => forall x y : A, R x y -> R' x y (f x) (g y). + +Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) := + Eval compute in (respectful_depT eqa (fun _ _ => eqb)). + +Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) := + fun f g => forall x y : A, R x y -> R' (f x) (g y). + +(** Notations reminiscent of the old syntax for declaring morphisms. + We use three + or - for type morphisms, and two for [Prop] ones. + *) + +Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20). +Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20). + +Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20). +Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20). + +(** A morphism on a relation [R] is an object respecting the relation (in its kernel). + The relation [R] will be instantiated by [respectful] and [A] by an arrow type + for usual morphisms. *) + +Class Morphism A (R : relationT A) (m : A) := + respect : R m m. + +Ltac simpl_morphism := + try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; + try (red ; intros) ; try ( solve [ intuition ]). + +Ltac obligations_tactic ::= simpl_morphism. + +(** The arrow is a reflexive and transitive relation on types. *) + +Program Instance arrow_refl : ? Reflexive arrow := + reflexive X := id. + +Program Instance arrow_trans : ? Transitive arrow := + transitive X Y Z f g := g o f. + +(** Can't use the definition [notT] as it gives a to universe inconsistency. *) + +Program Instance notT_arrow_morphism : + Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False). + +(** Isomorphism. *) + +Definition iso (A B : Type) := + A -> B * B -> A. + +Program Instance iso_refl : ? Reflexive iso. +Program Instance iso_sym : ? Symmetric iso. +Program Instance iso_trans : ? Transitive iso. + +Program Instance not_iso_morphism : + Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False). + +(** Logical implication. *) + +Program Instance impl_refl : ? Reflexive impl. +Program Instance impl_trans : ? Transitive impl. + +Program Instance not_impl_morphism : + Morphism (Prop -> Prop) (impl --> impl) not. + +(** Logical equivalence. *) + +Program Instance iff_refl : ? Reflexive iff. +Program Instance iff_sym : ? Symmetric iff. +Program Instance iff_trans : ? Transitive iff. + +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]. + +(** If you have a morphism from [RA] to [RB] you have a contravariant morphism + from [RA] to [inverse RB]. *) + +Program Instance `A` (RA : relation A) `B` (RB : relation B) [ ? Morphism (RA ++> RB) m ] => + morph_impl_co_contra_inverse : + ? Morphism (RA --> inverse RB) m. + + Next Obligation. + Proof. + apply respect. + apply H. + Qed. + +(** Every transitive relation gives rise to a binary morphism on [impl], + contravariant in the first argument, covariant in the second. *) + +Program Instance [ Transitive A (R : relation A) ] => + trans_contra_co_morphism : ? Morphism (R --> R ++> impl) R. + + Next Obligation. + Proof with auto. + trans x... + trans x0... + Qed. + +(** Dually... *) + +Program Instance [ Transitive A (R : relation A) ] => + trans_co_contra_inv_impl_morphism : ? Morphism (R ++> R --> inverse impl) R. + + Obligations Tactic := idtac. + + Next Obligation. + Proof with auto. + intros. + destruct (trans_contra_co_morphism (R:=inverse R)). + revert respect0. + unfold respectful, inverse, flip in * ; intros. + apply respect0 ; auto. + Qed. + +Obligations Tactic := simpl_morphism. + +(** With symmetric relations, variance is no issue ! *) + +Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) + [ Morphism _ (R ++> R') m ] => + sym_contra_morphism : ? Morphism (R --> R') m. + + Next Obligation. + Proof with auto. + apply respect. + sym... + Qed. + +(** Every symmetric and transitive relation gives rise to an equivariant morphism. *) + +Program Instance [ Transitive A (R : relation A), Symmetric A R ] => + trans_sym_morphism : ? Morphism (R ++> R ++> iff) R. + + Next Obligation. + Proof with auto. + split ; intros. + trans x0... trans x... sym... + + trans y... trans y0... sym... + Qed. + +(** The complement of a relation conserves its morphisms. *) + +Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => + complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R). + + Next Obligation. + Proof. + red ; unfold complement ; intros. + pose (respect). + pose (r x y H). + pose (r0 x0 y0 H0). + intuition. + Qed. + +(** The inverse too. *) + +Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => + inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R). + + Next Obligation. + Proof. + unfold inverse ; unfold flip. + apply respect ; auto. + 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. + +(** Any binary morphism respecting some relations up to [iff] respects + them up to [impl] in each way. Very important instances as we need [impl] + morphisms at the top level when we rewrite. *) + +Program Instance `A` (R : relation A) `B` (R' : relation B) + [ ? Morphism (R ++> R' ++> iff) m ] => + iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m. + + Next Obligation. + Proof. + destruct respect with x y x0 y0 ; auto. + Qed. + +Program Instance `A` (R : relation A) `B` (R' : relation B) + [ ? Morphism (R ++> R' ++> iff) m ] => + iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m. + + Next Obligation. + Proof. + destruct respect with x y x0 y0 ; auto. + Qed. + +(** 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_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_iff_morphism : ? Morphism (iff ++> iff ++> iff) or. + +(** Leibniz equality. *) + +Program Instance eq_refl : ? Reflexive (@eq A). +Program Instance eq_sym : ? Symmetric (@eq A). +Program Instance eq_trans : ? Transitive (@eq A). + +Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)) := + trans_sym_morphism. + +Program Instance `A B` (m : A -> B) => arrow_morphism : ? Morphism (eq ++> eq) m. + +(** The [PER] typeclass. *) + +Class PER (carrier : Type) (pequiv : relationT carrier) := + per_sym :> Symmetric pequiv ; + per_trans :> Transitive pequiv. + +(** We can build a PER on the coq function space if we have PERs on the domain and + codomain. *) + +Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => + arrow_per : PER (A -> B) + (fun f g => forall (x y : A), R x y -> R' (f x) (g y)). + + Next Obligation. + Proof with auto. + constructor ; intros... + assert(R x0 x0) by (trans y0 ; [ auto | sym ; auto ]). + trans (y x0)... + Qed. + +(** The [Equivalence] typeclass. *) + +Class Equivalence (carrier : Type) (equiv : relationT carrier) := + equiv_refl :> Reflexive equiv ; + equiv_sym :> Symmetric equiv ; + equiv_trans :> Transitive equiv. + +(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) + +Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) := + antisymmetric : forall x y, R x y -> R y x -> eqA x y. + +Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => + flip_antisymmetric : ? Antisymmetric eq (flip R). + + Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto. + +(** 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 : relation A), Equivalence B (R' : relation B) ] => + respecting_equiv : Equivalence respecting + (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)). + + Next Obligation. + Proof. + constructor ; intros. + destruct x ; simpl. + apply r ; auto. + Qed. + + Next Obligation. + Proof. + constructor ; intros. + sym ; apply H. + sym ; auto. + Qed. + + Next Obligation. + Proof. + constructor ; intros. + trans ((`y) y0). + apply H ; auto. + apply H0. refl. + Qed. + +(** Leibinz equality [eq] is an equivalence relation. *) + +Program Instance eq_equivalence : Equivalence A eq. + +(** Logical equivalence [iff] is an equivalence relation. *) + +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)). +*) diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index f61b4a4159..78e53aa012 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -22,72 +22,48 @@ Require Import Coq.Classes.Init. Set Implicit Arguments. Unset Strict Implicit. -(** We first define setoids on a carrier, it amounts to an equivalence relation. - Now [equiv] is overloaded for every [Setoid]. -*) +Require Export Coq.Classes.Relations. -Require Export Coq.Relations.Relations. +(** A setoid wraps an equivalence. *) -Class Setoid (carrier : Type) (equiv : relation carrier) := - equiv_prf : equivalence carrier equiv. +Class Setoid A := + equiv : relation A ; + setoid_equiv :> Equivalence A equiv. -(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +(** Shortcuts to make proof search easier. *) -Definition equiv [ Setoid A R ] : _ := R. +Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. +Proof. eauto with typeclass_instances. Qed. -(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *) +Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. +Proof. eauto with typeclass_instances. Qed. -(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *) -Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope. +Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. +Proof. eauto with typeclass_instances. Qed. -Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope. +(** Standard setoids. *) -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. +Program Instance eq_setoid : Setoid A := + equiv := eq ; setoid_equiv := eq_equivalence. -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. - -(** 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) - | [ |- ?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. +Program Instance iff_setoid : Setoid Prop := + equiv := iff ; setoid_equiv := iff_equivalence. -Ltac refl := do_setoid_refl. +(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) -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. +(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *) +(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *) -Ltac sym := do_setoid_sym. +Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope. -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)) - | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z)) - | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z)) - | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z)) - end. +Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope. -Ltac trans y := do_setoid_trans y. +Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x. +Proof with auto. + intros ; red ; intros. + apply H. + sym... +Qed. (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *) @@ -106,66 +82,24 @@ Ltac clsubst_nofail := Tactic Notation "clsubst" "*" := clsubst_nofail. -(** 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) - | [ H : ?X =/= ?X |- _ ] => elim H ; setoid_refl - 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. + assert(z == y) by relation_sym. + assert(x == y) by relation_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. + assert(y == x) by relation_sym. + assert(y == z) by relation_trans. contradiction. Qed. Open Scope type_scope. -(** Need to fix fresh to not fail if some arguments are not identifiers. *) -(* Ltac setoid_sat ::= *) -(* match goal with *) -(* | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *) -(* | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *) -(* | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *) -(* | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *) -(* | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *) -(* end. *) - -Ltac setoid_sat := - match goal with - | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H) - | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H) - | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H') - | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H') - | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H') - end. - Ltac setoid_simplify_one := match goal with | [ H : ?x == ?x |- _ ] => clear H @@ -175,192 +109,68 @@ Ltac setoid_simplify_one := Ltac setoid_simplify := repeat setoid_simplify_one. -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 |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y) + | [ s : Setoid ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H + | [ s : Setoid ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y) 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). - -Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => - Morphism (m : a -> b) := - respect : respectful m. - -(** Here we build a setoid instance for functions which relates respectful ones only. *) - -Definition respecting [ Setoid a R, Setoid b R' ] : Type := - { morph : a -> b | respectful morph }. - -Ltac obligations_tactic ::= try red ; program_simpl ; try tauto. - -Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => - arrow_setoid : - Setoid ({ morph : a -> b | respectful morph }) - - (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) := - equiv_prf := Build_equivalence _ _ _ _ _. - - Next Obligation. - Proof. - trans (y x0) ; eauto. - apply H. - refl. - Qed. - - Next Obligation. - Proof. - sym ; apply H. - sym ; auto. - Qed. - -(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from - some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *) - -Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] - (m : a -> b -> c) : Prop := - forall x y, eqa x y -> - forall z w, eqb z w -> eqc (m x z) (m y w). - -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => - BinaryMorphism (m : a -> b -> c) := - respect2 : binary_respectful m. - -Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] - (m : a -> b -> c -> d) : Prop := - forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v). - -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => - TernaryMorphism (m : a -> b -> c -> d) := - respect3 : ternary_respectful m. - -(** Definition of the usual morphisms in [Prop]. *) - -Program Instance iff_setoid : Setoid Prop iff := - equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym. - -Program Instance not_morphism : Morphism Prop iff Prop iff not. - -Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and. - -(* We make the setoids implicit, they're always [iff] *) - -Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]]. - -Program Instance or_morphism : ? BinaryMorphism or. - -Definition impl (A B : Prop) := A -> B. - -Program Instance impl_morphism : ? BinaryMorphism impl. - -Next Obligation. -Proof. - unfold impl. tauto. -Qed. - (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) -Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R. +Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv := + trans_sym_morphism. -Next Obligation. -Proof with auto. - split ; intros. - trans x. sym... trans z... - trans y... trans w... sym... -Qed. - -Definition iff_morphism : BinaryMorphism iff := setoid_morphism. +(** Add this very useful instance in the database. *) -Existing Instance iff_morphism. +Implicit Arguments setoid_morphism [[!sa]]. +Existing Instance setoid_morphism. -Implicit Arguments eq [[A]]. +Definition type_eq : relation Type := + fun x y => x = y. -Program Instance eq_setoid : Setoid A eq := - equiv_prf := Build_equivalence _ _ _ _ _. +Program Instance type_equivalence : Equivalence Type type_eq. -Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq. + Solve Obligations using constructor ; unfold type_eq ; program_simpl. -Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m. +Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto. -Implicit Arguments arrow_morphism [[A] [B] [C]]. +Ltac obligations_tactic ::= morphism_tac. -Program Instance type_setoid : Setoid Type (fun x y => x = y) := - equiv_prf := Build_equivalence _ _ _ _ _. +(** 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. *) -Lemma setoid_subst : forall (x y : Type), x == y -> x -> y. -Proof. - intros. - rewrite <- H. - apply X. -Qed. +Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id. -Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y. -Proof. - intros. - clrewrite <- H. - apply H0. -Qed. +Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. -Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, - mg : ? Morphism sb sc g, mf : ? Morphism sa sb f ] => - compose_morphism : ? Morphism sa sc (fun x => g (f x)). +(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *) +(* (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *) + -Next Obligation. -Proof. - apply (respect (m0:=mg)). - apply (respect (m0:=mf)). - assumption. -Qed. +(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *) +(* [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] => *) +(* compose_morphism : ? Morphism (compose_respect R R') (g o f). *) + +(* Next Obligation. *) +(* Proof. *) +(* apply (respect (m0:=mg)). *) +(* apply (respect (m0:=mf)). *) +(* assumption. *) +(* Qed. *) (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *) -Class PartialSetoid (carrier : Type) (equiv : relation carrier) := - pequiv_prf : PER carrier equiv. +Class PartialSetoid (carrier : Type) := + pequiv : relation carrier ; + pequiv_prf :> PER carrier pequiv. (** Overloaded notation for partial setoid equivalence. *) -Definition pequiv [ PartialSetoid A R ] : _ := R. - Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. -Definition pequiv_sym [ s : PartialSetoid A R ] : forall x y : A, R x y -> R y x := per_sym _ _ pequiv_prf. -Definition pequiv_trans [ s : PartialSetoid A R ] : forall x y z : A, R x y -> R y z -> R x z := per_trans _ _ pequiv_prf. - -Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_partial_setoid : - PartialSetoid (a -> b) - (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) := - pequiv_prf := Build_PER _ _ _ _. - -Next Obligation. -Proof. - sym. - apply H. - sym ; assumption. -Qed. - -Next Obligation. -Proof. - trans (y x0). - apply H ; auto. - trans y0 ; auto. - sym ; auto. - apply H0 ; auto. -Qed. - -(** The following is not definable. *) -(* -Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : - Setoid (a -> b) - (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) := - equiv_prf := Build_equivalence _ _ _ _ _. -*) - (** Reset the default Program tactic. *) Ltac obligations_tactic ::= program_simpl. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index f68a7d3a4b..0a86233166 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass. Require Import Coq.Logic.Decidable. -Class [ Setoid A R ] => DecidableSetoid := +Class [ Setoid A ] => DecidableSetoid := setoid_decidable : forall x y : A, decidable (x == y). (** The [EqDec] class gives a decision procedure for a particular setoid equality. *) -Class [ Setoid A R ] => EqDec := +Class [ Setoid A ] => EqDec := equiv_dec : forall x y : A, { x == y } + { x =/= y }. (** We define the [==] overloaded notation for deciding equality. It does not take precedence @@ -44,15 +44,15 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } := match x with - | left H => right _ H - | right H => left _ H + | left H => @right _ _ H + | right H => @left _ _ H end. Require Import Coq.Program.Program. (** Invert the branches. *) -Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). +Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). (** Overloaded notation for inequality. *) @@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70). (** Define boolean versions, losing the logical information. *) -Definition equiv_decb [ EqDec A R ] (x y : A) : bool := +Definition equiv_decb [ EqDec A ] (x y : A) : bool := if x == y then true else false. -Definition nequiv_decb [ EqDec A R ] (x y : A) : bool := +Definition nequiv_decb [ EqDec A ] (x y : A) : bool := negb (equiv_decb x y). Infix "==b" := equiv_decb (no associativity, at level 70). @@ -71,19 +71,19 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -Implicit Arguments eq [[A]]. - Require Import Coq.Arith.Arith. -Program Instance nat_eqdec : EqDec nat eq := +(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) + +Program Instance nat_eq_eqdec : ? EqDec (@eq_setoid nat) := equiv_dec := eq_nat_dec. Require Import Coq.Bool.Bool. -Program Instance bool_eqdec : EqDec bool eq := +Program Instance bool_eqdec : ? EqDec (@eq_setoid bool) := equiv_dec := bool_dec. -Program Instance unit_eqdec : EqDec unit eq := +Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) := equiv_dec x y := left. Next Obligation. @@ -92,7 +92,8 @@ Program Instance unit_eqdec : EqDec unit eq := reflexivity. Qed. -Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq := +Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => + prod_eqdec : ? EqDec (@eq_setoid (prod A B)) := equiv_dec x y := dest x as (x1, x2) in dest y as (y1, y2) in @@ -101,13 +102,11 @@ Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq else right else right. - Solve Obligations using unfold equiv ; program_simpl ; try red ; intros ; autoinjections ; discriminates. - (** Objects of function spaces with countable domains like bool have decidable equality. *) Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq := +Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then if f false == g false then left @@ -118,7 +117,6 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq := Next Obligation. Proof. - red. extensionality x. destruct x ; auto. Qed. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 540ac184e6..39809865cd 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -25,12 +25,12 @@ Require Export Coq.Classes.SetoidClass. (* Application of the extensionality axiom to turn a goal on leibinz equality to a setoid equivalence. *) -Lemma setoideq_eq [ sa : Setoid a eqa ] : forall x y, eqa x y -> x = y. +Lemma setoideq_eq [ sa : Setoid a ] : forall x y : a, x == y -> x = y. Proof. admit. Qed. -Implicit Arguments setoideq_eq [[a] [eqa] [sa]]. +Implicit Arguments setoideq_eq [[a] [sa]]. (** Application of the extensionality principle for setoids. *) @@ -65,5 +65,25 @@ Ltac setoid_tactic := | [ 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 + | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tactic end. +(** Need to fix fresh to not fail if some arguments are not identifiers. *) +(* Ltac setoid_sat ::= *) +(* match goal with *) +(* | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *) +(* | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *) +(* | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *) +(* | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *) +(* | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *) +(* end. *) + +Ltac setoid_sat := + match goal with + | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H) + | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H) + | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H') + | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H') + | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H') + end. +Ltac setoid_saturate := repeat setoid_sat. + diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v new file mode 100644 index 0000000000..e5bc98dee3 --- /dev/null +++ b/theories/Program/Basics.v @@ -0,0 +1,143 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* Standard functions and proofs about them. + * Author: Matthieu Sozeau + * Institution: LRI, CNRS UMR 8623 - Universit�copyright Paris Sud + * 91405 Orsay, France *) + +(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) + +Set Implicit Arguments. +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). + +Definition arrow (A B : Type) := A -> B. + +Definition impl (A B : Prop) : Prop := A -> B. + +Definition id `A` := fun x : A => x. + +Hint Unfold compose. + +Notation " g 'o' f " := (compose g f) (at level 50, left associativity) : program_scope. + +Open Scope program_scope. + +Lemma compose_id_left : forall A B (f : A -> B), id o 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. +Proof. + intros. + unfold id, compose. + symmetry ; apply eta_expansion. +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. +Proof. + reflexivity. +Qed. + +Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. + +Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing). + +Definition const `A B` (a : A) := fun x : B => a. + +Definition flip `A B C` (f : A -> B -> C) x y := f y x. + +Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f. +Proof. + unfold flip. + intros. + extensionality x ; extensionality y. + reflexivity. +Qed. + +Definition apply `A B` (f : A -> B) (x : A) := f x. + +(** Notations for the unit type and value. *) + +Notation " () " := Datatypes.unit : type_scope. +Notation " () " := tt. + +(** Set maximally inserted implicit arguments for standard definitions. *) + +Implicit Arguments eq [[A]]. + +Implicit Arguments Some [[A]]. +Implicit Arguments None [[A]]. + +Implicit Arguments inl [[A] [B]]. +Implicit Arguments inr [[A] [B]]. + +Implicit Arguments left [[A] [B]]. +Implicit Arguments right [[A] [B]]. + +(** Curryfication. *) + +Definition curry `a b c` (f : a -> b -> c) (p : prod a b) : c := + let (x, y) := p in f x y. + +Definition uncurry `a b c` (f : prod a b -> c) (x : a) (y : b) : c := + f (x, y). + +Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f. +Proof. + simpl ; intros. + unfold uncurry, curry. + extensionality x ; extensionality y. + reflexivity. +Qed. + +Lemma curry_uncurry : forall a b c (f : prod a b -> c), curry (uncurry f) = f. +Proof. + simpl ; intros. + unfold uncurry, curry. + extensionality x. + destruct x ; simpl ; reflexivity. +Qed. + +(** Useful implicits and notations for lists. *) + +Require Export Coq.Lists.List. + +Implicit Arguments nil [[A]]. +Implicit Arguments cons [[A]]. + +Notation " [] " := nil. +Notation " [ x ] " := (cons x nil). +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..). + +(** n-ary exists ! *) + +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)))))) + (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)))))))) + (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope. + +Tactic Notation "exist" constr(x) := exists x. +Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. +Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. +Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. + +Notation " ! A " := (notT A) (at level 200, A at level 100) : type_scope. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index fb172db845..4d92be3c5d 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -2,3 +2,4 @@ Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. Require Export Coq.Program.Subset. +Require Export Coq.Program.Basics.
\ No newline at end of file |