aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--interp/constrintern.ml6
-rw-r--r--interp/topconstr.ml21
-rw-r--r--interp/topconstr.mli16
-rw-r--r--lib/flags.ml2
-rw-r--r--parsing/g_constr.ml419
-rw-r--r--parsing/g_vernac.ml429
-rw-r--r--parsing/ppvernac.ml98
-rw-r--r--plugins/funind/indfun.ml3
-rw-r--r--plugins/interface/xlate.ml8
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_command.ml14
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml2
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/termops.ml2
-rw-r--r--pretyping/termops.mli2
-rw-r--r--proofs/pfedit.ml6
-rw-r--r--proofs/pfedit.mli9
-rw-r--r--test-suite/success/Fixpoint.v41
-rw-r--r--theories/Arith/Compare_dec.v16
-rw-r--r--theories/Classes/Morphisms.v2
-rw-r--r--toplevel/command.ml127
-rw-r--r--toplevel/command.mli19
-rw-r--r--toplevel/lemmas.ml147
-rw-r--r--toplevel/lemmas.mli13
-rw-r--r--toplevel/vernacentries.ml4
-rw-r--r--toplevel/vernacexpr.ml8
28 files changed, 374 insertions, 252 deletions
diff --git a/CHANGES b/CHANGES
index b6744e25d..627408cc8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -42,6 +42,9 @@ Tactics
- A new tactic name "exfalso" for the use of 'ex-falso quodlibet' principle.
This tactic is simply a shortcut for "elimtype False".
- Added support for Leibniz-rewriting of dependent hypotheses.
+- Binders given before ":" in lemmas are now automatically
+ introduced in the context (possible source of incompatibility that can be
+ avoided by unsetting option "Automatic Introduction").
Tactic Language
@@ -75,6 +78,7 @@ Vernacular commands
- Made support for automatic generation of case analysis schemes and
congruence schemes available to user (governed by options "Unset
Case Analysis Schemes" and "Unset Congruence Schemes").
+- Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
Tools
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 85f84b850..e819e7009 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1048,11 +1048,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
let intern_ro_arg f =
- let idx =
- match n with
- Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
- | None -> 0
- in
+ let idx = Option.default 0 (index_of_annot bl n) in
let before, after = list_chop idx bl in
let ((ids',_,_,_) as env',rbefore) =
List.fold_left intern_local_binder (env,[]) before in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a6b4b1b0a..ecb61e15b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -639,8 +639,8 @@ type cases_pattern_expr =
type constr_expr =
| CRef of reference
- | CFix of loc * identifier located * fixpoint_expr list
- | CCoFix of loc * identifier located * cofixpoint_expr list
+ | CFix of loc * identifier located * fix_expr list
+ | CCoFix of loc * identifier located * cofix_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
@@ -667,7 +667,7 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-and fixpoint_expr =
+and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
@@ -678,7 +678,7 @@ and typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
-and cofixpoint_expr =
+and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
@@ -918,6 +918,19 @@ let coerce_to_name = function
(constr_loc a,"coerce_to_name",
str "This expression should be a name.")
+(* Interpret the index of a recursion order annotation *)
+
+let index_of_annot bl na =
+ let names = List.map snd (names_of_local_assums bl) in
+ match na with
+ | None ->
+ if names = [] then error "A fixpoint needs at least one parameter."
+ else None
+ | Some (loc, id) ->
+ try Some (list_index0 (Name id) names)
+ with Not_found ->
+ user_err_loc(loc,"",
+ str "No parameter named " ++ Nameops.pr_id id ++ str".")
(* Used in correctness and interface *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1c0b207ea..b7e389d6b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,8 +125,8 @@ type cases_pattern_expr =
type constr_expr =
| CRef of reference
- | CFix of loc * identifier located * fixpoint_expr list
- | CCoFix of loc * identifier located * cofixpoint_expr list
+ | CFix of loc * identifier located * fix_expr list
+ | CCoFix of loc * identifier located * cofix_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
@@ -153,10 +153,10 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-and fixpoint_expr =
+and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
-and cofixpoint_expr =
+and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
@@ -205,6 +205,8 @@ val coerce_reference_to_id : reference -> identifier
val coerce_to_id : constr_expr -> identifier located
val coerce_to_name : constr_expr -> name located
+val index_of_annot : local_binder list -> identifier located option -> int option
+
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
@@ -220,12 +222,12 @@ val local_binders_length : local_binder list -> int
(* Excludes let binders *)
val local_assums_length : local_binder list -> int
-(* Does not take let binders into account *)
-val names_of_local_assums : local_binder list -> name located list
-
(* With let binders *)
val names_of_local_binders : local_binder list -> name located list
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
(* Used in typeclasses *)
val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
diff --git a/lib/flags.ml b/lib/flags.ml
index 971b560ec..555739b11 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -65,7 +65,7 @@ let if_verbose f x = if not !silent then f x
let auto_intros = ref false
let make_auto_intros flag = auto_intros := flag
-let is_auto_intros () = !auto_intros
+let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
let hash_cons_proofs = ref true
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 669d1f2ae..393125e29 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -10,6 +10,7 @@
(* $Id$ *)
+open Pp
open Pcoq
open Constr
open Prim
@@ -43,21 +44,11 @@ let binders_of_lidents l =
LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
CHole (loc, Some (Evd.BinderType (Name id))))) l
-let rec index_and_rec_order_of_annot loc bl ann =
- match names_of_local_assums bl,ann with
- | [loc,Name id], (None, r) -> Some (loc, id), r
- | lids, (Some (loc, n), ro) ->
- if List.exists (fun (_, x) -> x = Name n) lids then
- Some (loc, n), ro
- else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.")
- | _, (None, r) -> None, r
-
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
- let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
let ty = match tyc with
Some ty -> ty
| None -> CHole (loc, None) in
- (id,(n,ro),bl,ty,body)
+ (id,ann,bl,ty,body)
let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
let _ = Option.map (fun (aloc,_) ->
@@ -308,7 +299,8 @@ GEXTEND Gram
;
fix_decl:
[ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
- c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ]
+ c=operconstr LEVEL "200" ->
+ (id,fst bl,snd bl,c,ty) ] ]
;
match_constr:
[ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
@@ -402,8 +394,7 @@ GEXTEND Gram
[ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
(assum (loc, Name id) :: fst bl), snd bl
| f = fixannot -> [], f
- | b = binder_let; bl = binders_let_fixannot ->
- b @ fst bl, snd bl
+ | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
| -> [], (None, CStructRec)
] ]
;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 56946ef27..54cf671cc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -129,8 +129,8 @@ GEXTEND Gram
[ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
l = LIST0
[ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
- (Some id,(bl,c)) ] ->
- VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
+ (Some id,(bl,c,None)) ] ->
+ VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
| stre = assumption_token; nl = inline; bl = assum_list ->
VernacAssumption (stre, nl, bl)
| stre = assumptions_token; nl = inline; bl = assum_list ->
@@ -275,29 +275,12 @@ GEXTEND Gram
[ [ id = identref;
bl = binders_let_fixannot;
ty = type_cstr;
- ":="; def = lconstr; ntn = decl_notation ->
- let bl, annot = bl in
- let names = names_of_local_assums bl in
- let ni =
- match fst annot with
- Some (loc, id) ->
- (if List.exists (fun (_, id') -> Name id = id') names then
- Some (loc, id)
- else Util.user_err_loc
- (loc,"Fixpoint",
- str "No argument named " ++ Nameops.pr_id id ++ str"."))
- | None ->
- (* If there is only one argument, it is the recursive one,
- otherwise, we search the recursive index later *)
- match names with
- | [(loc, Name na)] -> Some (loc, na)
- | _ -> None
- in
- ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
+ def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
+ let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = identref; bl = binders_let; ty = type_cstr; ":=";
- def = lconstr; ntn = decl_notation ->
+ [ [ id = identref; bl = binders_let; ty = type_cstr;
+ def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
type_cstr:
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 190271159..4f31607aa 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -302,6 +302,28 @@ let pr_binders_arg =
let pr_and_type_binders_arg bl =
pr_binders_arg bl
+let names_of_binder = function
+ | LocalRawAssum (nal,_,_) -> nal
+ | LocalRawDef (_,_) -> []
+
+let pr_guard_annot bl (n,ro) =
+ match n with
+ | None -> mt ()
+ | Some (loc, id) ->
+ match (ro : Topconstr.recursion_order_expr) with
+ | CStructRec ->
+ let ids = List.flatten (List.map names_of_binder bl) in
+ if List.length ids > 1 then
+ spc() ++ str "{struct " ++ pr_id id ++ str"}"
+ else mt()
+ | CWfRec c ->
+ spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
+ pr_id id ++ str"}"
+ | CMeasureRec (m,r) ->
+ spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
+ pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
+ pr_lconstr_expr r) ++ str"}"
+
let pr_onescheme (idop,schem) =
match schem with
| InductionScheme (dep,ind,s) ->
@@ -409,6 +431,14 @@ let pr_paren_reln_or_extern = function
| Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
| _ -> mt()
+let pr_statement head (id,(bl,c,guard)) =
+ assert (id<>None);
+ hov 0
+ (head ++ pr_lident (Option.get id) ++ spc() ++
+ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+ pr_opt (pr_guard_annot bl) guard ++
+ str":" ++ pr_spc_lconstr c)
+
(**************************************)
(* Pretty printer for vernac commands *)
(**************************************)
@@ -567,11 +597,6 @@ let rec pr_vernac = function
| Some cc -> str" :=" ++ spc() ++ cc))
| VernacStartTheoremProof (ki,l,_,_) ->
- let pr_statement head (id,(bl,c)) =
- hov 0
- (head ++ pr_opt pr_lident id ++ spc() ++
- (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
- str":" ++ pr_spc_lconstr c) in
hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
prlist (pr_statement (spc () ++ str "with")) (List.tl l))
@@ -605,75 +630,46 @@ let rec pr_vernac = function
spc() ++
pr_record_decl b c fs in
let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
- let kw =
- str (match k with Record -> "Record" | Structure -> "Structure"
- | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
- | Class b -> if b then "Definitional Class" else "Class")
- in
- hov 0 (
- kw ++ spc() ++
- (if i then str"Infer" else str"") ++
- (if coe then str" > " else str" ") ++ pr_lident id ++
+ hov 0 (
+ str key ++ spc() ++
+ (if i then str"Infer " else str"") ++
+ (if coe then str"> " else str"") ++ pr_lident id ++
pr_and_type_binders_arg indpar ++ spc() ++
Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
str" :=") ++ pr_constructor_list k lc ++
prlist (pr_decl_notation pr_constr) ntn
in
- hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
- ++
+ let key =
+ let (_,_,_,k,_),_ = List.hd l in
+ match k with Record -> "Record" | Structure -> "Structure"
+ | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+ | Class b -> if b then "Definitional Class" else "Class" in
+ hov 1 (pr_oneind key (List.hd l)) ++
(prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
| VernacFixpoint (recs,b) ->
- let name_of_binder = function
- | LocalRawAssum (nal,_,_) -> nal
- | LocalRawDef (_,_) -> [] in
let pr_onerec = function
- | ((loc,id),(n,ro),bl,type_,def),ntn ->
- let (bl',def,type_) =
- if Flags.do_beautify() then extract_def_binders def type_
- else ([],def,type_) in
- let bl = bl @ bl' in
- let ids = List.flatten (List.map name_of_binder bl) in
- let annot =
- match n with
- | None -> mt ()
- | Some (loc, id) ->
- match (ro : Topconstr.recursion_order_expr) with
- CStructRec ->
- if List.length ids > 1 then
- spc() ++ str "{struct " ++ pr_id id ++ str"}"
- else mt()
- | CWfRec c ->
- spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
- pr_id id ++ str"}"
- | CMeasureRec (m,r) ->
- spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
- pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
- pr_lconstr_expr r) ++ str"}"
- in
+ | ((loc,id),ro,bl,type_,def),ntn ->
+ let annot = pr_guard_annot bl ro in
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
- ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++
+ ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
prlist (pr_decl_notation pr_constr) ntn
in
let start = if b then "Boxed Fixpoint" else "Fixpoint" in
- hov 1 (str start ++ spc() ++
- prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
+ hov 0 (str start ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
| VernacCoFixpoint (corecs,b) ->
let pr_onecorec (((loc,id),bl,c,def),ntn) =
- let (bl',def,c) =
- if Flags.do_beautify() then extract_def_binders def c
- else ([],def,c) in
- let bl = bl @ bl' in
pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
spc() ++ pr_lconstr_expr c ++
- str" :=" ++ brk(1,1) ++ pr_lconstr def ++
+ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
prlist (pr_decl_notation pr_constr) ntn
in
let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
- hov 1 (str start ++ spc() ++
+ hov 0 (str start ++ spc() ++
prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
| VernacScheme l ->
hov 2 (str"Scheme" ++ spc() ++
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bd3f7e8ec..781a841c9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -372,6 +372,9 @@ let register_struct is_rec fixpoint_exprl =
fname (Decl_kinds.Global,Decl_kinds.Definition)
ce imps (fun _ _ -> ())
| _ ->
+ let fixpoint_exprl =
+ List.map (fun ((name,annot,bl,types,body),ntn) ->
+ ((name,annot,bl,types,Some body),ntn)) fixpoint_exprl in
Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
let generate_correction_proof_wf f_ref tcc_lemma_ref
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 9ba1d6715..5f3b6b28d 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1917,7 +1917,7 @@ let rec xlate_vernac =
| VernacBeginSection (_,id) ->
CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
| VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
- | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
+ | VernacStartTheoremProof (k, [Some (_,s), (bl,c,None)], _, _) ->
CT_coerce_THEOREM_GOAL_to_COMMAND(
CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
xlate_binder_list bl, xlate_formula c))
@@ -1993,9 +1993,10 @@ let rec xlate_vernac =
| VernacFixpoint ([],_) -> xlate_error "mutual recursive"
| VernacFixpoint ((lm :: lmi),boxed) ->
let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) =
+ if ardef = None then xlate_error "Fixpoint proved by tactics";
let struct_arg = make_fix_struct (n, bl) in
let arf = xlate_formula arf in
- let ardef = xlate_formula ardef in
+ let ardef = xlate_formula (Option.get ardef) in
match xlate_binder_list bl with
| CT_binder_list (b :: bl) ->
CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
@@ -2006,8 +2007,9 @@ let rec xlate_vernac =
| VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
| VernacCoFixpoint ((lm :: lmi),boxed) ->
let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) =
+ if ardef = None then xlate_error "Fixpoint proved by tactics";
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
- xlate_formula arf, xlate_formula ardef) in
+ xlate_formula arf, xlate_formula (Option.get ardef)) in
CT_cofix_decl
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
| VernacScheme [] -> xlate_error "induction scheme"
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 2db253373..b337d3352 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -152,7 +152,9 @@ let subtac (loc, command) =
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
- | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
+ | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
+ if guard <> None then
+ error "Do not support building theorems as a fixpoint.";
Dumpglob.dump_definition id false "prf";
if not(Pfedit.refining ()) then
if lettop then
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index c63e8488b..dc57e4aad 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -365,8 +365,8 @@ let interp_fix_ccl evdref (env,_) fix =
let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
let env = push_rel_context ctx env_rec in
- let body = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in
- it_mkLambda_or_LetIn body ctx
+ let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in
+ Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
@@ -416,6 +416,10 @@ let check_evars env initial_sigma evd c =
| _ -> iter_constr proc_rec c
in proc_rec c
+let out_def = function
+ | Some def -> def
+ | None -> error "Program Fixpoint needs defined bodies."
+
let interp_recursive fixkind l boxed =
let env = Global.env() in
let fixl, ntnl = List.split l in
@@ -452,6 +456,8 @@ let interp_recursive fixkind l boxed =
list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
() in
+ let fixdefs = List.map out_def fixdefs in
+
(* Instantiate evars and check all are resolved *)
let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
let evd = Typeclasses.resolve_typeclasses
@@ -507,14 +513,14 @@ let build_recursive l b =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
- ignore(build_wellfounded (id, n, bl, typ, def) r
+ ignore(build_wellfounded (id, n, bl, typ, out_def def) r
(match n with Some n -> mkIdentC (snd n) | None ->
errorlabstrm "Subtac_command.build_recursive"
(str "Recursive argument required for well-founded fixpoints"))
ntn false)
| [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
- ignore(build_wellfounded (id, n, bl, typ, def) (Option.default (CRef lt_ref) r)
+ ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
m ntn false)
| _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 3e275cd0f..7d1f2cd62 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -110,7 +110,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let pretype_id loc env (lvar,unbndltacvars) id =
let id = strip_meta id in (* May happen in tactics defined by Grammar *)
try
- let (n,typ) = lookup_rel_id id (rel_context env) in
+ let (n,_,typ) = lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
try
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ae7106fb3..177389c98 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1316,7 +1316,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
(* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
(* \--env-/ (= x:ty) *)
(* \--------------extenv------------/ *)
- let (p,_) = lookup_rel_id x (rel_context extenv) in
+ let (p,_,_) = lookup_rel_id x (rel_context extenv) in
let rec aux n (_,b,ty) =
match b with
| Some c ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 10d9a1c4e..288eb9da2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -230,7 +230,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let pretype_id loc env (lvar,unbndltacvars) id =
try
- let (n,typ) = lookup_rel_id id (rel_context env) in
+ let (n,_,typ) = lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
try
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 81c740580..4de4bde2c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -221,7 +221,7 @@ let push_named_rec_types (lna,typarray,_) env =
let rec lookup_rel_id id sign =
let rec lookrec = function
| (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
- | (n, (Name id',_,t)::l) -> if id' = id then (n,t) else lookrec (n+1,l)
+ | (n, (Name id',b,t)::l) -> if id' = id then (n,b,t) else lookrec (n+1,l)
| (_, []) -> raise Not_found
in
lookrec (1,sign)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 7f9ccb28e..59f7750d3 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -39,7 +39,7 @@ val print_env : env -> std_ppcmds
val push_rel_assum : name * types -> env -> env
val push_rels_assum : (name * types) list -> env -> env
val push_named_rec_types : name array * types array * 'a -> env -> env
-val lookup_rel_id : identifier -> rel_context -> int * types
+val lookup_rel_id : identifier -> rel_context -> int * constr option * types
(* builds argument lists matching a block of binders or a context *)
val rel_vect : int -> int -> constr array
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7895bfac9..f3658ad4b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -31,10 +31,12 @@ open Safe_typing
(* Mainly contributed by C. Murthy *)
(*********************************************************************)
+type lemma_possible_guards = int list list
+
type proof_topstate = {
mutable top_end_tac : tactic option;
top_init_tac : tactic option;
- top_compute_guard : bool;
+ top_compute_guard : lemma_possible_guards;
top_goal : goal;
top_strength : Decl_kinds.goal_kind;
top_hook : declaration_hook }
@@ -252,7 +254,7 @@ let set_end_tac tac =
(* Modifying the current prooftree *)
(*********************************************************************)
-let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
+let start_proof na str sign concl ?init_tac ?(compute_guard=[]) hook =
let top_goal = mk_goal sign concl None in
let ts = {
top_end_tac = None;
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6acf1ff78..acb852471 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -78,9 +78,12 @@ val get_undo : unit -> int option
systematically apply at initialization time (e.g. to start the
proof of mutually dependent theorems) *)
+type lemma_possible_guards = int list list
+
val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
- ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
+ ?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
+ declaration_hook -> unit
(* [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
@@ -108,7 +111,9 @@ val suspend_proof : unit -> unit
it also tells if the guardness condition has to be inferred. *)
val cook_proof : (Refiner.pftreestate -> unit) ->
- identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
+ identifier *
+ (Entries.definition_entry * lemma_possible_guards * goal_kind *
+ declaration_hook)
(* To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 4130a16ca..fcf8d8d4a 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -48,3 +48,44 @@ Fixpoint foldrn n bs :=
End folding.
+(* Check definition by tactics *)
+
+Inductive even : nat -> Type :=
+ | even_O : even 0
+ | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Type :=
+ odd_S : forall n, even n -> odd (S n).
+
+Fixpoint even_div2 n (H:even n) : nat :=
+ match H with
+ | even_O => 0
+ | even_S n H => S (odd_div2 n H)
+ end
+with odd_div2 n H : nat.
+destruct H.
+apply even_div2 with n.
+assumption.
+Qed.
+
+Fixpoint even_div2' n (H:even n) : nat with odd_div2' n (H:odd n) : nat.
+destruct H.
+exact 0.
+apply odd_div2' with n.
+assumption.
+destruct H.
+apply even_div2' with n.
+assumption.
+Qed.
+
+CoInductive Stream1 (A B:Type) := Cons1 : A -> Stream2 A B -> Stream1 A B
+with Stream2 (A B:Type) := Cons2 : B -> Stream1 A B -> Stream2 A B.
+
+CoFixpoint ex1 (n:nat) (b:bool) : Stream1 nat bool
+with ex2 (n:nat) (b:bool) : Stream2 nat bool.
+apply Cons1.
+exact n.
+apply (ex2 n b).
+apply Cons2.
+exact b.
+apply (ex1 (S n) (negb b)).
+Defined.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index deb6f229b..d696360fd 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -22,17 +22,17 @@ Definition zerop n : {n = 0} + {0 < n}.
Defined.
Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
- induction n; simple destruct m; auto with arith.
- intros m0; elim (IHn m0); auto with arith.
- induction 1; auto with arith.
+ intros; induction n in m |- *; destruct m; auto with arith.
+ destruct (IHn m) as [H|H]; auto with arith.
+ destruct H; auto with arith.
Defined.
Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
- exact lt_eq_lt_dec.
+ intros; apply lt_eq_lt_dec; assumption.
Defined.
Definition le_lt_dec n m : {n <= m} + {m < n}.
- induction n.
+ intros; induction n in m |- *.
auto with arith.
destruct m.
auto with arith.
@@ -40,7 +40,7 @@ Definition le_lt_dec n m : {n <= m} + {m < n}.
Defined.
Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
- exact le_lt_dec.
+ intros; exact (le_lt_dec n m).
Defined.
Definition le_ge_dec n m : {n <= m} + {n >= m}.
@@ -48,11 +48,11 @@ Definition le_ge_dec n m : {n <= m} + {n >= m}.
Defined.
Definition le_gt_dec n m : {n <= m} + {n > m}.
- exact le_lt_dec.
+ intros; exact (le_lt_dec n m).
Defined.
Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
- intros; elim (lt_eq_lt_dec n m); auto with arith.
+ intros; destruct (lt_eq_lt_dec n m); auto with arith.
intros; absurd (m < n); auto with arith.
Defined.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f5d08edb4..f66fa87b6 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -406,7 +406,7 @@ Qed.
Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
-Proof. unfold Normalizes. intros.
+Proof. unfold Normalizes in *. intros.
rewrite NA, NB. firstorder.
Qed.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d59b16d82..50cc702e2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -446,7 +446,7 @@ let check_mutuality env isfix fixl =
type structured_fixpoint_expr = {
fix_name : identifier;
fix_binders : local_binder list;
- fix_body : constr_expr;
+ fix_body : constr_expr option;
fix_type : constr_expr
}
@@ -457,9 +457,10 @@ let interp_fix_ccl evdref (env,_) fix =
interp_type_evars evdref env fix.fix_type
let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
- let env = push_rel_context ctx env_rec in
- let body = interp_casted_constr_evars evdref env ~impls fix.fix_body ccl in
- it_mkLambda_or_LetIn body ctx
+ Option.map (fun body ->
+ let env = push_rel_context ctx env_rec in
+ let body = interp_casted_constr_evars evdref env ~impls body ccl in
+ it_mkLambda_or_LetIn body ctx) fix.fix_body
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
@@ -483,29 +484,19 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
(* Jump over let-bindings. *)
-let rel_index n ctx =
- list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
-
-let rec unfold f b =
- match f b with
- | Some (x, b') -> x :: unfold f b'
- | None -> []
-
-let compute_possible_guardness_evidences n fixctx fixtype =
- match n with
- | Some (loc, n) -> [rel_index n fixctx]
+let compute_possible_guardness_evidences n fix =
+ match index_of_annot fix.fix_binders n with
+ | Some i -> [i]
| None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
- let len = List.length fixctx in
- unfold (function x when x = len -> None
- | n -> Some (n, succ n)) 0
+ interval 0 (local_assums_length fix.fix_binders - 1)
type recursive_preentry =
- identifier list * constr list * types list
+ identifier list * constr option list * types list
let interp_recursive isfix fixl notations =
let env = Global.env() in
@@ -532,53 +523,79 @@ let interp_recursive isfix fixl notations =
(* Instantiate evars and check all are resolved *)
let evd,_ = consider_remaining_unif_problems env_rec !evdref in
- let fixdefs = List.map (nf_evar evd) fixdefs in
+ let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
let fixtypes = List.map (nf_evar evd) fixtypes in
+ let fixctxlength = List.map (fun (_,ctx) -> rel_context_nhyps ctx) fixctxs in
let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
- List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+ List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs;
List.iter (check_evars env Evd.empty evd) fixtypes;
- check_mutuality env isfix (List.combine fixnames fixdefs);
+ if not (List.mem None fixdefs) then begin
+ let fixdefs = List.map Option.get fixdefs in
+ check_mutuality env isfix (List.combine fixnames fixdefs)
+ end;
(* Build the fix declaration block *)
- let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
- (snd (List.split fixctxs),fixnames,fixdecls,fixtypes),fiximps
-
-let interp_fixpoint fixl wfl notations =
- let (fixctxs,fixnames,fixdecls,fixtypes),fiximps =
- interp_recursive true fixl notations in
- let indexes, fixdecls =
- let possible_indexes =
- list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
- let indexes =
- search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
- Some indexes,
- list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames
- in
- ((fixnames,fixdecls,fixtypes),fiximps,indexes)
-
-let interp_cofixpoint fixl notations =
- let (fixctxs,fixnames,fixdecls,fixtypes),fiximps =
- interp_recursive false fixl notations in
- let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
- ((fixnames,fixdecls,fixtypes),fiximps)
-
-let declare_fixpoint boxed ((fixnames,fixdecls,fixtypes),fiximps,indexes) ntns =
- ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
- (* Declare the recursive definitions *)
- fixpoint_message indexes fixnames;
+ (fixnames,fixdefs,fixtypes),List.combine fixctxlength fiximps
+
+let interp_fixpoint = interp_recursive true
+let interp_cofixpoint = interp_recursive false
+
+let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
+ if List.mem None fixdefs then
+ (* Some bodies to define by proof *)
+ let thms =
+ list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+ let init_tac =
+ Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+ fixdefs) in
+ Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
+ (Some(false,indexes,init_tac)) thms (fun _ _ -> ())
+ else begin
+ (* We shortcut the proof process *)
+ let fixdefs = List.map Option.get fixdefs in
+ let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+ let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in
+ let fiximps = List.map snd fiximps in
+ let fixdecls =
+ list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+ ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
+ (* Declare the recursive definitions *)
+ fixpoint_message (Some indexes) fixnames;
+ end;
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation ntns
-let declare_cofixpoint boxed ((fixnames,fixdecls,fixtypes),fiximps) ntns =
- ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
- (* Declare the recursive definitions *)
- cofixpoint_message fixnames;
+let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
+ if List.mem None fixdefs then
+ (* Some bodies to define by proof *)
+ let thms =
+ list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+ let init_tac =
+ Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
+ fixdefs) in
+ Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
+ (Some(true,[],init_tac)) thms (fun _ _ -> ())
+ else begin
+ (* We shortcut the proof process *)
+ let fixdefs = List.map Option.get fixdefs in
+ let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+ let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+ let fiximps = List.map snd fiximps in
+ ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
+ (* Declare the recursive definitions *)
+ cofixpoint_message fixnames
+ end;
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation ntns
+let extract_decreasing_argument = function
+ | (_,(na,CStructRec),_,_,_) -> na
+ | _ -> error
+ "Only structural decreasing is supported for a non-Program Fixpoint"
+
let extract_fixpoint_components l =
let fixl, ntnl = List.split l in
- let wfl = List.map (fun (_,wf,_,_,_) -> fst wf) fixl in
+ let wfl = List.map extract_decreasing_argument fixl in
let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
{fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
fixl, List.flatten ntnl, wfl
@@ -591,7 +608,9 @@ let extract_cofixpoint_components l =
let do_fixpoint l b =
let fixl,ntns,wfl = extract_fixpoint_components l in
- declare_fixpoint b (interp_fixpoint fixl wfl ntns) ntns
+ let possible_indexes =
+ List.map2 compute_possible_guardness_evidences wfl fixl in
+ declare_fixpoint b (interp_fixpoint fixl ntns) possible_indexes ntns
let do_cofixpoint l b =
let fixl,ntns = extract_cofixpoint_components l in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index e42580c2b..48fc5a8eb 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -20,6 +20,7 @@ open Topconstr
open Decl_kinds
open Redexpr
open Constrintern
+open Pfedit
(*i*)
(*s This file is about the interpretation of raw commands into typed
@@ -102,7 +103,7 @@ val do_mutual_inductive :
type structured_fixpoint_expr = {
fix_name : identifier;
fix_binders : local_binder list;
- fix_body : constr_expr;
+ fix_body : constr_expr option;
fix_type : constr_expr
}
@@ -118,27 +119,27 @@ val extract_cofixpoint_components :
(cofixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
-(* Typing fixpoints and cofixpoint_expr *)
+(* Typing global fixpoints and cofixpoint_expr *)
type recursive_preentry =
- identifier list * constr list * types list
+ identifier list * constr option list * types list
val interp_fixpoint :
- structured_fixpoint_expr list -> lident option list -> decl_notation list ->
- recursive_preentry * manual_implicits list * int array option
+ structured_fixpoint_expr list -> decl_notation list ->
+ recursive_preentry * (int * manual_implicits) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * manual_implicits list
+ recursive_preentry * (int * manual_implicits) list
(* Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
- bool -> recursive_preentry * manual_implicits list * int array option ->
- decl_notation list -> unit
+ bool -> recursive_preentry * (int * manual_implicits) list ->
+ lemma_possible_guards -> decl_notation list -> unit
val declare_cofixpoint :
- bool -> recursive_preentry * manual_implicits list ->
+ bool -> recursive_preentry * (int * manual_implicits) list ->
decl_notation list -> unit
(* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index d9a26b427..48666c514 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -33,6 +33,7 @@ open Reductionops
open Topconstr
open Constrintern
open Impargs
+open Tacticals
(* Support for mutually proved theorems *)
@@ -44,26 +45,43 @@ let retrieve_first_recthm = function
(Option.map Declarations.force body,opaq)
| _ -> assert false
-let adjust_guardness_conditions const =
+let adjust_guardness_conditions const = function
+ | [] -> const (* Not a recursive statement *)
+ | possible_indexes ->
(* Try all combinations... not optimal *)
match kind_of_term const.const_entry_body with
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
- let possible_indexes =
- List.map (fun c ->
+(* let possible_indexes =
+ List.map2 (fun i c -> match i with Some i -> i | None ->
interval 0 (List.length ((lam_assum c))))
- (Array.to_list fixdefs) in
+ lemma_guard (Array.to_list fixdefs) in
+*)
let indexes =
search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
{ const with const_entry_body = mkFix ((indexes,0),fixdecls) }
| c -> const
-let look_for_mutual_statements thms =
- if List.tl thms <> [] then
- (* More than one statement: we look for a common inductive hyp or a *)
- (* common coinductive conclusion *)
+let find_mutually_recursive_statements thms =
let n = List.length thms in
- let inds = List.map (fun (id,(t,_) as x) ->
+ let inds = List.map (fun (id,(t,impls,annot)) ->
let (hyps,ccl) = decompose_prod_assum t in
+ let x = (id,(t,impls)) in
+ match annot with
+ (* Explicit fixpoint decreasing argument is given *)
+ | Some (Some (_,id),CStructRec) ->
+ let i,b,typ = lookup_rel_id id hyps in
+ (match kind_of_term t with
+ | Ind (kn,_ as ind) when
+ let mind = Global.lookup_mind kn in
+ mind.mind_finite & b = None ->
+ [ind,x,i],[]
+ | _ ->
+ error "Decreasing argument is not an inductive assumption.")
+ (* Unsupported cases *)
+ | Some (_,(CWfRec _|CMeasureRec _)) ->
+ error "Only structural decreasing is supported for mutual statements."
+ (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
+ | None | Some (None, CStructRec) ->
let whnf_hyp_hds = map_rel_context_in_env
(fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
(Global.env()) hyps in
@@ -75,7 +93,7 @@ let look_for_mutual_statements thms =
mind.mind_finite & b = None ->
[ind,x,i]
| _ ->
- []) 1 (List.rev whnf_hyp_hds)) in
+ []) 0 (List.rev whnf_hyp_hds)) in
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
@@ -102,7 +120,7 @@ let look_for_mutual_statements thms =
list_cartesians_filter (fun hyp oks ->
if List.for_all (of_same_mutind hyp) oks
then Some (hyp::oks) else None) [] inds_hyps in
- let ordered_inds,finite =
+ let ordered_inds,finite,guard =
match ordered_same_indccl, common_same_indhyp with
| indccl::rest, _ ->
assert (rest=[]);
@@ -110,37 +128,36 @@ let look_for_mutual_statements thms =
if common_same_indhyp <> [] then
if_verbose warning "Assuming mutual coinductive statements.";
flush_all ();
- indccl, true
+ indccl, true, []
| [], _::_ ->
if same_indccl <> [] &&
list_distinct (List.map pi1 (List.hd same_indccl)) then
if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+ let possible_guards = List.map (List.map pi3) inds_hyps in
(* assume the largest indices as possible *)
- list_last common_same_indhyp, false
+ list_last common_same_indhyp, false, possible_guards
| _, [] ->
error
("Cannot find common (mutual) inductive premises or coinductive" ^
" conclusions in the statements.")
in
- let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
- let rec_tac =
- if finite then
- match List.map (fun (id,(t,_)) -> (id,t)) thms with
- | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
- | _ -> assert false
- else
- (* nl is dummy: it will be recomputed at Qed-time *)
- match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
- | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
- | _ -> assert false in
- Some rec_tac,thms
- else
- None, thms
+ (finite,guard,None), List.map pi2 ordered_inds
+
+let look_for_possibly_mutual_statements = function
+ | [id,(t,impls,None)] ->
+ (* One non recursively proved theorem *)
+ None,[id,(t,impls)]
+ | _::_ as thms ->
+ (* More than one statement and/or an explicit decreasing mark: *)
+ (* we look for a common inductive hyp or a common coinductive conclusion *)
+ let recguard,thms = find_mutually_recursive_statements thms in
+ Some recguard,thms
+ | [] -> anomaly "Empty list of theorems."
(* Saving a goal *)
let save id const do_guard (locality,kind) hook =
- let const = if do_guard then adjust_guardness_conditions const else const in
+ let const = adjust_guardness_conditions const do_guard in
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
@@ -221,9 +238,6 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
error "This command can only be used for unnamed theorem."
-(*
- message("Overriding name "^(string_of_id id)^" and using "^save_ident)
-*)
let save_anonymous opacity save_ident =
let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
@@ -243,26 +257,47 @@ let save_anonymous_with_strength kind opacity save_ident =
let start_hook = ref ignore
let set_start_hook = (:=) start_hook
-let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
+let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
let sign = Global.named_context () in
let sign = clear_proofs sign in
!start_hook c;
Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
-let start_proof_com kind thms hook =
- let evdref = ref (create_evar_defs Evd.empty) in
- let env = Global.env () in
- let thms = List.map (fun (sopt,(bl,t)) ->
- let (env, ctx), imps = interp_context_evars evdref env bl in
- let t', imps' = interp_type_evars_impls ~evdref env t in
- let len = List.length ctx in
- (compute_proof_name sopt,
- (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), (len, imps @ lift_implicits len imps'))))
- thms in
- let rec_tac,thms = look_for_mutual_statements thms in
+let rec_tac_initializer finite guard thms =
+ if finite then
+ match List.map (fun (id,(t,_)) -> (id,t)) thms with
+ | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
+ | _ -> assert false
+ else
+ (* nl is dummy: it will be recomputed at Qed-time *)
+ let nl = List.map succ (List.map list_last guard) in
+ match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+ | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
+ | _ -> assert false
+
+let start_proof_with_initialization kind recguard thms hook =
+ let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
+ let init_tac,guard = match recguard with
+ | Some (finite,guard,init_tac) ->
+ let rec_tac = rec_tac_initializer finite guard thms in
+ Some (match init_tac with
+ | None ->
+ if Flags.is_auto_intros () then
+ tclTHENS rec_tac (List.map intro_tac thms)
+ else
+ rec_tac
+ | Some tacl ->
+ tclTHENS rec_tac
+ (if Flags.is_auto_intros () then
+ List.map2 (fun tac thm -> tclTHEN tac (intro_tac thm)) tacl thms
+ else
+ tacl)),guard
+ | None ->
+ assert (List.length thms = 1);
+ (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
match thms with
| [] -> anomaly "No proof to start"
- | (id,(t,(len,imps)) as thm)::other_thms ->
+ | (id,(t,(len,imps)))::other_thms ->
let hook strength ref =
let other_thms_data =
if other_thms = [] then [] else
@@ -273,14 +308,22 @@ let start_proof_com kind thms hook =
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
hook strength ref) thms_data in
- let init_tac =
- let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
- if Flags.is_auto_intros () then
- match rec_tac with
- | None -> Some (intro_tac thm)
- | Some tac -> Some (Tacticals.tclTHENS tac (List.map intro_tac thms))
- else rec_tac
- in start_proof id kind t ?init_tac hook ~compute_guard:(rec_tac<>None)
+ start_proof id kind t ?init_tac hook ~compute_guard:guard
+
+let start_proof_com kind thms hook =
+ let evdref = ref (create_evar_defs Evd.empty) in
+ let env = Global.env () in
+ let thms = List.map (fun (sopt,(bl,t,guard)) ->
+ let (env, ctx), imps = interp_context_evars evdref env bl in
+ let t', imps' = interp_type_evars_impls ~evdref env t in
+ let len = List.length ctx in
+ (compute_proof_name sopt,
+ (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx),
+ (len, imps @ lift_implicits len imps'),
+ guard)))
+ thms in
+ let recguard,thms = look_for_possibly_mutual_statements thms in
+ start_proof_with_initialization kind recguard thms hook
(* Admitted *)
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 398b336be..5d4f014a3 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -3,7 +3,7 @@
(* <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 *)
+(* * GNU Lesser General Public License Version 2.fix_expr *)
(************************************************************************)
(*i $Id$ i*)
@@ -16,16 +16,23 @@ open Topconstr
open Tacexpr
open Vernacexpr
open Proof_type
+open Pfedit
(*i*)
(* A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (types -> unit) -> unit
val start_proof : identifier -> goal_kind -> types ->
- ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
+ ?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
+ declaration_hook -> unit
val start_proof_com : goal_kind ->
- (lident option * (local_binder list * constr_expr)) list ->
+ (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+ declaration_hook -> unit
+
+val start_proof_with_initialization :
+ goal_kind -> (bool * lemma_possible_guards * tactic list option) option ->
+ (identifier * (types * (int * Impargs.manual_explicitation list))) list ->
declaration_hook -> unit
(* A hook the next three functions pass to cook_proof *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a37e3e5df..e7d32782d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -313,7 +313,7 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook =
| ProveBody (bl,t) -> (* local binders, typ *)
let hook _ _ = () in
start_proof_and_print (local,DefinitionBody Definition)
- [Some lid, (bl,t)] hook
+ [Some lid, (bl,t,None)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -1402,7 +1402,7 @@ let interp c = match c with
| VernacNop -> ()
(* Proof management *)
- | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->())
+ | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false (fun _ _->())
| VernacAbort id -> vernac_abort id
| VernacAbortAll -> vernac_abort_all ()
| VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6148b98ae..f75e1771d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -150,6 +150,12 @@ type definition_expr =
| DefineBody of local_binder list * raw_red_expr option * constr_expr
* constr_expr option
+type fixpoint_expr =
+ identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+
+type cofixpoint_expr =
+ identifier located * local_binder list * constr_expr * constr_expr option
+
type local_decl_expr =
| AssumExpr of lname * constr_expr
| DefExpr of lname * constr_expr * constr_expr option
@@ -218,7 +224,7 @@ type vernac_expr =
| VernacDefinition of definition_kind * lident * definition_expr *
declaration_hook
| VernacStartTheoremProof of theorem_kind *
- (lident option * (local_binder list * constr_expr)) list *
+ (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
bool * declaration_hook
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 14:15:36 +0000