Permalink
Browse files

Adapt to latest coq trunk version.

  • Loading branch information...
mattam82 committed Mar 26, 2012
1 parent 6a05aa1 commit f90c86d7bcba71075a0ca2ee93a0daab66915956
Showing with 94 additions and 67 deletions.
  1. +0 −1 src/depelim.ml4
  2. +25 −9 src/eqdec.ml4
  3. +22 −22 src/equations.ml4
  4. +3 −1 src/equations_common.ml4
  5. +2 −2 src/sigma.ml4
  6. +4 −4 src/subterm.ml4
  7. +31 −25 test-suite/rec.v
  8. +7 −3 theories/DepElim.v
View
@@ -1,4 +1,3 @@
-(* -*- compile-command: "COQBIN=~/research/coq/trunk/bin/ make -k -C .. src/equations_plugin.cma src/equations_plugin.cmxs" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
View
@@ -133,13 +133,16 @@ let dec_eq () =
init_constant ["Equations";"EqDec"] "dec_eq"
open Decl_kinds
+let vars_of_pars pars =
+ Array.of_list (List.map (fun x -> mkVar (pi1 x)) pars)
let derive_eq_dec ind =
let info = inductive_info ind in
let ctx = info.mutind_params in
- let _cl = eq_dec_class () in
- let stmt_of ind =
- let indapp = mkApp (ind.ind_c, extended_rel_vect 0 ind.ind_args) in
+ let cl = fst (snd (eq_dec_class ())) in
+ let info_of ind =
+ let argsvect = extended_rel_vect 0 ind.ind_args in
+ let indapp = mkApp (ind.ind_c, argsvect) in
let app =
mkApp (dec_eq (), [| indapp |])
in
@@ -152,21 +155,34 @@ let derive_eq_dec ind =
in
let typ = it_mkProd_or_LetIn app ind.ind_args in
let full = it_mkNamedProd_or_LetIn typ ctx in
- full
+ let tc gr =
+ let b, ty = Typeclasses.instance_constructor cl [indapp; mkApp (constr_of_global gr, Array.append (vars_of_pars ctx) argsvect) ] in
+ let ce = { const_entry_body = it_mkNamedLambda_or_LetIn (it_mkLambda_or_LetIn (Option.get b) ind.ind_args) ctx;
+ const_entry_type = Some (it_mkNamedProd_or_LetIn (it_mkProd_or_LetIn ty ind.ind_args) ctx);
+ const_entry_opaque = false; const_entry_secctx = None }
+ in ce
+ in full, tc
in
let indsl = Array.to_list info.mutind_inds in
+ let indsl = List.map (fun ind -> ind, info_of ind) indsl in
let possible_guards =
List.map
- (fun ind ->
+ (fun (ind, _) ->
list_tabulate (fun i -> i) (List.length ind.ind_args + 2))
indsl
+ in
+ let hook _ gr =
+ List.iter (fun (ind, (stmt, tc)) ->
+ let ce = tc gr in
+ let inst = Declare.declare_constant (add_suffix ind.ind_name "_EqDec") (DefinitionEntry ce, IsDefinition Instance) in
+ Typeclasses.add_instance (Typeclasses.new_instance cl None true (ConstRef inst)))
+ indsl
in
Lemmas.start_proof_with_initialization
(Global, Proof Lemma)
(Some (false, possible_guards, None))
- (List.map (fun ind -> add_suffix ind.ind_name "_eqdec", (stmt_of ind, ([], []))) indsl)
- None
- (fun l gr -> ())
+ (List.map (fun (ind, (stmt, tc)) -> add_suffix ind.ind_name "_eqdec", (stmt, ([], []))) indsl)
+ None hook
(* let impl = *)
(* let xname = Name (id_of_string "x") in *)
@@ -283,7 +299,7 @@ VERNAC COMMAND EXTEND Derive_EqDec
let c' = Constrintern.interp_constr Evd.empty (Global.env ()) c in
match kind_of_term c' with
| Ind i -> derive_eq_dec i
- | _ -> error "Expected an inductive type")
+ | _ -> Errors.error "Expected an inductive type")
c
]
END
View
@@ -14,6 +14,7 @@
open Cases
open Util
+open Errors
open Names
open Nameops
open Term
@@ -526,7 +527,7 @@ let rels_above ctx x =
let is_fix_proto t =
match kind_of_term t with
- | App (f, args) when eq_constr f (delayed_force Subtac_utils.fix_proto) ->
+ | App (f, args) when eq_constr f (Lazy.force coq_fix_proto) ->
true
| _ -> false
@@ -809,7 +810,7 @@ let interp_constr_in_rhs env ctx evars (i,comp,impls) ty s lets c =
(push_rel_context ctx env) ~impls c
in
let c' = substnl pats 0 c in
- evars := Typeclasses.resolve_typeclasses ~onlyargs:false env !evars;
+ evars := Typeclasses.resolve_typeclasses ~with_goals:true env !evars;
let c' = nf_evar !evars c' in
c', Typing.type_of envctx !evars c'
@@ -819,7 +820,7 @@ let interp_constr_in_rhs env ctx evars (i,comp,impls) ty s lets c =
let c, _ = interp_casted_constr_evars_impls ~evdref:evars ~fail_evar:false
(push_rel_context ctx env) ~impls c ty'
in
- evars := Typeclasses.resolve_typeclasses ~onlyargs:false env !evars;
+ evars := Typeclasses.resolve_typeclasses ~with_goals:true env !evars;
let c' = nf_evar !evars (substnl pats 0 c) in
c', nf_evar !evars (substnl pats 0 ty')
@@ -1794,7 +1795,7 @@ let ind_fun_tac is_rec f info fid split ind =
[fix (Some recid) (succ i);
onLastDecl (fun (n,b,t) gl ->
let sort = pf_type_of gl t in
- let fixprot = mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|]) in
+ let fixprot = mkApp (Lazy.force coq_fix_proto, [|sort; t|]) in
change_in_hyp None fixprot (n, InHyp) gl);
intros; aux_ind_fun info split])
else tclCOMPLETE (tclTHEN intros (aux_ind_fun info split))
@@ -2256,7 +2257,7 @@ let build_equations with_ind env id info data sign is_rec arity cst
in
try
(* Conv_oracle.set_strategy (ConstKey cst) Conv_oracle.Expand; *)
- ignore(Subtac_obligations.add_definition (add_suffix id "_elim")
+ ignore(Obligations.add_definition (add_suffix id "_elim")
~tactic:(ind_elim_tac (constr_of_global elim) leninds info)
~hook:hookelim newty [||])
with e ->
@@ -2270,7 +2271,7 @@ let build_equations with_ind env id info data sign is_rec arity cst
let instid = add_prefix "FunctionalInduction_" id in
ignore(declare_instance instid [] cl args)
in
- try ignore(Subtac_obligations.add_definition ~hook:hookind
+ try ignore(Obligations.add_definition ~hook:hookind
indid statement ~tactic:(ind_fun_tac is_rec f info id split ind) [||])
with e ->
warn (str "Induction principle could not be proved automatically: " ++ fnl () ++
@@ -2296,7 +2297,7 @@ let build_equations with_ind env id info data sign is_rec arity cst
Conv_oracle.set_strategy (ConstKey cst) Conv_oracle.Opaque;
if with_ind && succ j = List.length ind_stmts then declare_ind ())
in
- ignore(Subtac_obligations.add_definition
+ ignore(Obligations.add_definition
ideq c ~tactic:(tclTHENLIST [intros; unf; solve_equation_tac (ConstRef cst) []]) ~hook [||])
in iter proof stmts
in iter proof ind_stmts
@@ -2328,9 +2329,8 @@ let hintdb_set_transparency cst b db =
let define_tree is_recursive impls status isevar env (i, sign, arity) comp ann split hook =
let _ = isevar := Evarutil.nf_evar_map_undefined !isevar in
let helpers, oblevs, t, ty = term_of_tree status isevar env (i, sign, arity) ann split in
- let undef = undefined_evars !isevar in
let obls, (emap, cmap), t', ty' =
- Eterm.eterm_obligations env i !isevar undef 0 ~status t (whd_betalet !isevar ty)
+ Obligations.eterm_obligations env i !isevar 0 ~status t (whd_betalet !isevar ty)
in
let obls =
Array.map (fun (id, ty, loc, s, d, t) ->
@@ -2339,18 +2339,18 @@ let define_tree is_recursive impls status isevar env (i, sign, arity) comp ann s
then Some (equations_tac ())
else if is_comp_obl comp (snd loc) then
Some (tclTRY (solve_rec_tac ()))
- else Some (snd (Subtac_obligations.get_default_tactic ()))
+ else Some (snd (Obligations.get_default_tactic ()))
in (id, ty, loc, s, d, tac)) obls
in
let term_info = map (fun (ev, arg) ->
(ev, arg, List.assoc ev emap)) helpers
in
let hook = hook cmap term_info in
if is_recursive = Some Structural then
- ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
- ~hook (Subtac_obligations.IsFixpoint [None, CStructRec]))
+ ignore(Obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
+ ~hook (Obligations.IsFixpoint [None, CStructRec]))
else
- ignore(Subtac_obligations.add_definition ~hook
+ ignore(Obligations.add_definition ~hook
~implicits:impls i ~term:t' ty' obls)
let conv_proj_call proj f_cst c =
@@ -2680,7 +2680,7 @@ let define_by_eqs opts i (l,ann) t nt eqs =
env Constrintern.Recursive [i] [ty] [impls]
in
let sort = Retyping.get_type_of env !isevar ty in
- let fixprot = mkApp (delayed_force Subtac_utils.fix_proto, [|sort; ty|]) in
+ let fixprot = mkApp (Lazy.force coq_fix_proto, [|sort; ty|]) in
let fixdecls = [(Name i, None, fixprot)] in
let is_recursive =
let rec occur_eqn (_, _, rhs) =
@@ -2723,7 +2723,7 @@ let define_by_eqs opts i (l,ann) t nt eqs =
let status = (* if is_recursive then Expand else *) Define false in
let baseid = string_of_id i in
let (ids, csts) = full_transparent_state in
- let fix_proto_ref = destConstRef (global_of_constr (Subtac_utils.fix_proto ())) in
+ let fix_proto_ref = destConstRef (global_of_constr (Lazy.force coq_fix_proto)) in
Auto.create_hint_db false baseid (ids, Cpred.remove fix_proto_ref csts) true;
let hook cmap helpers subst gr =
let info = { base_id = baseid; helpers_info = helpers } in
@@ -2766,7 +2766,7 @@ let define_by_eqs opts i (l,ann) t nt eqs =
in
let tac = prove_unfolding_lemma info (mkConst r.comp_proj) f_cst funf_cst unfold_split in
let unfold_eq_id = add_suffix unfoldi "_eq" in
- ignore(Subtac_obligations.add_definition ~hook:hook_eqs ~reduce:(fun x -> x)
+ ignore(Obligations.add_definition ~hook:hook_eqs ~reduce:(fun x -> x)
~implicits:impls unfold_eq_id stmt ~tactic:tac [||])
in
define_tree None impls status isevar env (unfoldi, sign, arity) None ann unfold_split hook_unfold
@@ -2872,35 +2872,35 @@ type 'a deppat_equations_argtype = (pre_equation list, 'a) Genarg.abstract_argum
let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype),
(globwit_deppat_equations : Genarg.glevel deppat_equations_argtype),
(rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) =
- Genarg.create_arg "deppat_equations"
+ Genarg.create_arg None "deppat_equations"
type 'a equation_options_argtype = ((equation_option * bool) list, 'a) Genarg.abstract_argument_type
let (wit_equation_options : Genarg.tlevel equation_options_argtype),
(globwit_equation_options : Genarg.glevel equation_options_argtype),
(rawwit_equation_options : Genarg.rlevel equation_options_argtype) =
- Genarg.create_arg "equation_options"
+ Genarg.create_arg None "equation_options"
type 'a binders_let2_argtype = (local_binder list * (identifier located option * recursion_order_expr), 'a) Genarg.abstract_argument_type
let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
(globwit_binders_let2 : Genarg.glevel binders_let2_argtype),
(rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) =
- Genarg.create_arg "binders_let2"
+ Genarg.create_arg None "binders_let2"
type 'a decl_notation_argtype = (Vernacexpr.decl_notation option, 'a) Genarg.abstract_argument_type
let (wit_decl_notation : Genarg.tlevel decl_notation_argtype),
(globwit_decl_notation : Genarg.glevel decl_notation_argtype),
(rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) =
- Genarg.create_arg "decl_notation"
+ Genarg.create_arg None "decl_notation"
type 'a identref_argtype = (identifier located, 'a) Genarg.abstract_argument_type
let (wit_identref : Genarg.tlevel identref_argtype),
(globwit_identref : Genarg.glevel identref_argtype),
(rawwit_identref : Genarg.rlevel identref_argtype) =
- Genarg.create_arg "identref"
+ Genarg.create_arg None "identref"
let with_rollback f x =
States.with_heavy_rollback f
@@ -3208,7 +3208,7 @@ let derive_no_confusion ind =
Typeclasses.add_instance (Typeclasses.new_instance tc None true (ConstRef inst))
| None -> error "Could not find constructor"
in
- ignore(Subtac_obligations.add_definition ~hook noid
+ ignore(Obligations.add_definition ~hook noid
stmt ~tactic:(noconf_tac ()) [||])
View
@@ -91,6 +91,8 @@ let coq_tt = lazy (init_constant ["Coq";"Init";"Datatypes"] "tt")
let coq_prod = lazy (init_constant ["Coq";"Init";"Datatypes"] "prod")
let coq_pair = lazy (init_constant ["Coq";"Init";"Datatypes"] "pair")
+let coq_fix_proto = lazy (init_constant ["Coq";"Program";"Tactics"] "fix_proto")
+
let fresh_id_in_env avoid id env =
Namegen.next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env))
@@ -328,7 +330,7 @@ let autounfold_first db cl gl =
let st =
List.fold_left (fun (i,c) dbname ->
let db = try searchtable_map dbname
- with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ with Not_found -> Errors.errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
in
let (ids, csts) = Hint_db.unfolds db in
(Idset.union ids i, Cset.union csts c)) (Idset.empty, Cset.empty) db
View
@@ -176,7 +176,7 @@ let declare_sig_of_ind env ind =
let lenpars = mib.mind_nparams_rec in
let lenargs = List.length ctx - lenpars in
if lenargs = 0 then
- user_err_loc (dummy_loc, "Derive Signature",
+ Errors.user_err_loc (dummy_loc, "Derive Signature",
str"No signature to derive for non-dependent inductive types");
let args, pars = list_chop lenargs ctx in
let parapp = mkApp (mkInd ind, extended_rel_vect 0 pars) in
@@ -213,7 +213,7 @@ VERNAC COMMAND EXTEND Derive_Signature
let c' = Constrintern.interp_constr Evd.empty (Global.env ()) c in
match kind_of_term c' with
| Ind i -> ignore(declare_sig_of_ind (Global.env ()) i)
- | _ -> error "Expected an inductive type"
+ | _ -> Errors.error "Expected an inductive type"
]
END
View
@@ -229,8 +229,8 @@ let derive_subterm ind =
let inst = Typeclasses.new_instance kl None global (ConstRef cst) in
Typeclasses.add_instance inst
in
- let obls, _, constr, typ = Eterm.eterm_obligations env id !evm !evm 0 body ty in
- Subtac_obligations.add_definition id ~term:constr typ
+ let obls, _, constr, typ = Obligations.eterm_obligations env id !evm 0 body ty in
+ Obligations.add_definition id ~term:constr typ
~kind:(Decl_kinds.Global,Decl_kinds.Instance)
~hook ~tactic:(solve_subterm_tac ()) obls
in ignore(declare_ind ())
@@ -240,7 +240,7 @@ VERNAC COMMAND EXTEND Derive_Subterm
let c' = Constrintern.interp_constr Evd.empty (Global.env ()) c in
match kind_of_term c' with
| Ind i -> derive_subterm i
- | _ -> error "Expected an inductive type"
+ | _ -> Errors.error "Expected an inductive type"
]
END
@@ -359,6 +359,6 @@ VERNAC COMMAND EXTEND Derive_Below
let c' = Constrintern.interp_constr Evd.empty (Global.env ()) c in
match kind_of_term c' with
| Ind i -> derive_below i
- | _ -> error "Expected an inductive type"
+ | _ -> Errors.error "Expected an inductive type"
]
END
View
@@ -16,27 +16,18 @@ Module RecRel.
End RecRel.
-Definition gt_bound n : relation nat :=
- fun x y => x > y /\ x < n.
+Definition measure {A B} (f : A -> B) (R : relation B) : relation A :=
+ fun x y => R (f x) (f y).
-Definition minus_12 n :=
- if le_lt_dec n 100 then n - 12 else n.
+Definition f91_rel : relation nat :=
+ measure (fun x => 101 - x) lt.
-Instance gt_bound_wf n : WellFounded (gt_bound n).
+Instance gt_bound_wf : WellFounded f91_rel.
Proof. red. red. intros.
Admitted.
-Equations foo (n : nat) : Prop :=
-foo n by rec n (gt_bound 100) :=
-foo n := _.
-
-Admit Obligations.
-
-
-Set Printing Existential Instances.
-
-Equations f91 n : { m : nat | n < m - 11 } :=
-f91 n by rec n (gt_bound 100) :=
+Equations f91 n : { m : nat | if le_lt_dec n 100 then m = 91 else m = n - 10 } :=
+f91 n by rec n f91_rel :=
f91 n with le_lt_dec n 100 := {
| left H := exist _ (proj1_sig (f91 (proj1_sig (f91 (n + 11))))) _ ;
| right H := exist _ (n - 10) _ }.
@@ -46,18 +37,33 @@ Admit Obligations.
Admit Obligations.
*)
-Next Obligation. intros. apply f91. red. admit. Defined.
-Next Obligation. intros. apply f91. destruct f91_comp_proj. simpl. red. simpl. admit. Defined.
-Next Obligation. intros. admit. Defined.
-Next Obligation. intros. admit. Defined.
+Require Import Omega.
-Next Obligation. intros. rec_wf_rel n IH (gt_bound 100).
- simp f91. Print f91_ind. constructor. destruct le_lt_dec. simpl. constructor. intros. apply IH. admit.
- apply IH. admit. apply IH. admit. intros. apply IH; auto.
- simpl. constructor. intros. apply IH; auto.
+Next Obligation. intros. apply f91. do 2 red. try omega. Defined.
+Next Obligation. intros. apply f91. destruct f91_comp_proj. simpl. do 2 red.
+ destruct_call le_lt_dec. subst. omega. subst. omega.
Defined.
+
+Next Obligation. destruct le_lt_dec. intros. destruct_call f91_comp_proj. simpl.
+ destruct_call f91_comp_proj. simpl in *. destruct le_lt_dec. subst. simpl in y. auto.
+ subst x0. destruct le_lt_dec. auto.
+ subst x. simpl. omega.
+
+ elimtype False. omega.
+Qed.
-About f91_elim. Print f91_ind.
+Next Obligation. destruct le_lt_dec. intros. omega. omega. Defined.
+Obligation Tactic := idtac.
+Next Obligation. equations. Defined.
+
+Next Obligation. intros. rec_wf_rel n IH f91_rel.
+ simp f91. Print f91_ind. constructor. destruct le_lt_dec. simpl. constructor. intros. apply IH.
+ admit.
+ apply IH. admit.
+ apply IH. admit.
+ intros. subst recres. apply IH. assumption.
+ simp f91.
+Defined.
Section Nested.
Hint Extern 3 => match goal with
Oops, something went wrong.

0 comments on commit f90c86d

Please sign in to comment.