diff options
| -rw-r--r-- | Makefile.common | 3 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 2 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 12 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 45 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 96 |
5 files changed, 151 insertions, 7 deletions
diff --git a/Makefile.common b/Makefile.common index a8801f3df0..919e9243e8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -706,7 +706,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.v +CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.v \ + theories/Classes/SetoidDec.v THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 0703bcb837..aba11231cd 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -118,7 +118,6 @@ let env_with_binders env isevars l = let subtac_process env isevars id bl c tycon = (* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *) - let imps = Implicit_quantifiers.implicits_of_binders bl in let c = Command.abstract_constr_expr c bl in let tycon = match tycon with @@ -130,6 +129,7 @@ let subtac_process env isevars id bl c tycon = mk_tycon coqt in let c = coqintern_constr !isevars env c in + let imps = Implicit_quantifiers.implicits_of_rawterm c in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars (evars_of !isevars) in evm, coqc, ctyp, imps diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 2de7945ee4..c029550a13 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -59,6 +59,9 @@ let is_freevar ids env x = with _ -> not (is_global x) with _ -> true +let rec make_fresh ids env x = + if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x) + let freevars_of_ids env ids = List.filter (is_freevar env (Global.env())) ids @@ -81,10 +84,10 @@ let compute_constrs_freevars_binders env constrs = let elts = compute_constrs_freevars env constrs in List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts -let next_ident_away_from id avoid = - let rec name_rec id = - if Idset.mem id avoid then name_rec (Nameops.lift_ident id) else id in - name_rec id +let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id +(* let rec name_rec id = *) +(* if Idset.mem id avoid then name_rec (Nameops.lift_ident id) else id in *) +(* name_rec id *) let ids_of_named_context_avoiding avoid l = List.fold_left (fun (ids, avoid) id -> @@ -172,6 +175,7 @@ let generalize_class_binders env l = cstrs let generalize_class_binders_raw env l = + let env = Idset.union env (Termops.vars_of_env (Global.env())) in let fv_ctx, cstrs = resolve_class_binders env l in List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx, List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 915a7a944a..851579e125 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -33,7 +33,7 @@ Class Setoid (carrier : Type) (equiv : relation carrier) := Definition equiv [ Setoid A R ] : _ := R. -Infix "==" := equiv (at level 70, no associativity). +Infix "==" := equiv (at level 70, no associativity) : type_scope. 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. @@ -190,3 +190,46 @@ Proof. apply (respect (m0:=m0)). 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. + +(** 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 _ _ _ _ _. +*)
\ No newline at end of file diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v new file mode 100644 index 0000000000..aa151772d4 --- /dev/null +++ b/theories/Classes/SetoidDec.v @@ -0,0 +1,96 @@ +(* -*- 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 *) +(************************************************************************) + +(* Certified Haskell Prelude. + * 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 Import Coq.Classes.SetoidClass. + +Class [ Setoid A R ] => EqDec := + equiv_dec : forall x y : A, { R x y } + { ~ R x y }. + +Infix "==" := equiv_dec (no associativity, at level 70). + +Require Import Coq.Program.Program. + +Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { ~ R x y } + { R x y } := + if x == y then right else left. + +Infix "<>" := nequiv_dec (no associativity, at level 70). + +Definition equiv_decb [ EqDec A R ] (x y : A) : bool := + if x == y then true else false. + +Definition nequiv_decb [ EqDec A R ] (x y : A) : bool := + negb (equiv_decb x y). + +Infix "==b" := equiv_decb (no associativity, at level 70). +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 := + equiv_dec := eq_nat_dec. + +Require Import Coq.Bool.Bool. + +Program Instance bool_eqdec : EqDec bool eq := + equiv_dec := bool_dec. + +Program Instance unit_eqdec : EqDec unit eq := + equiv_dec x y := left. + +Next Obligation. +Proof. + destruct x ; destruct y. + reflexivity. +Qed. + +Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq := + equiv_dec x y := + dest x as (x1, x2) in + dest y as (y1, y2) in + if x1 == y1 then + if x2 == y2 then left + else right + else right. + +Solve Obligations using program_simpl ; red ; intro ; autoinjections ; discriminates. + +Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq := + equiv_dec f g := + if f true == g true then + if f false == g false then left + else right + else right. + +Require Import Coq.Program.FunctionalExtensionality. + +Next Obligation. +Proof. + extensionality x. + destruct x ; auto. +Qed. + +Next Obligation. +Proof. + red ; intro ; subst. + discriminates. +Qed. |