diff options
| author | jforest | 2006-05-03 10:15:05 +0000 |
|---|---|---|
| committer | jforest | 2006-05-03 10:15:05 +0000 |
| commit | c599e13efd9e7b00c39d5a3812d8360124257f4b (patch) | |
| tree | bb5bcbd431cc2cde7efeb01d2149a30f8cecb515 | |
| parent | 836c28c4027b9626be4ca5371cc6559517fd7d1e (diff) | |
Cleanning and factorizing code in funind. Spliting new_arg_principles into to files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8781 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 308 | ||||
| -rw-r--r-- | .depend.coq | 79 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 1435 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_proofs.mli | 20 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 550 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.mli | 28 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 29 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 7 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 1770 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.mli | 34 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 15 | ||||
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 4 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 407 | ||||
| -rw-r--r-- | toplevel/vernacentries.mli | 2 |
15 files changed, 2407 insertions, 2285 deletions
@@ -350,7 +350,7 @@ toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \ library/libobject.cmi toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ - interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ + lib/util.cmi interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi @@ -426,6 +426,10 @@ contrib/first-order/sequent.cmi: lib/util.cmi kernel/term.cmi \ library/libnames.cmi lib/heap.cmi contrib/first-order/formula.cmi \ tactics/auto.cmi contrib/first-order/unify.cmi: kernel/term.cmi +contrib/funind/functional_principles_proofs.cmi: kernel/term.cmi \ + proofs/tacmach.cmi kernel/names.cmi +contrib/funind/functional_principles_types.cmi: kernel/term.cmi \ + proofs/tacmach.cmi pretyping/rawterm.cmi kernel/names.cmi contrib/funind/indfun_common.cmi: kernel/term.cmi pretyping/rawterm.cmi \ lib/pp.cmi kernel/names.cmi library/libnames.cmi contrib/funind/new_arg_principle.cmi: kernel/term.cmi proofs/tacmach.cmi \ @@ -537,13 +541,15 @@ ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ - lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \ - ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \ - ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi + lib/system.cmi ide/preferences.cmi lib/pp.cmi proofs/pfedit.cmi \ + ide/ideutils.cmi ide/highlight.cmo ide/find_phrase.cmo \ + ide/coq_commands.cmo ide/coq.cmi ide/command_windows.cmi \ + ide/blaster_window.cmo ide/coqide.cmi ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ - lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \ - ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \ - ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi + lib/system.cmx ide/preferences.cmx lib/pp.cmx proofs/pfedit.cmx \ + ide/ideutils.cmx ide/highlight.cmx ide/find_phrase.cmx \ + ide/coq_commands.cmx ide/coq.cmx ide/command_windows.cmx \ + ide/blaster_window.cmx ide/coqide.cmi ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \ toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi library/states.cmi \ @@ -2012,10 +2018,11 @@ tactics/tacinterp.cmo: lib/util.cmi pretyping/typing.cmi interp/topconstr.cmi \ library/libobject.cmi library/libnames.cmi library/lib.cmi \ tactics/leminv.cmi tactics/inv.cmi pretyping/inductiveops.cmi \ tactics/hiddentac.cmi lib/gmap.cmi library/global.cmi interp/genarg.cmi \ - parsing/g_xml.cmo pretyping/evd.cmi kernel/environ.cmi kernel/entries.cmi \ - tactics/elim.cmi lib/dyn.cmi tactics/dhyp.cmi pretyping/detyping.cmi \ - kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \ - kernel/closure.cmi tactics/auto.cmi tactics/tacinterp.cmi + parsing/g_xml.cmo pretyping/evd.cmi tactics/equality.cmi \ + kernel/environ.cmi kernel/entries.cmi tactics/elim.cmi lib/dyn.cmi \ + tactics/dhyp.cmi pretyping/detyping.cmi kernel/declarations.cmi \ + library/decl_kinds.cmo interp/constrintern.cmi kernel/closure.cmi \ + tactics/auto.cmi tactics/tacinterp.cmi tactics/tacinterp.cmx: lib/util.cmx pretyping/typing.cmx interp/topconstr.cmx \ pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ @@ -2030,10 +2037,11 @@ tactics/tacinterp.cmx: lib/util.cmx pretyping/typing.cmx interp/topconstr.cmx \ library/libobject.cmx library/libnames.cmx library/lib.cmx \ tactics/leminv.cmx tactics/inv.cmx pretyping/inductiveops.cmx \ tactics/hiddentac.cmx lib/gmap.cmx library/global.cmx interp/genarg.cmx \ - parsing/g_xml.cmx pretyping/evd.cmx kernel/environ.cmx kernel/entries.cmx \ - tactics/elim.cmx lib/dyn.cmx tactics/dhyp.cmx pretyping/detyping.cmx \ - kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \ - kernel/closure.cmx tactics/auto.cmx tactics/tacinterp.cmi + parsing/g_xml.cmx pretyping/evd.cmx tactics/equality.cmx \ + kernel/environ.cmx kernel/entries.cmx tactics/elim.cmx lib/dyn.cmx \ + tactics/dhyp.cmx pretyping/detyping.cmx kernel/declarations.cmx \ + library/decl_kinds.cmx interp/constrintern.cmx kernel/closure.cmx \ + tactics/auto.cmx tactics/tacinterp.cmi tactics/tacticals.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi proofs/refiner.cmi \ kernel/reduction.cmi lib/pp.cmi pretyping/pattern.cmi kernel/names.cmi \ @@ -2838,6 +2846,60 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \ parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx +contrib/funind/functional_principles_proofs.cmo: lib/util.cmi \ + pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ + tactics/tactics.cmi tactics/tacticals.cmi proofs/tactic_debug.cmi \ + pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ + proofs/tacexpr.cmo kernel/sign.cmi pretyping/reductionops.cmi \ + contrib/recdef/recdef.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \ + parsing/printer.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \ + library/libnames.cmi contrib/funind/indfun_common.cmi \ + tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \ + pretyping/evd.cmi tactics/equality.cmi kernel/entries.cmi \ + tactics/elim.cmi tactics/eauto.cmi kernel/declarations.cmi \ + interp/coqlib.cmi kernel/closure.cmi toplevel/cerrors.cmi \ + contrib/funind/functional_principles_proofs.cmi +contrib/funind/functional_principles_proofs.cmx: lib/util.cmx \ + pretyping/typing.cmx pretyping/termops.cmx kernel/term.cmx \ + tactics/tactics.cmx tactics/tacticals.cmx proofs/tactic_debug.cmx \ + pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ + proofs/tacexpr.cmx kernel/sign.cmx pretyping/reductionops.cmx \ + contrib/recdef/recdef.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ + parsing/printer.cmx lib/pp.cmx lib/options.cmx kernel/names.cmx \ + library/libnames.cmx contrib/funind/indfun_common.cmx \ + tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \ + pretyping/evd.cmx tactics/equality.cmx kernel/entries.cmx \ + tactics/elim.cmx tactics/eauto.cmx kernel/declarations.cmx \ + interp/coqlib.cmx kernel/closure.cmx toplevel/cerrors.cmx \ + contrib/funind/functional_principles_proofs.cmi +contrib/funind/functional_principles_types.cmo: toplevel/vernacexpr.cmo \ + toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \ + pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \ + tactics/tacticals.cmi pretyping/tacred.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi lib/system.cmi proofs/proof_type.cmi \ + parsing/printer.cmi pretyping/pretyping.cmi parsing/ppconstr.cmi \ + lib/pp.cmi proofs/pfedit.cmi lib/options.cmi kernel/names.cmi \ + library/libnames.cmi pretyping/indrec.cmi \ + contrib/funind/indfun_common.cmi tactics/hiddentac.cmi library/global.cmi \ + contrib/funind/functional_principles_proofs.cmi pretyping/evd.cmi \ + kernel/environ.cmi kernel/entries.cmi library/declare.cmi \ + kernel/declarations.cmi library/decl_kinds.cmo toplevel/command.cmi \ + kernel/closure.cmi toplevel/cerrors.cmi \ + contrib/funind/functional_principles_types.cmi +contrib/funind/functional_principles_types.cmx: toplevel/vernacexpr.cmx \ + toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ + pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ + tactics/tacticals.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx lib/system.cmx proofs/proof_type.cmx \ + parsing/printer.cmx pretyping/pretyping.cmx parsing/ppconstr.cmx \ + lib/pp.cmx proofs/pfedit.cmx lib/options.cmx kernel/names.cmx \ + library/libnames.cmx pretyping/indrec.cmx \ + contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \ + contrib/funind/functional_principles_proofs.cmx pretyping/evd.cmx \ + kernel/environ.cmx kernel/entries.cmx library/declare.cmx \ + kernel/declarations.cmx library/decl_kinds.cmx toplevel/command.cmx \ + kernel/closure.cmx toplevel/cerrors.cmx \ + contrib/funind/functional_principles_types.cmi contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi pretyping/rawterm.cmi lib/pp.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi library/global.cmi \ @@ -2853,43 +2915,45 @@ contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo kernel/sign.cmi \ proofs/refiner.cmi pretyping/rawterm.cmi parsing/pptactic.cmi lib/pp.cmi \ - parsing/pcoq.cmi contrib/funind/new_arg_principle.cmi kernel/names.cmi \ - library/nameops.cmi parsing/lexer.cmi contrib/funind/invfun.cmo \ - pretyping/indrec.cmi contrib/funind/indfun_common.cmi \ - contrib/funind/indfun.cmo interp/genarg.cmi parsing/egrammar.cmi \ - toplevel/cerrors.cmi + parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi parsing/lexer.cmi \ + contrib/funind/invfun.cmo pretyping/indrec.cmi \ + contrib/funind/indfun_common.cmi contrib/funind/indfun.cmo \ + interp/genarg.cmi contrib/funind/functional_principles_types.cmi \ + parsing/egrammar.cmi toplevel/cerrors.cmi contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx kernel/sign.cmx \ proofs/refiner.cmx pretyping/rawterm.cmx parsing/pptactic.cmx lib/pp.cmx \ - parsing/pcoq.cmx contrib/funind/new_arg_principle.cmx kernel/names.cmx \ - library/nameops.cmx parsing/lexer.cmx contrib/funind/invfun.cmx \ - pretyping/indrec.cmx contrib/funind/indfun_common.cmx \ - contrib/funind/indfun.cmx interp/genarg.cmx parsing/egrammar.cmx \ - toplevel/cerrors.cmx + parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx parsing/lexer.cmx \ + contrib/funind/invfun.cmx pretyping/indrec.cmx \ + contrib/funind/indfun_common.cmx contrib/funind/indfun.cmx \ + interp/genarg.cmx contrib/funind/functional_principles_types.cmx \ + parsing/egrammar.cmx toplevel/cerrors.cmx contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \ library/states.cmi contrib/recdef/recdef.cmo \ contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi \ parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi interp/notation.cmi \ - contrib/funind/new_arg_principle.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi pretyping/indrec.cmi \ - contrib/funind/indfun_common.cmi library/impargs.cmi library/global.cmi \ - pretyping/evd.cmi kernel/environ.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \ - toplevel/command.cmi toplevel/cerrors.cmi + kernel/names.cmi library/nameops.cmi library/libnames.cmi \ + pretyping/indrec.cmi contrib/funind/indfun_common.cmi library/impargs.cmi \ + library/global.cmi contrib/funind/functional_principles_types.cmi \ + contrib/funind/functional_principles_proofs.cmi pretyping/evd.cmi \ + kernel/environ.cmi kernel/declarations.cmi library/decl_kinds.cmo \ + interp/constrintern.cmi interp/constrextern.cmi toplevel/command.cmi \ + toplevel/cerrors.cmi contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx kernel/term.cmx proofs/tacmach.cmx \ library/states.cmx contrib/recdef/recdef.cmx \ contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx \ parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx interp/notation.cmx \ - contrib/funind/new_arg_principle.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx pretyping/indrec.cmx \ - contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \ - pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \ - library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \ - toplevel/command.cmx toplevel/cerrors.cmx + kernel/names.cmx library/nameops.cmx library/libnames.cmx \ + pretyping/indrec.cmx contrib/funind/indfun_common.cmx library/impargs.cmx \ + library/global.cmx contrib/funind/functional_principles_types.cmx \ + contrib/funind/functional_principles_proofs.cmx pretyping/evd.cmx \ + kernel/environ.cmx kernel/declarations.cmx library/decl_kinds.cmx \ + interp/constrintern.cmx interp/constrextern.cmx toplevel/command.cmx \ + toplevel/cerrors.cmx contrib/funind/invfun.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi contrib/funind/tacinvutils.cmi \ kernel/sign.cmi pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi \ @@ -3298,13 +3362,14 @@ contrib/omega/g_omega.cmx: lib/util.cmx tactics/tacinterp.cmx \ toplevel/cerrors.cmx contrib/omega/omega.cmo: lib/util.cmi kernel/names.cmi contrib/omega/omega.cmx: lib/util.cmx kernel/names.cmx -contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ - pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \ - kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ - pretyping/tacred.cmi proofs/tacmach.cmi kernel/safe_typing.cmi \ - pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ - pretyping/pretyping.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \ - lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ +contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi \ + toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \ + interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \ + tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \ + proofs/tacmach.cmi kernel/safe_typing.cmi pretyping/rawterm.cmi \ + proofs/proof_type.cmi parsing/printer.cmi pretyping/pretyping.cmi \ + lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi lib/options.cmi \ + library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi library/lib.cmi tactics/hiddentac.cmi \ library/global.cmi interp/genarg.cmi pretyping/evd.cmi \ tactics/equality.cmi kernel/environ.cmi kernel/entries.cmi \ @@ -3312,13 +3377,14 @@ contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \ interp/coqlib.cmi interp/constrintern.cmi toplevel/command.cmi \ kernel/closure.cmi toplevel/cerrors.cmi tactics/auto.cmi -contrib/recdef/recdef.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ - pretyping/typing.cmx interp/topconstr.cmx pretyping/termops.cmx \ - kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ - pretyping/tacred.cmx proofs/tacmach.cmx kernel/safe_typing.cmx \ - pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ - pretyping/pretyping.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ - lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ +contrib/recdef/recdef.cmx: toplevel/vernacinterp.cmx \ + toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ + interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \ + tactics/tactics.cmx tactics/tacticals.cmx pretyping/tacred.cmx \ + proofs/tacmach.cmx kernel/safe_typing.cmx pretyping/rawterm.cmx \ + proofs/proof_type.cmx parsing/printer.cmx pretyping/pretyping.cmx \ + lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx lib/options.cmx \ + library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx library/lib.cmx tactics/hiddentac.cmx \ library/global.cmx interp/genarg.cmx pretyping/evd.cmx \ tactics/equality.cmx kernel/environ.cmx kernel/entries.cmx \ @@ -3778,6 +3844,8 @@ ide/utils/uoptions.cmo: ide/utils/uoptions.cmi ide/utils/uoptions.cmx: ide/utils/uoptions.cmi tools/coqdoc/alpha.cmo: tools/coqdoc/alpha.cmi tools/coqdoc/alpha.cmx: tools/coqdoc/alpha.cmi +tools/coqdoc/cdglobals.cmo: config/coq_config.cmi +tools/coqdoc/cdglobals.cmx: config/coq_config.cmx tools/coqdoc/index.cmo: tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmi \ tools/coqdoc/index.cmi tools/coqdoc/index.cmx: tools/coqdoc/cdglobals.cmx tools/coqdoc/alpha.cmx \ @@ -3901,74 +3969,96 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/memory.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/alloc.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/alloc.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /usr/local/lib/ocaml/caml/alloc.h + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_memory.h /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local//lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/memory.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/alloc.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_memory.h /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/alloc.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h + kernel/byterun/coq_memory.h /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /usr/local/lib/ocaml/caml/alloc.h + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/compatibility.h \ + /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_memory.h /usr/local//lib/ocaml/caml/config.h \ + /usr/local//lib/ocaml/caml/fail.h \ + /usr/local//lib/ocaml/caml/mlvalues.h \ + /usr/local//lib/ocaml/caml/misc.h \ + /usr/local//lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local//lib/ocaml/caml/alloc.h diff --git a/.depend.coq b/.depend.coq index 981e76b3bb..483ca08ad5 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,3 +1,30 @@ +theories/FSets/DecidableType.vo: theories/FSets/DecidableType.v theories/Lists/SetoidList.vo +theories/FSets/OrderedType.vo: theories/FSets/OrderedType.v theories/Lists/SetoidList.vo +theories/FSets/OrderedTypeEx.vo: theories/FSets/OrderedTypeEx.v theories/FSets/OrderedType.vo theories/ZArith/ZArith.vo theories/NArith/NArith.vo theories/NArith/Ndec.vo theories/Arith/Compare_dec.vo +theories/FSets/OrderedTypeAlt.vo: theories/FSets/OrderedTypeAlt.v theories/FSets/OrderedType.vo +theories/FSets/FSetInterface.vo: theories/FSets/FSetInterface.v theories/Bool/Bool.vo theories/FSets/OrderedType.vo +theories/FSets/FSetList.vo: theories/FSets/FSetList.v theories/FSets/FSetInterface.vo +theories/FSets/FSetBridge.vo: theories/FSets/FSetBridge.v theories/FSets/FSetInterface.vo +theories/FSets/FSetFacts.vo: theories/FSets/FSetFacts.v theories/FSets/FSetInterface.vo +theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v theories/FSets/FSetInterface.vo theories/FSets/FSetFacts.vo +theories/FSets/FSetEqProperties.vo: theories/FSets/FSetEqProperties.v theories/FSets/FSetProperties.vo theories/Bool/Zerob.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo +theories/FSets/FSets.vo: theories/FSets/FSets.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetToFiniteSet.vo +theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/FSets/DecidableType.vo +theories/FSets/FSetWeakList.vo: theories/FSets/FSetWeakList.v theories/FSets/FSetWeakInterface.vo +theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/FSetWeakInterface.vo +theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/FSets/DecidableType.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetWeakList.vo +theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.vo +theories/FSets/FMapList.vo: theories/FSets/FMapList.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo +theories/FSets/FMaps.vo: theories/FSets/FMaps.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapIntMap.vo +theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo +theories/FSets/FMapWeakList.vo: theories/FSets/FMapWeakList.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakInterface.vo +theories/FSets/FMapWeak.vo: theories/FSets/FMapWeak.v theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo +theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo +theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo +theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo +theories/FSets/Int.vo: theories/FSets/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo +theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo +theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo @@ -189,7 +216,6 @@ theories/FSets/FSetBridge.vo: theories/FSets/FSetBridge.v theories/FSets/FSetInt theories/FSets/FSetFacts.vo: theories/FSets/FSetFacts.v theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo: theories/FSets/FSetProperties.v theories/FSets/FSetInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetEqProperties.vo: theories/FSets/FSetEqProperties.v theories/FSets/FSetProperties.vo theories/Bool/Zerob.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo -theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo theories/FSets/FSets.vo: theories/FSets/FSets.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FSetInterface.vo theories/FSets/FSetBridge.vo theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetList.vo theories/FSets/FSetToFiniteSet.vo theories/FSets/FSetWeakInterface.vo: theories/FSets/FSetWeakInterface.v theories/Bool/Bool.vo theories/FSets/DecidableType.vo theories/FSets/FSetWeakList.vo: theories/FSets/FSetWeakList.v theories/FSets/FSetWeakInterface.vo @@ -197,7 +223,6 @@ theories/FSets/FSetWeakFacts.vo: theories/FSets/FSetWeakFacts.v theories/FSets/F theories/FSets/FSetWeak.vo: theories/FSets/FSetWeak.v theories/FSets/DecidableType.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FSetFacts.vo theories/FSets/FSetWeakList.vo theories/FSets/FMapInterface.vo: theories/FSets/FMapInterface.v theories/FSets/FSetInterface.vo theories/FSets/FMapList.vo: theories/FSets/FMapList.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo -theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo theories/FSets/FMaps.vo: theories/FSets/FMaps.v theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapIntMap.vo theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakList.vo: theories/FSets/FMapWeakList.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakInterface.vo @@ -206,6 +231,8 @@ theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/ZArith/ZA theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo theories/FSets/Int.vo: theories/FSets/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo +theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo +theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo @@ -239,6 +266,54 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base. theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo +theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo +theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo +theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo +theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo +theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo +theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo +theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo +theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo +theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo +theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo +theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo +theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo +theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo +theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo +theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo +theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo +theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo +theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo +theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo +theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo +theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo +theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo +theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo +theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo +theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo +theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo +theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo +theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo +theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo +theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo +theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo +theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo +theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo +theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo +theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo +theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Relations/Relation_Definitions.vo theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo @@ -276,7 +276,9 @@ JPROVERCMO=\ FUNINDCMO=\ contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo \ contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \ - contrib/funind/rawterm_to_relation.cmo contrib/funind/new_arg_principle.cmo \ + contrib/funind/rawterm_to_relation.cmo \ + contrib/funind/functional_principles_proofs.cmo \ + contrib/funind/functional_principles_types.cmo \ contrib/funind/invfun.cmo contrib/funind/indfun.cmo \ contrib/funind/indfun_main.cmo diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml new file mode 100644 index 0000000000..0ee8a7e759 --- /dev/null +++ b/contrib/funind/functional_principles_proofs.ml @@ -0,0 +1,1435 @@ +open Printer +open Util +open Term +open Termops +open Names +open Declarations +open Pp +open Entries +open Hiddentac +open Evd +open Tacmach +open Proof_type +open Tacticals +open Tactics +open Indfun_common +open Libnames + +let msgnl = Pp.msgnl + +let do_observe () = + Tacinterp.get_debug () <> Tactic_debug.DebugOff + + +let observe strm = + if do_observe () + then Pp.msgnl strm + else () + +let observennl strm = + if do_observe () + then begin Pp.msg strm;Pp.pp_flush () end + else () + + + + +let do_observe_tac s tac g = + try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v + with e -> + let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in + msgnl (str "observation "++ s++str " raised exception " ++ + Cerrors.explain_exn e ++ str " on goal " ++ goal ); + raise e;; + + +let observe_tac s tac g = + if do_observe () + then do_observe_tac (str s) tac g + else tac g + +(* let observe_stream_tac s tac g = *) +(* if do_observe () *) +(* then do_observe_tac s tac g *) +(* else tac g *) + + + +let tclTRYD tac = + if !Options.debug || do_observe () + then (fun g -> try (* do_observe_tac "" *)tac g with _ -> tclIDTAC g) + else tac + + +let list_chop ?(msg="") n l = + try + list_chop n l + with Failure (msg') -> + failwith (msg ^ msg') + + +let make_refl_eq type_of_t t = + let refl_equal_term = Lazy.force refl_equal in + mkApp(refl_equal_term,[|type_of_t;t|]) + + +type pte_info = + { + proving_tac : (identifier list -> Tacmach.tactic); + is_valid : constr -> bool + } + +type ptes_info = pte_info Idmap.t + +type 'a dynamic_info = + { + nb_rec_hyps : int; + rec_hyps : identifier list ; + eq_hyps : identifier list; + info : 'a + } + +type body_info = constr dynamic_info + + +let finish_proof dynamic_infos g = + observe_tac "finish" + ( h_assumption) + g + + +let refine c = + Tacmach.refine_no_check c + +let thin l = + Tacmach.thin_no_check l + + +let cut_replacing id t tac :tactic= + tclTHENS (cut t) + [ tclTHEN (thin_no_check [id]) (introduction_no_check id); + tac + ] + +let intro_erasing id = tclTHEN (thin [id]) (introduction id) + + + +let rec_hyp_id = id_of_string "rec_hyp" + +let is_trivial_eq t = + match kind_of_term t with + | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> + eq_constr t1 t2 + | _ -> false + + +let rec incompatible_constructor_terms t1 t2 = + let c1,arg1 = decompose_app t1 + and c2,arg2 = decompose_app t2 + in + (not (eq_constr t1 t2)) && + isConstruct c1 && isConstruct c2 && + ( + not (eq_constr c1 c2) || + List.exists2 incompatible_constructor_terms arg1 arg2 + ) + +let is_incompatible_eq t = + match kind_of_term t with + | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> + incompatible_constructor_terms t1 t2 + | _ -> false + +let change_hyp_with_using msg hyp_id t tac : tactic = + fun g -> + let prov_id = pf_get_new_id hyp_id g in + tclTHENS + (observe_tac msg (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t)) + [tclTHENLIST + [ + observe_tac "change_hyp_with_using thin" (thin [hyp_id]); + observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id) + ]] g + +exception TOREMOVE + + +let prove_trivial_eq h_id context (type_of_term,term) = + let nb_intros = List.length context in + tclTHENLIST + [ + tclDO nb_intros intro; (* introducing context *) + (fun g -> + let context_hyps = + fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) + in + let context_hyps' = + (mkApp(Lazy.force refl_equal,[|type_of_term;term|])):: + (List.map mkVar context_hyps) + in + let to_refine = applist(mkVar h_id,List.rev context_hyps') in + refine to_refine g + ) + ] + + +let isAppConstruct t = + if isApp t + then isConstruct (fst (destApp t)) + else false + + +let nf_betaiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta + + +let rec subst_rel_map sub t = + match kind_of_term t with + | Rel k -> + begin + try + Intmap.find (k+1) sub + with Not_found -> + t + end + | _ -> map_constr (subst_rel_map sub) t + + +let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = + let nochange msg = + begin +(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *) + failwith "NoChange"; + end + in + if not (noccurn 1 end_of_type) + then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) + if not (isApp t) then nochange "not an equality"; + let f_eq,args = destApp t in + if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality"; + let t1 = args.(1) + and t2 = args.(2) + and t1_typ = args.(0) + in + if not (closed0 t1) then nochange "not a closed lhs"; + let rec compute_substitution sub t1 t2 = + if isRel t2 + then + let t2 = destRel t2 in + begin + try + let t1' = Intmap.find t2 sub in + if not (eq_constr t1 t1') then nochange "twice bound variable"; + sub + with Not_found -> + assert (closed0 t1); + Intmap.add t2 t1 sub + end + else if isAppConstruct t1 && isAppConstruct t2 + then + begin + let c1,args1 = destApp t1 + and c2,args2 = destApp t2 + in + if not (eq_constr c1 c2) then anomaly "deconstructing equation"; + array_fold_left2 compute_substitution sub args1 args2 + end + else + if (eq_constr t1 t2) then sub else nochange "cannot solve" + in + let sub = compute_substitution Intmap.empty t1 t2 in + let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) + let new_end_of_type = + Intmap.fold + (fun i t end_of_type -> lift 1 (substnl [t] (i-1) end_of_type)) + sub + end_of_type_with_pop + in + let old_context_length = List.length context + 1 in + let witness_fun = + mkLetIn(Anonymous,make_refl_eq t1_typ t1,t, + mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) + ) + in + let new_type_of_hyp,ctxt_size,witness_fun = + list_fold_left_i + (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> + try + let witness = Intmap.find i sub in + if b' <> None then anomaly "can not redefine a rel!"; + (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) + with Not_found -> + (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) + ) + 1 + (new_end_of_type,0,witness_fun) + context + in + let new_type_of_hyp = Reductionops.nf_betaiota new_type_of_hyp in + let new_ctxt,new_end_of_type = + Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp + in + let prove_new_hyp : tactic = + tclTHEN + (tclDO ctxt_size intro) + (fun g -> + let all_ids = pf_ids_of_hyps g in + let new_ids,_ = list_chop ctxt_size all_ids in + let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in + refine to_refine g + ) + in + let simpl_eq_tac = + change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp prove_new_hyp + in +(* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) +(* str "removing an equation " ++ fnl ()++ *) +(* str "old_typ_of_hyp :=" ++ *) +(* Printer.pr_lconstr_env *) +(* env *) +(* (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *) +(* ++ fnl () ++ *) +(* str "new_typ_of_hyp := "++ *) +(* Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *) +(* ++ str "old context := " ++ pr_rel_context env context ++ fnl () *) +(* ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl () *) +(* ++ str "old type := " ++ pr_lconstr end_of_type ++ fnl () *) +(* ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl () *) +(* ); *) + new_ctxt,new_end_of_type,simpl_eq_tac + + +let is_property ptes_info t_x full_type_of_hyp = + if isApp t_x + then + let pte,args = destApp t_x in + if isVar pte && array_for_all closed0 args + then + try + let info = Idmap.find (destVar pte) ptes_info in + info.is_valid full_type_of_hyp + with Not_found -> false + else false + else false + +let isLetIn t = + match kind_of_term t with + | LetIn _ -> true + | _ -> false + + +let h_reduce_with_zeta = + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + + + +let rewrite_until_var arg_num eq_ids : tactic = + let test_var g = + let _,args = destApp (pf_concl g) in + isVar args.(arg_num) + in + let rec do_rewrite eq_ids g = + if test_var g + then tclIDTAC g + else + match eq_ids with + | [] -> anomaly "Cannot find a way to prove recursive property"; + | eq_id::eq_ids -> + tclTHEN + (tclTRY (Equality.rewriteRL (mkVar eq_id))) + (do_rewrite eq_ids) + g + in + do_rewrite eq_ids + + +let rec_pte_id = id_of_string "Hrec" +let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = + let coq_False = Coqlib.build_coq_False () in + let coq_True = Coqlib.build_coq_True () in + let coq_I = Coqlib.build_coq_I () in + let rec scan_type context type_of_hyp : tactic = + if isLetIn type_of_hyp then + let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in + let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in + (* length of context didn't change ? *) + let new_context,new_typ_of_hyp = + Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp + in + tclTHENLIST + [ + h_reduce_with_zeta + (Tacticals.onHyp hyp_id) + ; + scan_type new_context new_typ_of_hyp + + ] + else if isProd type_of_hyp + then + begin + let (x,t_x,t') = destProd type_of_hyp in + let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in + if is_property ptes_infos t_x actual_real_type_of_hyp then + begin + let pte,pte_args = (destApp t_x) in + let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in + let popped_t' = pop t' in + let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in + let prove_new_type_of_hyp = + let context_length = List.length context in + tclTHENLIST + [ + tclDO context_length intro; + (fun g -> + let context_hyps_ids = + fst (list_chop ~msg:"rec hyp : context_hyps" + context_length (pf_ids_of_hyps g)) + in + let rec_pte_id = pf_get_new_id rec_pte_id g in + let to_refine = + applist(mkVar hyp_id, + List.rev_map mkVar (rec_pte_id::context_hyps_ids) + ) + in + observe_tac "rec hyp " + (tclTHENS + (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x) + [observe_tac "prove rec hyp" (prove_rec_hyp eq_hyps); + observe_tac "prove rec hyp" + (refine to_refine) + ]) + g + ) + ] + in + tclTHENLIST + [ + observe_tac "hyp rec" + (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp); + scan_type context popped_t' + ] + end + else if eq_constr t_x coq_False then + begin +(* observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ *) +(* str " since it has False in its preconds " *) +(* ); *) + raise TOREMOVE; (* False -> .. useless *) + end + else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) + else if eq_constr t_x coq_True (* Trivial => we remove this precons *) + then +(* observe (str "In "++Ppconstr.pr_id hyp_id++ *) +(* str " removing useless precond True" *) +(* ); *) + let popped_t' = pop t' in + let real_type_of_hyp = + it_mkProd_or_LetIn ~init:popped_t' context + in + let prove_trivial = + let nb_intro = List.length context in + tclTHENLIST [ + tclDO nb_intro intro; + (fun g -> + let context_hyps = + fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) + in + let to_refine = + applist (mkVar hyp_id, + List.rev (coq_I::List.map mkVar context_hyps) + ) + in + refine to_refine g + ) + ] + in + tclTHENLIST[ + change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp + (observe_tac "prove_trivial" prove_trivial); + scan_type context popped_t' + ] + else if is_trivial_eq t_x + then (* t_x := t = t => we remove this precond *) + let popped_t' = pop t' in + let real_type_of_hyp = + it_mkProd_or_LetIn ~init:popped_t' context + in + let _,args = destApp t_x in + tclTHENLIST + [ + change_hyp_with_using + "prove_trivial_eq" + hyp_id + real_type_of_hyp + (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1)))); + scan_type context popped_t' + ] + else + begin + try + let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in + tclTHEN + tac + (scan_type new_context new_t') + with Failure "NoChange" -> + (* Last thing todo : push the rel in the context and continue *) + scan_type ((x,None,t_x)::context) t' + end + end + else + tclIDTAC + in + try + scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id] + with TOREMOVE -> + thin [hyp_id],[] + + +let clean_goal_with_heq ptes_infos continue_tac dyn_infos = + fun g -> + let env = pf_env g + and sigma = project g + in + let tac,new_hyps = + List.fold_left ( + fun (hyps_tac,new_hyps) hyp_id -> + let hyp_tac,new_hyp = + clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma + in + (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps + ) + (tclIDTAC,[]) + dyn_infos.rec_hyps + in + let new_infos = + { dyn_infos with + rec_hyps = new_hyps; + nb_rec_hyps = List.length new_hyps + } + in + tclTHENLIST + [ + tac ; + (continue_tac new_infos) + ] + g + +let heq_id = id_of_string "Heq" + +let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = + fun g -> + let heq_id = pf_get_new_id heq_id g in + let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in + tclTHENLIST + [ + (* We first introduce the variables *) + tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps); + (* Then the equation itself *) + introduction_no_check heq_id; + (* Then the new hypothesis *) + tclMAP introduction_no_check dyn_infos.rec_hyps; + observe_tac "after_introduction" (fun g' -> + (* We get infos on the equations introduced*) + let new_term_value_eq = pf_type_of g' (mkVar heq_id) in + (* compute the new value of the body *) + let new_term_value = + match kind_of_term new_term_value_eq with + | App(f,[| _;_;args2 |]) -> args2 + | _ -> +(* observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++ *) +(* pr_lconstr_env (pf_env g') new_term_value_eq *) +(* ); *) + anomaly "cannot compute new term value" + in + let fun_body = + mkLambda(Anonymous, + pf_type_of g' term, + replace_term term (mkRel 1) dyn_infos.info + ) + in + let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in + let new_infos = + {dyn_infos with + info = new_body; + eq_hyps = heq_id::dyn_infos.eq_hyps + } + in + clean_goal_with_heq ptes_infos continue_tac new_infos g' + ) + ] + g + + +let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = + let args = Array.of_list (List.map mkVar args_id) in + let instanciate_one_hyp hid = + tclORELSE + ( (* we instanciate the hyp if possible *) + fun g -> + let prov_hid = pf_get_new_id hid g in + tclTHENLIST[ + forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); + thin [hid]; + h_rename prov_hid hid + ] g + ) + ( (* + if not then we are in a mutual function block + and this hyp is a recursive hyp on an other function. + + We are not supposed to use it while proving this + principle so that we can trash it + + *) + (fun g -> +(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *) + thin [hid] g + ) + ) + in + if args_id = [] + then + tclTHENLIST [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + do_prove hyps + ] + else + tclTHENLIST + [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP instanciate_one_hyp hyps; + (fun g -> + let all_g_hyps_id = + List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty + in + let remaining_hyps = + List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps + in + do_prove remaining_hyps g + ) + ] + +let build_proof + (interactive_proof:bool) + (fnames:constant list) + ptes_infos + dyn_infos + : tactic = + let rec build_proof_aux do_finalize dyn_infos : tactic = + fun g -> + +(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) + match kind_of_term dyn_infos.info with + | Case(_,_,t,_) -> + let g_nb_prod = nb_prod (pf_concl g) in + let type_of_term = pf_type_of g t in + let term_eq = + make_refl_eq type_of_term t + in + tclTHENSEQ + [ + h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps); + thin dyn_infos.rec_hyps; + pattern_option [[-1],t] None; + h_simplest_case t; + (fun g' -> + let g'_nb_prod = nb_prod (pf_concl g') in + let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos + nb_instanciate_partial + (build_proof do_finalize) + t + dyn_infos) + g' + ) + + ] g + | Lambda(n,t,b) -> + begin + match kind_of_term( pf_concl g) with + | Prod _ -> + tclTHEN + intro + (fun g' -> + let (id,_,_) = pf_last_hyp g' in + let new_term = + pf_nf_betaiota g' + (mkApp(dyn_infos.info,[|mkVar id|])) + in + let new_infos = {dyn_infos with info = new_term} in + let do_prove new_hyps = + build_proof do_finalize + {new_infos with + rec_hyps = new_hyps; + nb_rec_hyps = List.length new_hyps + } + in + observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' + (* build_proof do_finalize new_infos g' *) + ) g + | _ -> + do_finalize dyn_infos g + end + | Cast(t,_,_) -> + build_proof do_finalize {dyn_infos with info = t} g + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + do_finalize dyn_infos g + | App(_,_) -> + let f,args = decompose_app dyn_infos.info in + begin + match kind_of_term f with + | App _ -> assert false (* we have collected all the app in decompose_app *) + | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> + let new_infos = + { dyn_infos with + info = (f,args) + } + in + build_proof_args do_finalize new_infos g + | Const c when not (List.mem c fnames) -> + let new_infos = + { dyn_infos with + info = (f,args) + } + in +(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) + build_proof_args do_finalize new_infos g + | Const _ -> + do_finalize dyn_infos g + | Lambda _ -> + let new_term = Reductionops.nf_beta dyn_infos.info in + build_proof do_finalize {dyn_infos with info = new_term} + g + | LetIn _ -> + let new_infos = + { dyn_infos with info = nf_betaiotazeta dyn_infos.info } + in + + tclTHENLIST + [tclMAP + (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + dyn_infos.rec_hyps; + h_reduce_with_zeta Tacticals.onConcl; + build_proof do_finalize new_infos + ] + g + | Cast(b,_,_) -> + build_proof do_finalize {dyn_infos with info = b } g + | Case _ | Fix _ | CoFix _ -> + let new_finalize dyn_infos = + let new_infos = + { dyn_infos with + info = dyn_infos.info,args + } + in + build_proof_args do_finalize new_infos + in + build_proof new_finalize {dyn_infos with info = f } g + end + | Fix _ | CoFix _ -> + error ( "Anonymous local (co)fixpoints are not handled yet") + + | Prod _ -> error "Prod" + | LetIn _ -> + let new_infos = + { dyn_infos with + info = nf_betaiotazeta dyn_infos.info + } + in + + tclTHENLIST + [tclMAP + (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + dyn_infos.rec_hyps; + h_reduce_with_zeta Tacticals.onConcl; + build_proof do_finalize new_infos + ] g + | Rel _ -> anomaly "Free var in goal conclusion !" + and build_proof do_finalize dyn_infos g = +(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *) + (build_proof_aux do_finalize dyn_infos) g + and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = + fun g -> +(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) +(* then msgnl (str "build_proof_args with " ++ *) +(* pr_lconstr_env (pf_env g) f_args' *) +(* ); *) + let (f_args',args) = dyn_infos.info in + let tac : tactic = + fun g -> + match args with + | [] -> + do_finalize {dyn_infos with info = f_args'} g + | arg::args -> +(* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *) +(* fnl () ++ *) +(* pr_goal (Tacmach.sig_it g) *) +(* ); *) + let do_finalize dyn_infos = + let new_arg = dyn_infos.info in + (* tclTRYD *) + (build_proof_args + do_finalize + {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} + ) + in + build_proof do_finalize + {dyn_infos with info = arg } + g + in + observe_tac "build_proof_args" (tac ) g + in + let do_finish_proof dyn_infos = + (* tclTRYD *) (clean_goal_with_heq + ptes_infos + finish_proof dyn_infos) + in + observe_tac "build_proof" + (build_proof do_finish_proof dyn_infos) + + + + + + + + + + + + +(* Proof of principles from structural functions *) +let is_pte_type t = + isSort (snd (decompose_prod t)) + +let is_pte (_,_,t) = is_pte_type t + + + + +type static_fix_info = + { + idx : int; + name : identifier; + types : types; + nb_realargs : int + } + +let prove_rec_hyp fix_info = + { proving_tac = + (fun eq_hyps -> tclTHEN + (rewrite_until_var (fix_info.idx - 1) eq_hyps) + (fun g -> + let _,pte_args = destApp (pf_concl g) in + let rec_hyp_proof = + mkApp(mkVar fix_info.name,array_get_start pte_args) + in + refine rec_hyp_proof g + )) + ; + is_valid = fun _ -> true + } + + +exception Not_Rec + + +let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic = + fun goal -> +(* observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++ *) +(* pr_lconstr (mkConst fnames.(fun_num))); *) + let princ_type = pf_concl goal in + let princ_info = compute_elim_sig princ_type in + let get_body const = + match (Global.lookup_constant const ).const_body with + | Some b -> + let body = force b in + Tacred.cbv_norm_flags + (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (Global.env ()) + (Evd.empty) + body + | None -> error ( "Cannot define a principle over an axiom ") + in + let fbody = get_body fnames.(fun_num) in + let params : identifier list ref = ref [] in + let predicates : identifier list ref = ref [] in + let args : identifier list ref = ref [] in + let branches : identifier list ref = ref [] in + let pte_to_fix = ref Idmap.empty in + let fbody_with_params = ref None in + let intro_with_remembrance ref number : tactic = + tclTHEN + ( tclDO number intro ) + (fun g -> + let last_n = list_chop number (pf_hyps g) in + ref := List.map (fun (id,_,_) -> id) (fst last_n)@ !ref; + tclIDTAC g + ) + in + let rec partial_combine body params = + match kind_of_term body,params with + | Lambda (x,t,b),param::params -> + partial_combine (subst1 param b) params + | Fix(infos),_ -> + body,params, Some (infos) + | _ -> body,params,None + in + let build_pte_to_fix (offset:int) params predicates + ((idxs,fix_num),(na,typearray,ca)) (avoid,_) = +(* let true_params,_ = list_chop offset params in *) + let true_params = List.rev params in + let avoid = ref avoid in + let res = list_fold_left_i + (fun i acc pte_id -> + let this_fix_id = fresh_id !avoid "fix___" in + avoid := this_fix_id::!avoid; +(* let this_body = substl (List.rev fnames_as_constr) ca.(i) in *) + let realargs,_ = decompose_lam ca.(i) in + let n_realargs = List.length realargs - List.length params in +(* observe (str "n_realargs := " ++ str (string_of_int n_realargs)); *) +(* observe (str "n_fix := " ++ str (string_of_int(Array.length ca))); *) +(* observe (str "body := " ++ pr_lconstr ca.(i)); *) + + let new_type = prod_applist typearray.(i) true_params in + let new_type_args,_ = decompose_prod new_type in + let nargs = List.length new_type_args in + let pte_args = + (* let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in *) + let f = applist((* all_funs *)mkConst fnames.(i),true_params) in + let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in + (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f] + in + let app_pte = applist(mkVar pte_id,pte_args) in + let new_type = compose_prod new_type_args app_pte in + + let fix_info = + { + idx = idxs.(i) - offset + 1; + name = this_fix_id; + types = new_type; + nb_realargs = n_realargs + } + in + pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix; + fix_info::acc + ) + 0 + [] + predicates + in + !avoid,List.rev res + in + let mk_fixes : tactic = + fun g -> + let body_p,params',fix_infos = + partial_combine fbody (List.rev_map mkVar !params) + in + fbody_with_params := Some body_p; + let offset = List.length params' in + let not_real_param,true_params = + list_chop + ((List.length !params ) - offset) + !params + in + params := true_params; args := not_real_param; +(* observe (str "mk_fixes : params are "++ *) +(* prlist_with_sep spc *) +(* (fun id -> pr_lconstr (mkVar id)) *) +(* !params *) +(* ); *) + let new_avoid,infos = + option_fold_right + (build_pte_to_fix + offset + (List.map mkVar !params) + (List.rev !predicates) + ) + fix_infos + ((pf_ids_of_hyps g),[]) + in + let pre_info,infos = list_chop fun_num infos in + match pre_info,infos with + | [],[] -> tclIDTAC g + | _,this_fix_info::infos' -> + let other_fix_info = + List.map + (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types) + (pre_info@infos') + in + if other_fix_info = [] + then h_fix (Some this_fix_info.name) this_fix_info.idx g + else h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info g + | _,[] -> anomaly "Not a valid information" + in + let do_prove ptes_to_fixes args branches : tactic = + fun g -> + let nb_intros_to_do = List.length (fst (Sign.decompose_prod_assum (pf_concl g))) in +(* observe (str "nb_intros_to_do " ++ str (string_of_int nb_intros_to_do)); *) + tclTHEN + (tclDO nb_intros_to_do intro) + (fun g -> + match kind_of_term (pf_concl g) with + | App(pte,pte_args) when isVar pte -> + begin + let pte = destVar pte in + try + if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec; + let nparams = List.length !params in + let args_as_constr = List.map mkVar args in + let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in + let other_args_as_constr = List.map mkVar other_args in + let rec_num,new_body = + let idx' = list_index pte (List.rev !predicates) - 1 in + let f = fnames.(idx') in + let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly "" + in + let name_of_f = Name ( id_of_label (con_label f)) in + let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in + let idx'' = list_index name_of_f (Array.to_list na) - 1 in + let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in + let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in + rec_nums.(idx'') - nparams ,body + in + let applied_body_with_real_args = + Reductionops.nf_betaiota + (applist(new_body,List.rev args_as_constr)) + in + let applied_body = +(* Reductionops.nf_beta *) + Reductionops.nf_betaiota + (applist(applied_body_with_real_args,List.rev other_args_as_constr)) + in +(* observe (str "applied_body_with_real_args := "++ pr_lconstr_env (pf_env g) applied_body_with_real_args); *) +(* observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); *) + let do_prove branches applied_body = + build_proof + interactive_proof + (Array.to_list fnames) + (Idmap.map prove_rec_hyp ptes_to_fixes) + branches + applied_body + in + let replace_and_prove = + tclTHENS + (fun g -> (Equality.replace (array_last pte_args) applied_body) g) + [ + tclTHENLIST + [ + generalize other_args_as_constr; + thin other_args; + clean_goal_with_heq + (Idmap.map prove_rec_hyp ptes_to_fixes) + do_prove + { + nb_rec_hyps = List.length branches; + rec_hyps = branches; + info = applied_body_with_real_args; + eq_hyps = []; + } ]; + let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in + let id_as_induction_constr = Tacexpr.ElimOnConstr id in + (tclTHENSEQ + [Tactics.new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *) + Tactics.intros_reflexivity + ]) + ] + in + (observe_tac "doing replacement" ( replace_and_prove)) g + with Not_Rec -> + let fname = destConst (fst (decompose_app (array_last pte_args))) in + tclTHEN + (unfold_in_concl [([],Names.EvalConstRef fname)]) + (observe_tac "" + (fun g' -> + let body = array_last (snd (destApp (pf_concl g'))) in + let dyn_infos = + { nb_rec_hyps = List.length branches; + rec_hyps = branches; + info = body; + eq_hyps = [] + } + in + let do_prove = + build_proof + interactive_proof + (Array.to_list fnames) + (Idmap.map prove_rec_hyp ptes_to_fixes) + in + clean_goal_with_heq (Idmap.map prove_rec_hyp ptes_to_fixes) + do_prove dyn_infos g' + ) + ) + g + end + | _ -> assert false + ) g + in + tclTHENSEQ + [ + (fun g -> observe_tac "introducing params" (intro_with_remembrance params princ_info.nparams) g); + (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates princ_info.npredicates) g); + (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g); + (fun g -> observe_tac "declaring fix(es)" mk_fixes g); + (fun g -> + let nb_real_args = + let pte_app = snd (Sign.decompose_prod_assum (pf_concl g)) in + let pte = fst (decompose_app pte_app) in + try + let fix_info = Idmap.find (destVar pte) !pte_to_fix in + fix_info.nb_realargs + with Not_found -> (* Not a recursive function *) + nb_prod (pf_concl g) + in + observe_tac "" (tclTHEN + (tclDO nb_real_args (observe_tac "intro" intro)) + (fun g' -> + let realargs_ids = fst (list_chop ~msg:"args" nb_real_args (pf_ids_of_hyps g')) in + let do_prove_on_branches branches : tactic = + observe_tac "proving" (do_prove !pte_to_fix ( realargs_ids) branches) + in + observe_tac "instanciating rec hyps" + (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev realargs_ids)) + g' + )) + g + ) + ] + goal + + + +(* Proof of principles of general functions *) +let h_id = Recdef.h_id +and hrec_id = Recdef.hrec_id +and acc_inv_id = Recdef.acc_inv_id +and ltof_ref = Recdef.ltof_ref +and acc_rel = Recdef.acc_rel +and well_founded = Recdef.well_founded +and delayed_force = Recdef.delayed_force +and h_intros = Recdef.h_intros +and list_rewrite = Recdef.list_rewrite +and evaluable_of_global_reference = Recdef.evaluable_of_global_reference + +let prove_with_tcc tcc_lemma_constr eqs : tactic = + match !tcc_lemma_constr with + | None -> anomaly "No tcc proof !!" + | Some lemma -> + fun gls -> + let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in + tclTHENSEQ + [ + generalize [lemma]; + h_intro hid; + Elim.h_decompose_and (mkVar hid); + tclTRY(list_rewrite true eqs); + Eauto.gen_eauto false (false,5) [] (Some []) + ] + gls + + +let backtrack_eqs_until_hrec hrec eqs : tactic = + fun gls -> + let rewrite = + tclFIRST (List.map Equality.rewriteRL eqs ) + in + let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in + let f_app = array_last (snd (destApp hrec_concl)) in + let f = (fst (destApp f_app)) in + let rec backtrack : tactic = + fun g -> + let f_app = array_last (snd (destApp (pf_concl g))) in + match kind_of_term f_app with + | App(f',_) when eq_constr f' f -> tclIDTAC g + | _ -> tclTHEN rewrite backtrack g + in + backtrack gls + + + + + +let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = + match !tcc_lemma_constr with + | None -> tclIDTAC_MESSAGE (str "No tcc proof !!") + | Some lemma -> + fun gls -> + let hid = next_global_ident_away true Recdef.h_id (pf_ids_of_hyps gls) in + (tclTHENSEQ + [ + generalize [lemma]; + h_intro hid; + Elim.h_decompose_and (mkVar hid); + backtrack_eqs_until_hrec hrec eqs; + tclCOMPLETE (tclTHENS (* We must have exactly ONE subgoal !*) + (apply (mkVar hrec)) + [ tclTHENSEQ + [ + thin [hrec]; + apply (Lazy.force acc_inv); + (fun g -> + if is_mes + then + unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + else tclIDTAC g + ); + tclTRY(Recdef.list_rewrite true eqs); + observe_tac "finishing" (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some []))) + ] + ] + ) + ]) + gls + + +let is_valid_hypothesis predicates_name = + let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in + let is_pte typ = + if isApp typ + then + let pte,_ = destApp typ in + if isVar pte + then Idset.mem (destVar pte) predicates_name + else false + else false + in + let rec is_valid_hypothesis typ = + is_pte typ || + match kind_of_term typ with + | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' + | _ -> false + in + is_valid_hypothesis + +let fresh_id avoid na = + let id = + match na with + | Name id -> id + | Anonymous -> h_id + in + next_global_ident_away true id avoid + + +let prove_principle_for_gen + (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes + rec_arg_num rec_arg_type relation = + fun g -> + let type_of_goal = pf_concl g in + let goal_ids = pf_ids_of_hyps g in + let goal_elim_infos = Tactics.compute_elim_sig type_of_goal in + let params_names,ids = List.fold_left + (fun (params_names,avoid) (na,_,_) -> + let new_id = fresh_id avoid na in + (new_id::params_names,new_id::avoid) + ) + ([],goal_ids) + goal_elim_infos.params + in + let predicates_names,ids = + List.fold_left + (fun (predicates_names,avoid) (na,_,_) -> + let new_id = fresh_id avoid na in + (new_id::predicates_names,new_id::avoid) + ) + ([],ids) + goal_elim_infos.predicates + in + let branches_names,ids = + List.fold_left + (fun (branches_names,avoid) (na,_,_) -> + let new_id = fresh_id avoid na in + (new_id::branches_names,new_id::avoid) + ) + ([],ids) + goal_elim_infos.branches + in + let to_intro = params_names@predicates_names@branches_names in + let nparams = List.length params_names in + let rec_arg_num = rec_arg_num - nparams in + let tac_intro_static = h_intros to_intro in + let args_info = ref None in + let arg_tac g = (* introducing args *) + let ids = pf_ids_of_hyps g in + let func_body = def_of_const (mkConst functional_ref) in + (* let _ = Pp.msgnl (Printer.pr_lconstr func_body) in *) + let (f_name, _, body1) = destLambda func_body in + let f_id = + match f_name with + | Name f_id -> next_global_ident_away true f_id ids + | Anonymous -> anomaly "anonymous function" + in + let n_names_types,_ = decompose_lam body1 in + let n_ids,ids = + List.fold_left + (fun (n_ids,ids) (n_name,_) -> + match n_name with + | Name id -> + let n_id = next_global_ident_away true id ids in + n_id::n_ids,n_id::ids + | _ -> anomaly "anonymous argument" + ) + ([],(f_id::ids)) + n_names_types + in + let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in + let args_ids = snd (list_chop nparams n_ids) in + args_info := Some (ids,args_ids,rec_arg_id); + h_intros args_ids g + in + let wf_tac = + if is_mes + then + Recdef.tclUSER_if_not_mes + else fun _ -> prove_with_tcc tcc_lemma_ref [] + in + let start_tac g = + let ids,args_ids,rec_arg_id = out_some !args_info in + let nargs = List.length args_ids in + let pre_rec_arg = + List.rev_map + mkVar + (fst (list_chop (rec_arg_num - 1) args_ids)) + in + let args_before_rec = pre_rec_arg@(List.map mkVar params_names) in + let relation = substl args_before_rec relation in + let input_type = substl args_before_rec rec_arg_type in + let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in + let wf_rec_arg = + next_global_ident_away true + (id_of_string ("Acc_"^(string_of_id rec_arg_id))) + (wf_thm::ids) + in + let hrec = next_global_ident_away true hrec_id (wf_rec_arg::wf_thm::ids) in + let acc_inv = + lazy ( + mkApp ( + delayed_force acc_inv_id, + [|input_type;relation;mkVar rec_arg_id|] + ) + ) + in + (tclTHENS + (observe_tac + "first assert" + (assert_tac + true (* the assert thm is in first subgoal *) + (Name wf_rec_arg) + (mkApp (delayed_force acc_rel, + [|input_type;relation;mkVar rec_arg_id|]) + ) + ) + ) + [ + (* accesibility proof *) + tclTHENS + (observe_tac + "second assert" + (assert_tac + true + (Name wf_thm) + (mkApp (delayed_force well_founded,[|input_type;relation|])) + ) + ) + [ + (* interactive proof of the well_foundness of the relation *) + wf_tac is_mes; + (* well_foundness -> Acc for any element *) + observe_tac + "apply wf_thm" + (h_apply ((mkApp(mkVar wf_thm, + [|mkVar rec_arg_id |])),Rawterm.NoBindings) + ) + ] + ; + (* rest of the proof *) + tclTHENSEQ + [ + observe_tac "generalize" (fun g -> + let to_thin = + fst (list_chop ( nargs + 1) (pf_ids_of_hyps g)) + in + let to_thin_c = List.rev_map mkVar to_thin in + tclTHEN (generalize to_thin_c) (observe_tac "thin" (h_clear false to_thin)) g + ); + observe_tac "h_fix" (h_fix (Some hrec) (nargs+1)); + h_intros args_ids; + h_intro wf_rec_arg; + Equality.rewriteLR (mkConst eq_ref); + (fun g' -> + let body = + let _,args = destApp (pf_concl g') in + array_last args + in + let body_info rec_hyps = + { + nb_rec_hyps = List.length rec_hyps; + rec_hyps = rec_hyps; + eq_hyps = []; + info = body + } + in + let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar wf_rec_arg|]) ) in + let pte_info = + { proving_tac = + (fun eqs -> + observe_tac "prove_with_tcc" + (new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_ref (List.map mkVar eqs)) + ); + is_valid = is_valid_hypothesis predicates_names + } + in + let ptes_info : pte_info Idmap.t = + List.fold_left + (fun map pte_id -> + Idmap.add pte_id + pte_info + map + ) + Idmap.empty + predicates_names + in + let make_proof rec_hyps = + build_proof + false + [f_ref] + ptes_info + (body_info rec_hyps) + in + instanciate_hyps_with_args + make_proof + branches_names + args_ids + g' + + ) + ] + ] + g + ) + in + tclTHENSEQ + [tac_intro_static; + arg_tac; + start_tac + ] g + + + + + + + + + + + + + + + diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli new file mode 100644 index 0000000000..35da5d507a --- /dev/null +++ b/contrib/funind/functional_principles_proofs.mli @@ -0,0 +1,20 @@ +open Names +open Term + +val prove_princ_for_struct : + bool -> + int -> constant array -> constr array -> int -> Tacmach.tactic + + +val prove_principle_for_gen : + constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *) + constr option ref -> (* a pointer to the obligation proofs lemma *) + bool -> (* is that function uses measure *) + int -> (* the number of recursive argument *) + types -> (* the type of the recursive argument *) + constr -> (* the wf relation used to prove the function *) + Tacmach.tactic + + +val is_pte : rel_declaration -> bool +val do_observe : unit -> bool diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml new file mode 100644 index 0000000000..072c3d518d --- /dev/null +++ b/contrib/funind/functional_principles_types.ml @@ -0,0 +1,550 @@ +open Printer +open Util +open Term +open Termops +open Names +open Declarations +open Pp +open Entries +open Hiddentac +open Evd +open Tacmach +open Proof_type +open Tacticals +open Tactics +open Indfun_common +open Functional_principles_proofs + +exception Toberemoved_with_rel of int*constr +exception Toberemoved + + + + + +(* + Transform an inductive induction principle into + a functional one +*) +let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = + let princ_type_info = compute_elim_sig princ_type in + let env = Global.env () in + let change_predicate_sort i (x,_,t) = + let new_sort = sorts.(i) in + let args,_ = decompose_prod t in + let real_args = + if princ_type_info.indarg_in_concl + then List.tl args + else args + in + x,None,compose_prod real_args (mkSort new_sort) + in + let new_predicates = + list_map_i + change_predicate_sort + 0 + princ_type_info.predicates + in + let env_with_params_and_predicates = + Environ.push_rel_context + new_predicates + (Environ.push_rel_context + princ_type_info.params + env + ) + in + let rel_as_kn = + fst (match princ_type_info.indref with + | Some (Libnames.IndRef ind) -> ind + | _ -> failwith "Not a valid predicate" + ) + in + let pre_princ = + it_mkProd_or_LetIn + ~init: + (it_mkProd_or_LetIn + ~init:(option_fold_right + mkProd_or_LetIn + princ_type_info.indarg + princ_type_info.concl + ) + princ_type_info.args + ) + princ_type_info.branches + in + let is_dom c = + match kind_of_term c with + | Ind((u,_)) -> u = rel_as_kn + | Construct((u,_),_) -> u = rel_as_kn + | _ -> false + in + let get_fun_num c = + match kind_of_term c with + | Ind(_,num) -> num + | Construct((_,num),_) -> num + | _ -> assert false + in + let dummy_var = mkVar (id_of_string "________") in + let mk_replacement c i args = + let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in +(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) + res + in + let rec has_dummy_var t = + fold_constr + (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t)) + false + t + in + let rec compute_new_princ_type remove env pre_princ : types*(constr list) = + let (new_princ_type,_) as res = + match kind_of_term pre_princ with + | Rel n -> + begin + try match Environ.lookup_rel n env with + | _,_,t when is_dom t -> raise Toberemoved + | _ -> pre_princ,[] with Not_found -> assert false + end + | Prod(x,t,b) -> + compute_new_princ_type_for_binder remove mkProd env x t b + | Lambda(x,t,b) -> + compute_new_princ_type_for_binder remove mkLambda env x t b + | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved + | App(f,args) when is_dom f -> + let var_to_be_removed = destRel (array_last args) in + let num = get_fun_num f in + raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args)) + | App(f,args) -> + let is_pte = + match kind_of_term f with + | Rel n -> + is_pte (Environ.lookup_rel n env) + | _ -> false + in + let args = + if is_pte && remove + then array_get_start args + else args + in + let new_args,binders_to_remove = + Array.fold_right (compute_new_princ_type_with_acc remove env) + args + ([],[]) + in + let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in + applist(new_f, new_args), + list_union_eq eq_constr binders_to_remove_from_f binders_to_remove + | LetIn(x,v,t,b) -> + compute_new_princ_type_for_letin remove env x v t b + | _ -> pre_princ,[] + in +(* observennl ( *) +(* match kind_of_term pre_princ with *) +(* | Prod _ -> *) +(* str "compute_new_princ_type for "++ *) +(* pr_lconstr_env env pre_princ ++ *) +(* str" is "++ *) +(* pr_lconstr_env env new_princ_type ++ fnl () *) +(* | _ -> str "" *) +(* ); *) + res + + and compute_new_princ_type_for_binder remove bind_fun env x t b = + begin + try + let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in + let new_x : name = get_name (ids_of_context env) x in + let new_env = Environ.push_rel (x,None,t) env in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in + if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + else + ( + bind_fun(new_x,new_t,new_b), + list_union_eq + eq_constr + binders_to_remove_from_t + (List.map pop binders_to_remove_from_b) + ) + + with + | Toberemoved -> +(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in + new_b, List.map pop binders_to_remove_from_b + | Toberemoved_with_rel (n,c) -> +(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in + new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) + end + and compute_new_princ_type_for_letin remove env x v t b = + begin + try + let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in + let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in + let new_x : name = get_name (ids_of_context env) x in + let new_env = Environ.push_rel (x,Some v,t) env in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in + if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + else + ( + mkLetIn(new_x,new_v,new_t,new_b), + list_union_eq + eq_constr + (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) + (List.map pop binders_to_remove_from_b) + ) + + with + | Toberemoved -> +(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in + new_b, List.map pop binders_to_remove_from_b + | Toberemoved_with_rel (n,c) -> +(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in + new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) + end + and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = + let new_e,to_remove_from_e = compute_new_princ_type remove env e + in + new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc + in +(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *) + let pre_res,_ = + compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in + it_mkProd_or_LetIn + ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates) + princ_type_info.params + + + +let change_property_sort toSort princ princName = + let princ_info = compute_elim_sig princ in + let change_sort_in_predicate (x,v,t) = + (x,None, + let args,_ = decompose_prod t in + compose_prod args (mkSort toSort) + ) + in + let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in + let init = + let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in + mkApp(princName_as_constr, + Array.init nargs + (fun i -> mkRel (nargs - i ))) + in + it_mkLambda_or_LetIn + ~init: + (it_mkLambda_or_LetIn ~init + (List.map change_sort_in_predicate princ_info.predicates) + ) + princ_info.params + + +let pp_dur time time' = + str (string_of_float (System.time_difference time time')) + +(* End of things to be removed latter : just here to compare + saving proof with and without normalizing the proof +*) + +let qed () = Command.save_named true +let defined () = Command.save_named false +let generate_functional_principle + interactive_proof + old_princ_type sorts new_princ_name funs i proof_tac + = + let f = funs.(i) in + let type_sort = Termops.new_sort_in_family InType in + let new_sorts = + match sorts with + | None -> Array.make (Array.length funs) (type_sort) + | Some a -> a + in + (* First we get the type of the old graph principle *) + let mutr_nparams = (compute_elim_sig old_princ_type).nparams in + (* First we get the type of the old graph principle *) + let new_principle_type = + compute_new_princ_type_from_rel + (Array.map mkConst funs) + new_sorts + old_princ_type + in +(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) + let base_new_princ_name,new_princ_name = + match new_princ_name with + | Some (id) -> id,id + | None -> + let id_of_f = id_of_label (con_label f) in + id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + in + let names = ref [new_princ_name] in + let hook _ _ = + if sorts = None + then +(* let id_of_f = id_of_label (con_label f) in *) + let register_with_sort fam_sort = + let s = Termops.new_sort_in_family fam_sort in + let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in + let value = + change_property_sort s new_principle_type new_princ_name + in +(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let ce = + { const_entry_body = value; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() + } + in + ignore( + Declare.declare_constant + name + (Entries.DefinitionEntry ce, + Decl_kinds.IsDefinition (Decl_kinds.Scheme) + ) + ); + names := name :: !names + in + register_with_sort InProp; + register_with_sort InSet + in + begin + Command.start_proof + new_princ_name + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) + new_principle_type + hook + ; + try + let _tim1 = System.get_time () in + Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); + let _tim2 = System.get_time () in +(* begin *) +(* let dur1 = System.time_difference tim1 tim2 in *) +(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) +(* end; *) + let do_save = not (do_observe ()) && not interactive_proof in + let _ = + try +(* Vernacentries.show_script (); *) + Options.silently defined (); + let _dur2 = System.time_difference _tim2 (System.get_time ()) in +(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *) + Options.if_verbose + (fun () -> + Pp.msgnl ( + prlist_with_sep + (fun () -> str" is defined " ++ fnl ()) + Ppconstr.pr_id + (List.rev !names) ++ str" is defined " + ) + ) + () + with e when do_save -> + msg_warning + ( + Cerrors.explain_exn e + ); + if not (do_observe ()) + then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end + in + () + +(* let tim3 = Sys.time () in *) +(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *) + + with + | e -> + msg_warning + ( + Cerrors.explain_exn e + ); + if not ( do_observe ()) + then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end + end + + + + +exception Not_Rec + +let get_funs_constant mp dp = + let rec get_funs_constant const e : (Names.constant*int) array = + match kind_of_term (snd (decompose_lam e)) with + | Fix((_,(na,_,_))) -> + Array.mapi + (fun i na -> + match na with + | Name id -> + let const = make_con mp dp (label_of_id id) in + const,i + | Anonymous -> + anomaly "Anonymous fix" + ) + na + | _ -> [|const,0|] + in + function const -> + let find_constant_body const = + match (Global.lookup_constant const ).const_body with + | Some b -> + let body = force b in + let body = Tacred.cbv_norm_flags + (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (Global.env ()) + (Evd.empty) + body + in + body + | None -> error ( "Cannot define a principle over an axiom ") + in + let f = find_constant_body const in + let l_const = get_funs_constant const f in + (* + We need to check that all the functions found are in the same block + to prevent Reset stange thing + *) + let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in + let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in + (* all the paremeter must be equal*) + let _check_params = + let first_params = List.hd l_params in + List.iter + (fun params -> + if not ((=) first_params params) + then error "Not a mutal recursive block" + ) + l_params + in + (* The bodies has to be very similar *) + let _check_bodies = + try + let extract_info is_first body = + match kind_of_term body with + | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) + | _ -> + if is_first && (List.length l_bodies = 1) + then raise Not_Rec + else error "Not a mutal recursive block" + in + let first_infos = extract_info true (List.hd l_bodies) in + let check body = (* Hope this is correct *) + if not (first_infos = (extract_info false body)) + then error "Not a mutal recursive block" + in + List.iter check l_bodies + with Not_Rec -> () + in + l_const + +let make_scheme fas = + let env = Global.env () + and sigma = Evd.empty in + let id_to_constr id = + Tacinterp.constr_of_id env id + in + let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in + let first_fun = destConst (List.hd funs) in + let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in + let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in + let first_fun_kn = + (* Fixme: take into accour funs_mp and funs_dp *) + fst (destInd (id_to_constr first_fun_rel_id)) + in + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in + let this_block_funs = Array.map fst this_block_funs_indexes in + let prop_sort = InProp in + let funs_indexes = + let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + List.map + (function const -> List.assoc (destConst const) this_block_funs_indexes) + funs + in + let ind_list = + List.map + (fun (idx) -> + let ind = first_fun_kn,idx in + let (mib,mip) = Global.lookup_inductive ind in + ind,mib,mip,true,prop_sort + ) + funs_indexes + in + let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in + let i = ref (-1) in + let sorts = + List.rev_map (fun (_,_,x) -> + Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) + ) + fas + in + let princ_names = List.map (fun (x,_,_) -> x) fas in + let _ = List.map2 + (fun princ_name scheme_type -> + incr i; +(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) +(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) +(* ); *) + generate_functional_principle + false + scheme_type + (Some (Array.of_list sorts)) + (Some princ_name) + this_block_funs + !i + (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs))) + ) + princ_names + l_schemes + in + () + +let make_case_scheme fa = + let env = Global.env () + and sigma = Evd.empty in + let id_to_constr id = + Tacinterp.constr_of_id env id + in + let funs = (fun (_,f,_) -> id_to_constr f) fa in + let first_fun = destConst funs in + let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in + let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in + let first_fun_kn = + (* Fixme: take into accour funs_mp and funs_dp *) + fst (destInd (id_to_constr first_fun_rel_id)) + in + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in + let this_block_funs = Array.map fst this_block_funs_indexes in + let prop_sort = InProp in + let funs_indexes = + let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + List.assoc (destConst funs) this_block_funs_indexes + in + let ind_fun = + let ind = first_fun_kn,funs_indexes in + ind,prop_sort + in + let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in + let sorts = + (fun (_,_,x) -> + Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) + ) + fa + in + let princ_name = (fun (x,_,_) -> x) fa in + let _ = +(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) +(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) +(* ); *) + generate_functional_principle + false + scheme_type + (Some ([|sorts|])) + (Some princ_name) + this_block_funs + 0 + (prove_princ_for_struct false 0 [|destConst funs|]) + in + () diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli new file mode 100644 index 0000000000..929c3db510 --- /dev/null +++ b/contrib/funind/functional_principles_types.mli @@ -0,0 +1,28 @@ +open Names +open Term +val generate_functional_principle : + (* do we accept interactive proving *) + bool -> + (* induction principle on rel *) + types -> + (* *) + sorts array option -> + (* Name of the new principle *) + (identifier) option -> + (* the compute functions to use *) + constant array -> + (* We prove the nth- principle *) + int -> + (* The tactic to use to make the proof w.r + the number of params + *) + (constr array -> int -> Tacmach.tactic) -> + unit + + + +val compute_new_princ_type_from_rel : constr array -> sorts array -> + types -> types + +val make_scheme : (identifier*identifier*Rawterm.rawsort) list -> unit +val make_case_scheme : (identifier*identifier*Rawterm.rawsort) -> unit diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 81527912dc..f65c94752e 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -1,7 +1,6 @@ open Util open Names open Term - open Pp open Indfun_common open Libnames @@ -29,6 +28,11 @@ let interp_casted_constr_with_implicits sigma env impls c = Constrintern.intern_gen false sigma env ~impls:([],impls) ~allow_soapp:false ~ltacvars:([],[]) c + +(* + Construct a fixpoint as a Rawterm + and not as a constr +*) let build_newrecursive (lnameargsardef) = let env0 = Global.env() @@ -78,6 +82,7 @@ let compute_annot (name,annot,args,types,body) = | Some r -> (name,r,args,types,body) +(* Checks whether or not the mutual bloc is recursive *) let rec is_rec names = let names = List.fold_right Idset.add names Idset.empty in let check_id id names = Idset.mem id names in @@ -85,7 +90,7 @@ let rec is_rec names = | RVar(_,id) -> check_id id names | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false | RCast(_,b,_,_) -> lookup names b - | RRec _ -> assert false + | RRec _ -> error "RRec not handled" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) -> @@ -143,7 +148,7 @@ let generate_principle let princ_type = (Global.lookup_constant princ).Declarations.const_type in - New_arg_principle.generate_functional_principle + Functional_principles_types.generate_functional_principle interactive_proof princ_type None @@ -175,12 +180,12 @@ let register_struct is_rec fixpoint_exprl = | _ -> Command.build_recursive fixpoint_exprl (Options.boxed_definitions()) - -let generate_correction_proof_wf tcc_lemma_ref - is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation +let generate_correction_proof_wf f_ref tcc_lemma_ref + is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = - Recdef.prove_principle tcc_lemma_ref - is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation + Functional_principles_proofs.prove_principle_for_gen + (f_ref,functional_ref,eq_ref) + tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body @@ -218,11 +223,11 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body [(f_app_args,None);(body,None)]) in let eq = Command.generalize_constr_expr unbounded_eq args in - let hook tcc_lemma_ref f_ref eq_ref rec_arg_num rec_arg_type nb_args relation = + let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation = try pre_hook - (generate_correction_proof_wf tcc_lemma_ref is_mes - f_ref eq_ref rec_arg_num rec_arg_type nb_args relation + (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes + functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); Command.save_named true with e -> @@ -351,7 +356,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = recdefs interactive_proof true - (New_arg_principle.prove_princ_for_struct interactive_proof); + (Functional_principles_proofs.prove_princ_for_struct interactive_proof); true in diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index a238de895b..c4f0c0ad6f 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -61,8 +61,7 @@ let is_rec scheme_info = let choose_dest_or_ind scheme_info = if is_rec scheme_info then Tactics.new_induct - else - Tactics.new_destruct + else Tactics.new_destruct TACTIC EXTEND newfunind @@ -178,7 +177,7 @@ END VERNAC COMMAND EXTEND NewFunctionalScheme ["New" "Functional" "Scheme" fun_scheme_args(fas) ] -> [ - New_arg_principle.make_scheme fas + Functional_principles_types.make_scheme fas ] END @@ -186,7 +185,7 @@ END VERNAC COMMAND EXTEND NewFunctionalCase ["New" "Functional" "Case" fun_scheme_arg(fas) ] -> [ - New_arg_principle.make_case_scheme fas + Functional_principles_types.make_case_scheme fas ] END diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml deleted file mode 100644 index 12a43b5dbc..0000000000 --- a/contrib/funind/new_arg_principle.ml +++ /dev/null @@ -1,1770 +0,0 @@ -open Printer -open Util -open Term -open Termops -open Names -open Declarations -open Pp -open Entries -open Hiddentac -open Evd -open Tacmach -open Proof_type -open Tacticals -open Tactics -open Indfun_common - - -let msgnl = Pp.msgnl - -let do_observe () = - Tacinterp.get_debug () <> Tactic_debug.DebugOff - - -let observe strm = - if do_observe () - then Pp.msgnl strm - else () - -let observennl strm = - if do_observe () - then begin Pp.msg strm;Pp.pp_flush () end - else () - - - - -let do_observe_tac s tac g = - try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v - with e -> - let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in - msgnl (str "observation "++str s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); - raise e;; - - -let observe_tac s tac g = - if do_observe () - then do_observe_tac s tac g - else tac g - - -let tclTRYD tac = - if !Options.debug || do_observe () - then (fun g -> try (* do_observe_tac "" *)tac g with _ -> tclIDTAC g) - else tac - - -let list_chop ?(msg="") n l = - try - list_chop n l - with Failure (msg') -> - failwith (msg ^ msg') - - -let make_refl_eq type_of_t t = - let refl_equal_term = Lazy.force refl_equal in - mkApp(refl_equal_term,[|type_of_t;t|]) - - -type static_fix_info = - { - idx : int; - name : identifier; - types : types; - nb_realargs : int - } - -type static_infos = - { - fixes_ids : identifier list; - ptes_to_fixes : static_fix_info Idmap.t - } - -type 'a dynamic_info = - { - nb_rec_hyps : int; - rec_hyps : identifier list ; - eq_hyps : identifier list; - info : 'a - } - -let finish_proof dynamic_infos g = - observe_tac "finish" - h_assumption - g - - -let refine c = - Tacmach.refine_no_check c - -let thin l = - Tacmach.thin_no_check l - - -let cut_replacing id t tac :tactic= - tclTHENS (cut t) - [ tclTHEN (thin_no_check [id]) (introduction_no_check id); - tac - ] - -let intro_erasing id = tclTHEN (thin [id]) (introduction id) - - - -let rec_hyp_id = id_of_string "rec_hyp" - -let is_trivial_eq t = - match kind_of_term t with - | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> - eq_constr t1 t2 - | _ -> false - - -let rec incompatible_constructor_terms t1 t2 = - let c1,arg1 = decompose_app t1 - and c2,arg2 = decompose_app t2 - in - (not (eq_constr t1 t2)) && - isConstruct c1 && isConstruct c2 && - ( - not (eq_constr c1 c2) || - List.exists2 incompatible_constructor_terms arg1 arg2 - ) - -let is_incompatible_eq t = - match kind_of_term t with - | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> - incompatible_constructor_terms t1 t2 - | _ -> false - -let change_hyp_with_using hyp_id t tac = - fun g -> - let prov_id = pf_get_new_id hyp_id g in - tclTHENLIST - [ - forward (Some tac) (Genarg.IntroIdentifier prov_id) t; - thin [hyp_id]; - h_rename prov_id hyp_id - ] g - -exception TOREMOVE - - -let prove_trivial_eq h_id context (type_of_term,term) = - let nb_intros = List.length context in - tclTHENLIST - [ - tclDO nb_intros intro; (* introducing context *) - (fun g -> - let context_hyps = - fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) - in - let context_hyps' = - (mkApp(Lazy.force refl_equal,[|type_of_term;term|])):: - (List.map mkVar context_hyps) - in - let to_refine = applist(mkVar h_id,List.rev context_hyps') in - refine to_refine g - ) - ] - - -let isAppConstruct t = - if isApp t - then isConstruct (fst (destApp t)) - else false - - -let nf_betaoiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta - -let remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 = - let rel_num = destRel t2 in - - let nb_kept = List.length context - rel_num - and nb_popped = rel_num - 1 - in - - (* We remove the equation *) - let new_end_of_type = pop end_of_type in - - let lt_relnum,ge_relnum = - list_chop - ~msg:("removing useless variable "^(string_of_int rel_num)^" :") - nb_popped - context - in - (* we rebuilt the type of hypothesis after the rel to remove *) - let hyp_type_lt_relnum = - it_mkProd_or_LetIn ~init:new_end_of_type lt_relnum - in - (* we replace Rel 1 by t1 *) - let new_hyp_type_lt_relnum = subst1 t1 hyp_type_lt_relnum in - (* we resplit the type of hyp_type *) - let new_lt_relnum,new_end_of_type = - Sign.decompose_prod_n_assum nb_popped new_hyp_type_lt_relnum - in - (* and rebuilt new context of hyp *) - let new_context = new_lt_relnum@(List.tl ge_relnum) in - let new_typ_of_hyp = - nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type new_context) - in - let prove_simpl_eq = - tclTHENLIST - [ - tclDO (nb_popped + nb_kept) intro; - (fun g' -> - let new_hyps_ids = pf_ids_of_hyps g' in - let popped_ids,others = - list_chop ~msg:"removing useless variable pop :" - nb_popped new_hyps_ids in - let kept_ids,_ = - list_chop ~msg: " removing useless variable kept : " - nb_kept others - in - let rev_to_apply = - (mkApp(Lazy.force refl_equal,[|Typing.type_of env sigma t1;t1|])):: - ((List.map mkVar popped_ids)@ - (t1:: - (List.map mkVar kept_ids))) - in - let to_refine = applist(mkVar hyp_id,List.rev rev_to_apply) in - refine to_refine g' - ) - ] - in - let simpl_eq_tac = change_hyp_with_using hyp_id new_typ_of_hyp - (observe_tac "prove_simpl_eq" prove_simpl_eq) - in - let new_end_of_type = nf_betaoiotazeta new_end_of_type in - (new_context,new_end_of_type,simpl_eq_tac),new_typ_of_hyp, - (str " removing useless variable " ++ str (string_of_int rel_num) ) - - -let decompose_eq env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 = - let c1,args1 = destApp t1 - and c2,args2 = destApp t2 - in - (* This tactic must be used after is_incompatible_eq *) - assert (eq_constr c1 c2); - (* we remove this equation *) - let new_end_of_type = pop end_of_type in - let new_eqs = - array_map2_i - (fun i arg1 arg2 -> - let new_eq = - let type_of_arg = Typing.type_of env sigma arg1 in - mkApp(Lazy.force eq,[|type_of_arg;arg1;arg2|]) - in - Anonymous,None,lift i new_eq - ) - args1 - args2 - in - let nb_new_eqs = Array.length new_eqs in - (* we add the new equation *) - let new_end_of_type = lift nb_new_eqs new_end_of_type in - let local_context = - List.rev (Array.to_list new_eqs) in - let new_end_of_type = it_mkProd_or_LetIn ~init:new_end_of_type local_context in - let new_typ_of_hyp = - nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type context) - in - let prove_pattern_simplification = - let context_length = List.length context in - tclTHENLIST - [ - tclDO (context_length + nb_new_eqs) intro ; - (fun g -> - let new_eqs,others = - list_chop ~msg:"simplifying pattern : new_eqs" nb_new_eqs (pf_hyps g) - in - let context_hyps,_ = list_chop ~msg:"simplifying pattern : context_hyps" - context_length others in - let eq_args = - List.rev_map - (fun (_,_, eq) -> let _,args = destApp eq in args.(1),args.(2)) - new_eqs - in - let lhs_args,rhs_args = List.split eq_args in - let lhs_eq = applist(c1,lhs_args) - and rhs_eq = applist(c1,rhs_args) - in - let type_of_eq = pf_type_of g lhs_eq in - let eq_to_assert = - mkApp(Lazy.force eq,[|type_of_eq;lhs_eq;rhs_eq|]) - in - let prove_new_eq = - tclTHENLIST [ - tclMAP - (fun (id,_,_) -> - (* The tclTRY here is used when trying to rewrite - on Set - eg (@cons A x l)=(@cons A x' l') generates 3 eqs - A=A -> x=x' -> l = l' ... - - *) - tclTRY (Equality.rewriteLR (mkVar id)) - ) - new_eqs; - reflexivity - ] - in - let new_eq_id = pf_get_new_id (id_of_string "H") g in - let create_new_eq = - forward - (Some (observe_tac "prove_new_eq" (prove_new_eq))) - (Genarg.IntroIdentifier new_eq_id) - eq_to_assert - in - let to_refine = - applist ( - mkVar hyp_id, - List.rev ((mkVar new_eq_id):: - (List.map (fun (id,_,_) -> mkVar id) context_hyps))) - in - tclTHEN - (observe_tac "create_new_eq" create_new_eq ) - (observe_tac "refine in decompose_eq " (refine to_refine)) - g - ) - ] - in - let simpl_eq_tac = - change_hyp_with_using hyp_id new_typ_of_hyp (observe_tac "prove_pattern_simplification " prove_pattern_simplification) - in - (context,nf_betaoiotazeta new_end_of_type,simpl_eq_tac),new_typ_of_hyp, - str "simplifying an equation " - -let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = - if not (noccurn 1 end_of_type) - then (* if end_of_type depends on this term we don't touch it *) - begin - observe (str "Not treating " ++ pr_lconstr t ); - failwith "NoChange"; - end; - let res,new_typ_of_hyp,msg = - if not (isApp t) then failwith "NoChange"; - let f,args = destApp t in - if not (eq_constr f (Lazy.force eq)) then failwith "NoChange"; - let t1 = args.(1) - and t2 = args.(2) - in - if isRel t2 && closed0 t1 then (* closed_term = x with x bound in context *) - begin - remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 - end - else if isAppConstruct t1 && isAppConstruct t2 (* C .... = C .... *) - then decompose_eq env sigma hyp_id context t end_of_type t1 t2 - else failwith "NoChange" - in - observe (str "In " ++ Ppconstr.pr_id hyp_id ++ - msg ++ fnl ()++ - str "old_typ_of_hyp :=" ++ - Printer.pr_lconstr_env - env - (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) - ++ fnl () ++ - str "new_typ_of_hyp := "++ - Printer.pr_lconstr_env env new_typ_of_hyp ++ fnl ()); - (res:'a*'b*'c) - - - - -let is_property static_info t_x = - if isApp t_x - then - let pte,args = destApp t_x in - if isVar pte && array_for_all closed0 args - then Idmap.mem (destVar pte) static_info.ptes_to_fixes - else false - else false - -let isLetIn t = - match kind_of_term t with - | LetIn _ -> true - | _ -> false - - -let h_reduce_with_zeta = - h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) - - - -let rewrite_until_var arg_num eq_ids : tactic = - let test_var g = - let _,args = destApp (pf_concl g) in - isVar args.(arg_num) - in - let rec do_rewrite eq_ids g = - if test_var g - then tclIDTAC g - else - match eq_ids with - | [] -> anomaly "Cannot find a way to prove recursive property"; - | eq_id::eq_ids -> - tclTHEN - (tclTRY (Equality.rewriteRL (mkVar eq_id))) - (do_rewrite eq_ids) - g - in - do_rewrite eq_ids - -let prove_rec_hyp eq_hyps fix_info = - tclTHEN - (rewrite_until_var (fix_info.idx - 1) eq_hyps) - (fun g -> - let _,pte_args = destApp (pf_concl g) in - let rec_hyp_proof = - mkApp(mkVar fix_info.name,array_get_start pte_args) - in - refine rec_hyp_proof g - ) - - - - - -let rec_pte_id = id_of_string "Hrec" -let clean_hyp_with_heq static_infos eq_hyps hyp_id env sigma = - let coq_False = Coqlib.build_coq_False () in - let coq_True = Coqlib.build_coq_True () in - let coq_I = Coqlib.build_coq_I () in - let rec scan_type context type_of_hyp : tactic = - if isLetIn type_of_hyp then - let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in - let reduced_type_of_hyp = nf_betaoiotazeta real_type_of_hyp in - (* length of context didn't change ? *) - let new_context,new_typ_of_hyp = - Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp - in - tclTHENLIST - [ - h_reduce_with_zeta - (Tacticals.onHyp hyp_id) - ; - scan_type new_context new_typ_of_hyp - - ] - else if isProd type_of_hyp - then - begin - let (x,t_x,t') = destProd type_of_hyp in - if is_property static_infos t_x then - begin - let pte,pte_args = (destApp t_x) in - let fix_info = Idmap.find (destVar pte) static_infos.ptes_to_fixes in - let popped_t' = pop t' in - let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in - let prove_new_type_of_hyp = - let context_length = List.length context in - tclTHENLIST - [ - tclDO context_length intro; - (fun g -> - let context_hyps_ids = - fst (list_chop ~msg:"rec hyp : context_hyps" - context_length (pf_ids_of_hyps g)) - in - let rec_pte_id = pf_get_new_id rec_pte_id g in - let to_refine = - applist(mkVar hyp_id, - List.rev_map mkVar (rec_pte_id::context_hyps_ids) - ) - in - tclTHENLIST - [ - forward - (Some (prove_rec_hyp eq_hyps fix_info)) - (Genarg.IntroIdentifier rec_pte_id) - t_x; - refine to_refine - ] - g - ) - ] - in - tclTHENLIST - [ - observe_tac "hyp rec" - (change_hyp_with_using hyp_id real_type_of_hyp prove_new_type_of_hyp); - scan_type context popped_t' - ] - end - else if eq_constr t_x coq_False then - begin - observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ - str " since it has False in its preconds " - ); - raise TOREMOVE; (* False -> .. useless *) - end - else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) - else if eq_constr t_x coq_True (* Trivial => we remove this precons *) - then - let _ = - observe (str "In "++Ppconstr.pr_id hyp_id++ - str " removing useless precond True" - ) - in - let popped_t' = pop t' in - let real_type_of_hyp = - it_mkProd_or_LetIn ~init:popped_t' context - in - let prove_trivial = - let nb_intro = List.length context in - tclTHENLIST [ - tclDO nb_intro intro; - (fun g -> - let context_hyps = - fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) - in - let to_refine = - applist (mkVar hyp_id, - List.rev (coq_I::List.map mkVar context_hyps) - ) - in - refine to_refine g - ) - ] - in - tclTHENLIST[ - change_hyp_with_using hyp_id real_type_of_hyp (observe_tac "prove_trivial" prove_trivial); - scan_type context popped_t' - ] - else if is_trivial_eq t_x - then (* t_x := t = t => we remove this precond *) - let popped_t' = pop t' in - let real_type_of_hyp = - it_mkProd_or_LetIn ~init:popped_t' context - in - let _,args = destApp t_x in - tclTHENLIST - [ - change_hyp_with_using - hyp_id - real_type_of_hyp - (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1)))); - scan_type context popped_t' - ] - else - begin - try - let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in - tclTHEN - tac - (scan_type new_context new_t') - with Failure "NoChange" -> - (* Last thing todo : push the rel in the context and continue *) - scan_type ((x,None,t_x)::context) t' - end - end - else - tclIDTAC - in - try - scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id] - with TOREMOVE -> - thin [hyp_id],[] - - -let clean_goal_with_heq static_infos continue_tac dyn_infos = - fun g -> - let env = pf_env g - and sigma = project g - in - let tac,new_hyps = - List.fold_left ( - fun (hyps_tac,new_hyps) hyp_id -> - let hyp_tac,new_hyp = - clean_hyp_with_heq static_infos dyn_infos.eq_hyps hyp_id env sigma - in - (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps - ) - (tclIDTAC,[]) - dyn_infos.rec_hyps - in - let new_infos = - { dyn_infos with - rec_hyps = new_hyps; - nb_rec_hyps = List.length new_hyps - } - in - tclTHENLIST - [ - tac ; - (continue_tac new_infos) - ] - g - -let heq_id = id_of_string "Heq" - -let treat_new_case static_infos nb_prod continue_tac term dyn_infos = - fun g -> - let heq_id = pf_get_new_id heq_id g in - let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in - tclTHENLIST - [ - (* We first introduce the variables *) - tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps); - (* Then the equation itself *) - introduction_no_check heq_id; - (* Then the new hypothesis *) - tclMAP introduction_no_check dyn_infos.rec_hyps; - observe_tac "after_introduction" (fun g' -> - (* We get infos on the equations introduced*) - let new_term_value_eq = pf_type_of g' (mkVar heq_id) in - (* compute the new value of the body *) - let new_term_value = - match kind_of_term new_term_value_eq with - | App(f,[| _;_;args2 |]) -> args2 - | _ -> - observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++ - pr_lconstr_env (pf_env g') new_term_value_eq - ); - assert false - in - let fun_body = - mkLambda(Anonymous, - pf_type_of g' term, - replace_term term (mkRel 1) dyn_infos.info - ) - in - let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in - let new_infos = - {dyn_infos with - info = new_body; - eq_hyps = heq_id::dyn_infos.eq_hyps - } - in - clean_goal_with_heq static_infos continue_tac new_infos g' - ) - ] - g - - -let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = - let args = Array.of_list (List.map mkVar args_id) in - let instanciate_one_hyp hid = - tclORELSE - ( (* we instanciate the hyp if possible *) - fun g -> - let prov_hid = pf_get_new_id hid g in - tclTHENLIST[ - forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); - thin [hid]; - h_rename prov_hid hid - ] g - ) - ( (* - if not then we are in a mutual function block - and this hyp is a recursive hyp on an other function. - - We are not supposed to use it while proving this - principle so that we can trash it - - *) - (fun g -> - observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); - thin [hid] g - ) - ) - in - if args_id = [] - then - tclTHENLIST [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; - do_prove hyps - ] - else - tclTHENLIST - [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; - tclMAP instanciate_one_hyp hyps; - (fun g -> - let all_g_hyps_id = - List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty - in - let remaining_hyps = - List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps - in - do_prove remaining_hyps g - ) - ] - - -let do_prove_princ_for_struct - (interactive_proof:bool) - (fnames:constant list) - static_infos -(* (ptes:identifier list) *) -(* (fixes:(int*constr*identifier*constr) Idmap.t) *) -(* (hyps: identifier list) *) -(* (term:constr) *) - dyn_infos - : tactic = -(* let fixes_ids = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *) - let rec do_prove_princ_for_struct_aux do_finalize dyn_infos : tactic = - fun g -> -(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match kind_of_term dyn_infos.info with - | Case(_,_,t,_) -> - let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in - let term_eq = - make_refl_eq type_of_term t - in - tclTHENSEQ - [ - h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps); - thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; - h_simplest_case t; - (fun g' -> - let g'_nb_prod = nb_prod (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - static_infos - nb_instanciate_partial - (do_prove_princ_for_struct do_finalize) - t - dyn_infos) - g' - ) - - ] g - | Lambda(n,t,b) -> - begin - match kind_of_term( pf_concl g) with - | Prod _ -> - tclTHEN - intro - (fun g' -> - let (id,_,_) = pf_last_hyp g' in - let new_term = - pf_nf_betaiota g' - (mkApp(dyn_infos.info,[|mkVar id|])) - in - let new_infos = {dyn_infos with info = new_term} in - let do_prove new_hyps = - do_prove_princ_for_struct do_finalize - {new_infos with - rec_hyps = new_hyps; - nb_rec_hyps = List.length new_hyps - } - in - observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' - (* do_prove_princ_for_struct do_finalize new_infos g' *) - ) g - | _ -> - do_finalize dyn_infos g - end - | Cast(t,_,_) -> - do_prove_princ_for_struct do_finalize {dyn_infos with info = t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> - do_finalize dyn_infos g - | App(_,_) -> - let f,args = decompose_app dyn_infos.info in - begin - match kind_of_term f with - | App _ -> assert false (* we have collected all the app in decompose_app *) - | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> - let new_infos = - { dyn_infos with - info = (f,args) - } - in - do_prove_princ_for_struct_args do_finalize new_infos g - | Const c when not (List.mem c fnames) -> - let new_infos = - { dyn_infos with - info = (f,args) - } - in -(* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) - do_prove_princ_for_struct_args do_finalize new_infos g - | Const _ -> - do_finalize dyn_infos g - | Lambda _ -> - let new_term = Reductionops.nf_beta dyn_infos.info in - do_prove_princ_for_struct do_finalize {dyn_infos with info = new_term} - g - | LetIn _ -> - let new_infos = - { dyn_infos with info = nf_betaoiotazeta dyn_infos.info } - in - - tclTHENLIST - [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) - dyn_infos.rec_hyps; - h_reduce_with_zeta Tacticals.onConcl; - do_prove_princ_for_struct do_finalize new_infos - ] - g - | Cast(b,_,_) -> - do_prove_princ_for_struct do_finalize {dyn_infos with info = b } g - | Case _ | Fix _ | CoFix _ -> - let new_finalize dyn_infos = - let new_infos = - { dyn_infos with - info = dyn_infos.info,args - } - in - do_prove_princ_for_struct_args do_finalize new_infos - in - do_prove_princ_for_struct new_finalize {dyn_infos with info = f } g - end - | Fix _ | CoFix _ -> - error ( "Anonymous local (co)fixpoints are not handled yet") - - | Prod _ -> assert false - | LetIn _ -> - let new_infos = - { dyn_infos with - info = nf_betaoiotazeta dyn_infos.info - } - in - - tclTHENLIST - [tclMAP - (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) - dyn_infos.rec_hyps; - h_reduce_with_zeta Tacticals.onConcl; - do_prove_princ_for_struct do_finalize new_infos - ] g - | Rel _ -> anomaly "Free var in goal conclusion !" - and do_prove_princ_for_struct do_finalize dyn_infos g = -(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *) - (do_prove_princ_for_struct_aux do_finalize dyn_infos) g - and do_prove_princ_for_struct_args do_finalize dyn_infos (* f_args' args *) :tactic = - fun g -> -(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) -(* then msgnl (str "do_prove_princ_for_struct_args with " ++ *) -(* pr_lconstr_env (pf_env g) f_args' *) -(* ); *) - let (f_args',args) = dyn_infos.info in - let tac : tactic = - fun g -> - match args with - | [] -> - do_finalize {dyn_infos with info = f_args'} g - | arg::args -> - observe (str "do_prove_princ_for_struct_args with arg := "++ pr_lconstr_env (pf_env g) arg++ - fnl () ++ - pr_goal (Tacmach.sig_it g) - ); - let do_finalize dyn_infos = - let new_arg = dyn_infos.info in - (* tclTRYD *) - (do_prove_princ_for_struct_args - do_finalize - {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} - ) - in - do_prove_princ_for_struct do_finalize - {dyn_infos with info = arg } - g - in - observe_tac "do_prove_princ_for_struct_args" (tac ) g - in - let do_finish_proof dyn_infos = - (* tclTRYD *) (clean_goal_with_heq - static_infos - finish_proof dyn_infos) - in - observe_tac "do_prove_princ_for_struct" - (do_prove_princ_for_struct do_finish_proof dyn_infos) - -let is_pte_type t = - isSort (snd (decompose_prod t)) - -let is_pte (_,_,t) = is_pte_type t - -exception Not_Rec - - - - -let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic = - fun goal -> -(* observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++ *) -(* pr_lconstr (mkConst fnames.(fun_num))); *) - let princ_type = pf_concl goal in - let princ_info = compute_elim_sig princ_type in - let get_body const = - match (Global.lookup_constant const ).const_body with - | Some b -> - let body = force b in - Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) - (Global.env ()) - (Evd.empty) - body - | None -> error ( "Cannot define a principle over an axiom ") - in - let fbody = get_body fnames.(fun_num) in - let params : identifier list ref = ref [] in - let predicates : identifier list ref = ref [] in - let args : identifier list ref = ref [] in - let branches : identifier list ref = ref [] in - let pte_to_fix = ref Idmap.empty in - let fbody_with_params = ref None in - let intro_with_remembrance ref number : tactic = - tclTHEN - ( tclDO number intro ) - (fun g -> - let last_n = list_chop number (pf_hyps g) in - ref := List.map (fun (id,_,_) -> id) (fst last_n)@ !ref; - tclIDTAC g - ) - in - let rec partial_combine body params = - match kind_of_term body,params with - | Lambda (x,t,b),param::params -> - partial_combine (subst1 param b) params - | Fix(infos),_ -> - body,params, Some (infos) - | _ -> body,params,None - in - let build_pte_to_fix (offset:int) params predicates - ((idxs,fix_num),(na,typearray,ca)) (avoid,_) = -(* let true_params,_ = list_chop offset params in *) - let true_params = List.rev params in - let avoid = ref avoid in - let res = list_fold_left_i - (fun i acc pte_id -> - let this_fix_id = fresh_id !avoid "fix___" in - avoid := this_fix_id::!avoid; -(* let this_body = substl (List.rev fnames_as_constr) ca.(i) in *) - let realargs,_ = decompose_lam ca.(i) in - let n_realargs = List.length realargs - List.length params in - observe (str "n_realargs := " ++ str (string_of_int n_realargs)); - observe (str "n_fix := " ++ str (string_of_int(Array.length ca))); - observe (str "body := " ++ pr_lconstr ca.(i)); - - let new_type = prod_applist typearray.(i) true_params in - let new_type_args,_ = decompose_prod new_type in - let nargs = List.length new_type_args in - let pte_args = - (* let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in *) - let f = applist((* all_funs *)mkConst fnames.(i),true_params) in - let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in - (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f] - in - let app_pte = applist(mkVar pte_id,pte_args) in - let new_type = compose_prod new_type_args app_pte in - - let fix_info = - { - idx = idxs.(i) - offset + 1; - name = this_fix_id; - types = new_type; - nb_realargs = n_realargs - } - in - pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix; - fix_info::acc - ) - 0 - [] - predicates - in - !avoid,List.rev res - in - let mk_fixes : tactic = - fun g -> - let body_p,params',fix_infos = - partial_combine fbody (List.rev_map mkVar !params) - in - fbody_with_params := Some body_p; - let offset = List.length params' in - let not_real_param,true_params = - list_chop - ((List.length !params ) - offset) - !params - in - params := true_params; args := not_real_param; -(* observe (str "mk_fixes : params are "++ *) -(* prlist_with_sep spc *) -(* (fun id -> pr_lconstr (mkVar id)) *) -(* !params *) -(* ); *) - let new_avoid,infos = - option_fold_right - (build_pte_to_fix - offset - (List.map mkVar !params) - (List.rev !predicates) - ) - fix_infos - ((pf_ids_of_hyps g),[]) - in - let pre_info,infos = list_chop fun_num infos in - match pre_info,infos with - | [],[] -> tclIDTAC g - | _,this_fix_info::infos' -> - let other_fix_info = - List.map - (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types) - (pre_info@infos') - in - tclORELSE - (h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info) - (tclFAIL 1000 (str "bad index" ++ - str (string_of_int this_fix_info.idx) ++ - str "offset := " ++ - (str (string_of_int offset)))) - g - | _,[] -> anomaly "Not a valid information" - in - let do_prove ptes_to_fixes args branches : tactic = - fun g -> - let static_infos = - { - ptes_to_fixes = ptes_to_fixes; - fixes_ids = - Idmap.fold - (fun _ fix_info acc -> fix_info.name::acc) - ptes_to_fixes [] - } - in - let nb_intros_to_do = List.length (fst (Sign.decompose_prod_assum (pf_concl g))) in - observe (str "nb_intros_to_do " ++ str (string_of_int nb_intros_to_do)); - tclTHEN - (tclDO nb_intros_to_do intro) - (fun g -> - match kind_of_term (pf_concl g) with - | App(pte,pte_args) when isVar pte -> - begin - let pte = destVar pte in - try - if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec; - let nparams = List.length !params in - let args_as_constr = List.map mkVar args in - let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in - let other_args_as_constr = List.map mkVar other_args in - let rec_num,new_body = - let idx' = list_index pte (List.rev !predicates) - 1 in - let f = fnames.(idx') in - let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly "" - in - let name_of_f = Name ( id_of_label (con_label f)) in - let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in - let idx'' = list_index name_of_f (Array.to_list na) - 1 in - let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in - let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in - rec_nums.(idx'') - nparams ,body - in - let applied_body_with_real_args = - Reductionops.nf_beta - (applist(new_body,List.rev args_as_constr)) - in - let applied_body = - Reductionops.nf_beta - (applist(applied_body_with_real_args,List.rev other_args_as_constr)) - in - observe (str "applied_body_with_real_args := "++ pr_lconstr_env (pf_env g) applied_body_with_real_args); - observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); - let do_prove branches applied_body = - do_prove_princ_for_struct - interactive_proof - (Array.to_list fnames) - static_infos - branches - applied_body - in - let replace_and_prove = - tclTHENS - (fun g -> (Equality.replace (array_last pte_args) applied_body) g) - [ - tclTHENLIST - [ - generalize other_args_as_constr; - thin other_args; - clean_goal_with_heq - static_infos do_prove - { - nb_rec_hyps = List.length branches; - rec_hyps = branches; - info = applied_body_with_real_args; - eq_hyps = []; - } ]; - let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in - let id_as_induction_constr = Tacexpr.ElimOnConstr id in - (tclTHENSEQ - [Tactics.new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *) - Tactics.intros_reflexivity - ]) - ] - in - (observe_tac "doing replacement" ( replace_and_prove)) g - with Not_Rec -> - let fname = destConst (fst (decompose_app (array_last pte_args))) in - tclTHEN - (unfold_in_concl [([],Names.EvalConstRef fname)]) - (observe_tac "" - (fun g' -> - let body = array_last (snd (destApp (pf_concl g'))) in - let dyn_infos = - { nb_rec_hyps = List.length branches; - rec_hyps = branches; - info = body; - eq_hyps = [] - } - in - let do_prove = - do_prove_princ_for_struct - interactive_proof - (Array.to_list fnames) - static_infos - in - clean_goal_with_heq static_infos - do_prove dyn_infos g' - ) - ) - g - end - | _ -> assert false - ) g - in - tclTHENSEQ - [ - (fun g -> observe_tac "introducing params" (intro_with_remembrance params princ_info.nparams) g); - (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates princ_info.npredicates) g); - (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g); - (fun g -> observe_tac "declaring fix(es)" mk_fixes g); - (fun g -> - let nb_real_args = - let pte_app = snd (Sign.decompose_prod_assum (pf_concl g)) in - let pte = fst (decompose_app pte_app) in - try - let fix_info = Idmap.find (destVar pte) !pte_to_fix in - fix_info.nb_realargs - with Not_found -> (* Not a recursive function *) - nb_prod (pf_concl g) - in - observe_tac "" (tclTHEN - (tclDO nb_real_args (observe_tac "intro" intro)) - (fun g' -> - let realargs_ids = fst (list_chop ~msg:"args" nb_real_args (pf_ids_of_hyps g')) in - let do_prove_on_branches branches : tactic = - observe_tac "proving" (do_prove !pte_to_fix ( realargs_ids) branches) - in - observe_tac "instanciating rec hyps" - (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev realargs_ids)) - g' - )) - g - ) - ] - goal - - - - - - - - - - - - - - - - - - - - - - - -exception Toberemoved_with_rel of int*constr -exception Toberemoved - -let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = - let princ_type_info = compute_elim_sig princ_type in - let env = Global.env () in -(* let type_sort = (Termops.new_sort_in_family InType) in *) - let change_predicate_sort i (x,_,t) = - let new_sort = sorts.(i) in - let args,_ = decompose_prod t in - let real_args = - if princ_type_info.indarg_in_concl - then List.tl args - else args - in - x,None,compose_prod real_args (mkSort new_sort) - in - let new_predicates = - list_map_i - change_predicate_sort - 0 - princ_type_info.predicates - in - let env_with_params_and_predicates = - Environ.push_rel_context - new_predicates - (Environ.push_rel_context - princ_type_info.params - env - ) - in - let rel_as_kn = - fst (match princ_type_info.indref with - | Some (Libnames.IndRef ind) -> ind - | _ -> failwith "Not a valid predicate" - ) - in - let pre_princ = - it_mkProd_or_LetIn - ~init: - (it_mkProd_or_LetIn - ~init:(option_fold_right - mkProd_or_LetIn - princ_type_info.indarg - princ_type_info.concl - ) - princ_type_info.args - ) - princ_type_info.branches - in - let is_dom c = - match kind_of_term c with - | Ind((u,_)) -> u = rel_as_kn - | Construct((u,_),_) -> u = rel_as_kn - | _ -> false - in - let get_fun_num c = - match kind_of_term c with - | Ind(_,num) -> num - | Construct((_,num),_) -> num - | _ -> assert false - in - let dummy_var = mkVar (id_of_string "________") in - let mk_replacement c i args = - let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in -(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) - res - in - let rec has_dummy_var t = - fold_constr - (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t)) - false - t - in - let rec compute_new_princ_type remove env pre_princ : types*(constr list) = - let (new_princ_type,_) as res = - match kind_of_term pre_princ with - | Rel n -> - begin - try match Environ.lookup_rel n env with - | _,_,t when is_dom t -> raise Toberemoved - | _ -> pre_princ,[] with Not_found -> assert false - end - | Prod(x,t,b) -> - compute_new_princ_type_for_binder remove mkProd env x t b - | Lambda(x,t,b) -> - compute_new_princ_type_for_binder remove mkLambda env x t b - | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved - | App(f,args) when is_dom f -> - let var_to_be_removed = destRel (array_last args) in - let num = get_fun_num f in - raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args)) - | App(f,args) -> - let is_pte = - match kind_of_term f with - | Rel n -> - is_pte (Environ.lookup_rel n env) - | _ -> false - in - let args = - if is_pte && remove - then array_get_start args - else args - in - let new_args,binders_to_remove = - Array.fold_right (compute_new_princ_type_with_acc remove env) - args - ([],[]) - in - let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - applist(new_f, new_args), - list_union_eq eq_constr binders_to_remove_from_f binders_to_remove - | LetIn(x,v,t,b) -> - compute_new_princ_type_for_letin remove env x v t b - | _ -> pre_princ,[] - in -(* observennl ( *) -(* match kind_of_term pre_princ with *) -(* | Prod _ -> *) -(* str "compute_new_princ_type for "++ *) -(* pr_lconstr_env env pre_princ ++ *) -(* str" is "++ *) -(* pr_lconstr_env env new_princ_type ++ fnl () *) -(* | _ -> str "" *) -(* ); *) - res - - and compute_new_princ_type_for_binder remove bind_fun env x t b = - begin - try - let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_x : name = get_name (ids_of_context env) x in - let new_env = Environ.push_rel (x,None,t) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b - else - ( - bind_fun(new_x,new_t,new_b), - list_union_eq - eq_constr - binders_to_remove_from_t - (List.map pop binders_to_remove_from_b) - ) - - with - | Toberemoved -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map pop binders_to_remove_from_b - | Toberemoved_with_rel (n,c) -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) - end - and compute_new_princ_type_for_letin remove env x v t b = - begin - try - let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in - let new_x : name = get_name (ids_of_context env) x in - let new_env = Environ.push_rel (x,Some v,t) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b - else - ( - mkLetIn(new_x,new_v,new_t,new_b), - list_union_eq - eq_constr - (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) - (List.map pop binders_to_remove_from_b) - ) - - with - | Toberemoved -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map pop binders_to_remove_from_b - | Toberemoved_with_rel (n,c) -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) - end - and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = - let new_e,to_remove_from_e = compute_new_princ_type remove env e - in - new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc - in -(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *) - let pre_res,_ = - compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in - it_mkProd_or_LetIn - ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates) - princ_type_info.params - - - -let change_property_sort toSort princ princName = - let princ_info = compute_elim_sig princ in - let change_sort_in_predicate (x,v,t) = - (x,None, - let args,_ = decompose_prod t in - compose_prod args (mkSort toSort) - ) - in - let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in - let init = - let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in - mkApp(princName_as_constr, - Array.init nargs - (fun i -> mkRel (nargs - i ))) - in - it_mkLambda_or_LetIn - ~init: - (it_mkLambda_or_LetIn ~init - (List.map change_sort_in_predicate princ_info.predicates) - ) - princ_info.params - - -let pp_dur time time' = - str (string_of_float (System.time_difference time time')) - -(* Things to be removed latter : just here to compare - saving proof with and without normalizing the proof -*) -let new_save id const (locality,kind) hook = - let {const_entry_body = pft; - const_entry_type = tpo; - const_entry_opaque = opacity } = const in - let l,r = match locality with - | Decl_kinds.Local when Lib.sections_are_opened () -> - let k = Decl_kinds.logical_kind_of_goal_kind kind in - let c = Declare.SectionLocalDef (pft, tpo, opacity) in - let _ = Declare.declare_variable id (Lib.cwd(), c, k) in - (Decl_kinds.Local, Libnames.VarRef id) - | Decl_kinds.Local -> - let k = Decl_kinds.logical_kind_of_goal_kind kind in - let kn = Declare.declare_constant id (DefinitionEntry const, k) in - (Decl_kinds.Global, Libnames.ConstRef kn) - | Decl_kinds.Global -> - let k = Decl_kinds.logical_kind_of_goal_kind kind in - let kn = Declare.declare_constant id (DefinitionEntry const, k) in - (Decl_kinds.Global, Libnames.ConstRef kn) in - let time1 = System.get_time () in - Pfedit.delete_current_proof (); - let time2 = System.get_time () in - hook l r; - time1,time2 -(* definition_message id *) - - - - - -let new_save_named opacity = -(* if do_observe () *) -(* then *) - let time1 = System.get_time () in - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let time2 = System.get_time () in - let const = - { const with - const_entry_body = (* nf_betaoiotazeta *)const.const_entry_body ; - const_entry_opaque = opacity - } - in - let time3 = System.get_time () in - let time4,time5 = new_save id const persistence hook in - let time6 = System.get_time () in - Pp.msgnl - (str "cooking proof time : " ++ pp_dur time1 time2 ++ fnl () ++ - str "reducing proof time : " ++ pp_dur time2 time3 ++ fnl () ++ - str "saving proof time : " ++ pp_dur time3 time4 ++fnl () ++ - str "deleting proof time : " ++ pp_dur time4 time5 ++fnl () ++ - str "hook time :" ++ pp_dur time5 time6 - ) - -;; - -(* End of things to be removed latter : just here to compare - saving proof with and without normalizing the proof -*) - - -let generate_functional_principle - interactive_proof - old_princ_type sorts new_princ_name funs i proof_tac - = - let f = funs.(i) in - let type_sort = Termops.new_sort_in_family InType in - let new_sorts = - match sorts with - | None -> Array.make (Array.length funs) (type_sort) - | Some a -> a - in - (* First we get the type of the old graph principle *) - let mutr_nparams = (compute_elim_sig old_princ_type).nparams in - (* First we get the type of the old graph principle *) - let new_principle_type = - compute_new_princ_type_from_rel - (Array.map mkConst funs) - new_sorts - old_princ_type - in -(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) - let base_new_princ_name,new_princ_name = - match new_princ_name with - | Some (id) -> id,id - | None -> - let id_of_f = id_of_label (con_label f) in - id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) - in - let names = ref [new_princ_name] in - let hook _ _ = - if sorts = None - then -(* let id_of_f = id_of_label (con_label f) in *) - let register_with_sort fam_sort = - let s = Termops.new_sort_in_family fam_sort in - let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in - let value = - change_property_sort s new_principle_type new_princ_name - in -(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = - { const_entry_body = value; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() - } - in - ignore( - Declare.declare_constant - name - (Entries.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme) - ) - ); - names := name :: !names - in - register_with_sort InProp; - register_with_sort InSet - in - begin - Command.start_proof - new_princ_name - (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) - new_principle_type - hook - ; - try - let _tim1 = System.get_time () in - Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); - let _tim2 = System.get_time () in -(* begin *) -(* let dur1 = System.time_difference tim1 tim2 in *) -(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) -(* end; *) - let do_save = not (do_observe ()) && not interactive_proof in - let _ = - try - Options.silently Command.save_named true; - let _dur2 = System.time_difference _tim2 (System.get_time ()) in -(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *) - Options.if_verbose - (fun () -> - Pp.msgnl ( - prlist_with_sep - (fun () -> str" is defined " ++ fnl ()) - Ppconstr.pr_id - (List.rev !names) ++ str" is defined " - ) - ) - () - with e when do_save -> - msg_warning - ( - Cerrors.explain_exn e - ); - if not (do_observe ()) - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end - in - () - -(* let tim3 = Sys.time () in *) -(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *) - - with - | e -> - msg_warning - ( - Cerrors.explain_exn e - ); - if not ( do_observe ()) - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end - end - - - - - - -let get_funs_constant mp dp = - let rec get_funs_constant const e : (Names.constant*int) array = - match kind_of_term (snd (decompose_lam e)) with - | Fix((_,(na,_,_))) -> - Array.mapi - (fun i na -> - match na with - | Name id -> - let const = make_con mp dp (label_of_id id) in - const,i - | Anonymous -> - anomaly "Anonymous fix" - ) - na - | _ -> [|const,0|] - in - function const -> - let find_constant_body const = - match (Global.lookup_constant const ).const_body with - | Some b -> - let body = force b in - let body = Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) - (Global.env ()) - (Evd.empty) - body - in - body - | None -> error ( "Cannot define a principle over an axiom ") - in - let f = find_constant_body const in - let l_const = get_funs_constant const f in - (* - We need to check that all the functions found are in the same block - to prevent Reset stange thing - *) - let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in - let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in - (* all the paremeter must be equal*) - let _check_params = - let first_params = List.hd l_params in - List.iter - (fun params -> - if not ((=) first_params params) - then error "Not a mutal recursive block" - ) - l_params - in - (* The bodies has to be very similar *) - let _check_bodies = - try - let extract_info is_first body = - match kind_of_term body with - | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) - | _ -> - if is_first && (List.length l_bodies = 1) - then raise Not_Rec - else error "Not a mutal recursive block" - in - let first_infos = extract_info true (List.hd l_bodies) in - let check body = (* Hope this is correct *) - if not (first_infos = (extract_info false body)) - then error "Not a mutal recursive block" - in - List.iter check l_bodies - with Not_Rec -> () - in - l_const - -let make_scheme fas = - let env = Global.env () - and sigma = Evd.empty in - let id_to_constr id = - Tacinterp.constr_of_id env id - in - let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in - let first_fun = destConst (List.hd funs) in - let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in - let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in - let first_fun_kn = - (* Fixme: take into accour funs_mp and funs_dp *) - fst (destInd (id_to_constr first_fun_rel_id)) - in - let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in - let this_block_funs = Array.map fst this_block_funs_indexes in - let prop_sort = InProp in - let funs_indexes = - let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.map - (function const -> List.assoc (destConst const) this_block_funs_indexes) - funs - in - let ind_list = - List.map - (fun (idx) -> - let ind = first_fun_kn,idx in - let (mib,mip) = Global.lookup_inductive ind in - ind,mib,mip,true,prop_sort - ) - funs_indexes - in - let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in - let i = ref (-1) in - let sorts = - List.rev_map (fun (_,_,x) -> - Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) - ) - fas - in - let princ_names = List.map (fun (x,_,_) -> x) fas in - let _ = List.map2 - (fun princ_name scheme_type -> - incr i; -(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) -(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) -(* ); *) - generate_functional_principle - false - scheme_type - (Some (Array.of_list sorts)) - (Some princ_name) - this_block_funs - !i - (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs))) - ) - princ_names - l_schemes - in - () - -let make_case_scheme fa = - let env = Global.env () - and sigma = Evd.empty in - let id_to_constr id = - Tacinterp.constr_of_id env id - in - let funs = (fun (_,f,_) -> id_to_constr f) fa in - let first_fun = destConst funs in - let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in - let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in - let first_fun_kn = - (* Fixme: take into accour funs_mp and funs_dp *) - fst (destInd (id_to_constr first_fun_rel_id)) - in - let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in - let this_block_funs = Array.map fst this_block_funs_indexes in - let prop_sort = InProp in - let funs_indexes = - let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc (destConst funs) this_block_funs_indexes - in - let ind_fun = - let ind = first_fun_kn,funs_indexes in - ind,prop_sort - in - let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in - let sorts = - (fun (_,_,x) -> - Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) - ) - fa - in - let princ_name = (fun (x,_,_) -> x) fa in - let _ = -(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) -(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) -(* ); *) - generate_functional_principle - false - scheme_type - (Some ([|sorts|])) - (Some princ_name) - this_block_funs - 0 - (prove_princ_for_struct false 0 [|destConst funs|]) - in - () diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli deleted file mode 100644 index cad68da673..0000000000 --- a/contrib/funind/new_arg_principle.mli +++ /dev/null @@ -1,34 +0,0 @@ - -val generate_functional_principle : - (* do we accept interactive proving *) - bool -> - (* induction principle on rel *) - Term.types -> - (* *) - Term.sorts array option -> - (* Name of the new principle *) - (Names.identifier) option -> - (* the compute functions to use *) - Names.constant array -> - (* We prove the nth- principle *) - int -> - (* The tactic to use to make the proof w.r - the number of params - *) - (Term.constr array -> int -> Tacmach.tactic) -> - unit - - - -(* val my_reflexivity : Tacmach.tactic *) - -val prove_princ_for_struct : - bool -> - int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic - - -val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array -> - Term.types -> Term.types - -val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list -> unit -val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) -> unit diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 681e43af0f..e52688dc0c 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -17,18 +17,11 @@ let observennl strm = then Pp.msg strm else () -(* type binder_type = *) -(* | Lambda *) -(* | Prod *) -(* | LetIn *) - -(* type raw_context = (binder_type*name*rawconstr) list *) type binder_type = | Lambda of name | Prod of name | LetIn of name -(* | LetTuple of name list * name *) type raw_context = (binder_type*rawconstr) list @@ -44,8 +37,6 @@ let compose_raw_context = | Lambda n -> mkRLambda(n,t,acc) | Prod n -> mkRProd(n,t,acc) | LetIn n -> mkRLetIn(n,t,acc) -(* | LetTuple (nal,na) -> *) -(* RLetTuple(dummy_loc,nal,(na,None),t,acc) *) in List.fold_right compose_binder @@ -245,11 +236,6 @@ let combine_prod n t b = let combine_letin n t b = { context = t.context@((LetIn n,t.value)::b.context); value = b.value} -(* let combine_tuple nal na b in_e = *) -(* { *) -(* context = b.context@(LetTuple(nal,na),b.value)::in_e.context; *) -(* value = in_e.value *) -(* } *) let mk_result ctxt value avoid = { @@ -624,7 +610,6 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo avoid matched_expr in -(* let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in *) let those_pattern_preconds = ( List.flatten ( diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index c2410d55ca..a12f1f01f3 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -378,7 +378,7 @@ let rec proofPrinc mi: constr funind = (* <pcase> Cases b of arrPt end.*) | Case (cinfo, pcase, b, arrPt) -> let prod_pcase,_ = decompose_lam pcase in - let nmeb,_ = List.hd prod_pcase in + let _nmeb,_ = List.hd prod_pcase in let newb'= apply_leqtrpl_t b mi.lst_eqs in let type_of_b = Typing.type_of mi.env mi.sigma b in (* Replace the recursive calls to the function by calls to the constant *) @@ -428,7 +428,7 @@ let rec proofPrinc mi: constr funind = let varnames = List.map snd mi.lst_vars in let nb_vars = List.length varnames in let nb_eqs = List.length mi.lst_eqs in - let eqrels = List.map fst mi.lst_eqs in + let _eqrels = List.map fst mi.lst_eqs in (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs trouvés dans les let in et les Cases avec ceux trouves dans u (ie mi.mimick). *) diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index febc14d386..ab0c0f9a50 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -50,15 +50,16 @@ let h_intros l = tclMAP h_intro l let do_observe_tac s tac g = - let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in + let goal = begin (Printer.pr_goal (sig_it g)) end in try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v with e -> msgnl (str "observation "++str s++str " raised exception " ++ - Cerrors.explain_exn e ++ str "on goal " ++ goal ); + Cerrors.explain_exn e ++ str " on goal " ++ goal ); raise e;; -let observe_tac s tac g = tac g +let observe_tac s tac g = + tac g let hyp_ids = List.map id_of_string @@ -121,7 +122,6 @@ let rec (find_call_occs: fun f expr -> match (kind_of_term expr) with App (g, args) when g = f -> - (* For now we suppose that the function takes only one argument. *) (fun l -> List.hd l), [Array.to_list args] | App (g, args) -> let (largs: constr list) = Array.to_list args in @@ -222,8 +222,8 @@ let lt = function () -> (coq_constant "lt") let mkCaseEq a : tactic = (fun g -> -(* commentaire de Yves: on pourra avoir des problemes si - a n'est pas bien type dans l'environnement du but *) + (* commentaire de Yves: on pourra avoir des problemes si + a n'est pas bien type dans l'environnement du but *) let type_of_a = pf_type_of g a in (tclTHEN (generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]) (tclTHEN @@ -426,8 +426,8 @@ let rec introduce_all_values is_mes acc_inv func context_fn (match args with [] -> tclTHENLIST - [split(ImplicitBindings - [context_fn (List.map mkVar (List.rev values))]); + [observe_tac "split" (split(ImplicitBindings + [context_fn (List.map mkVar (List.rev values))])); observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] | arg::args -> @@ -436,23 +436,25 @@ let rec introduce_all_values is_mes acc_inv func context_fn let rec_res = next_global_ident_away true rec_res_id ids in let ids = rec_res::ids in let hspec = next_global_ident_away true hspec_id ids in - let tac = introduce_all_values is_mes acc_inv func context_fn eqs - hrec args - (rec_res::values)(hspec::specs) in + let tac = + observe_tac "introduce_all_values" ( + introduce_all_values is_mes acc_inv func context_fn eqs + hrec args + (rec_res::values)(hspec::specs)) in (tclTHENS - (simplest_elim (mkApp(mkVar hrec, Array.of_list arg))) + (observe_tac "elim h_rec" (simplest_elim (mkApp(mkVar hrec, Array.of_list arg)))) [tclTHENLIST [h_intros [rec_res; hspec]; tac]; (tclTHENS - (apply (Lazy.force acc_inv)) - [ h_assumption + (observe_tac "acc_inv" (apply (Lazy.force acc_inv))) + [ observe_tac "h_assumption" h_assumption ; - (fun g -> - tclUSER - is_mes - (Some (hrec::hspec::(retrieve_acc_var g)@specs)) - g - ) + observe_tac "user proof" (fun g -> + tclUSER + is_mes + (Some (hrec::hspec::(retrieve_acc_var g)@specs)) + g + ) ] ) ]) g) @@ -466,48 +468,6 @@ let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr = observe_tac "introduce_all_values" (introduce_all_values is_mes acc_inv func context_fn eqs hrec args [] []) -(* -let rec proveterminate is_mes acc_inv (hrec:identifier) - (f_constr:constr) (func:global_reference) (eqs:constr list) (expr:constr) = -try -(* let _ = msgnl (str "entering proveterminate") in *) - let v = - match (kind_of_term expr) with - Case (_, t, a, l) -> - (match find_call_occs f_constr a with - _,[] -> - tclTHENS (fun g -> -(* let _ = msgnl(str "entering mkCaseEq") in *) - let v = (mkCaseEq a) g in -(* let _ = msgnl (str "exiting mkCaseEq") in *) - v - ) - (List.map (mk_intros_and_continue true - (proveterminate is_mes acc_inv hrec f_constr func) - eqs) - (Array.to_list l)) - | _, _::_ -> - ( - match find_call_occs f_constr expr with - _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr) - | _, _:: _ -> - observe_tac "rec_leaf" (rec_leaf is_mes acc_inv hrec func eqs expr) - ) - ) - | _ -> (match find_call_occs f_constr expr with - _,[] -> - (try - observe_tac "base_leaf" (base_leaf func eqs expr) - with e -> (msgerrnl (str "failure in base case");raise e )) - | _, _::_ -> - observe_tac "rec_leaf" (rec_leaf is_mes acc_inv hrec func eqs expr) - ) in - (* let _ = msgnl(str "exiting proveterminate") in *) - v -with e -> - msgerrnl(str "failure in proveterminate"); - raise e -*) let proveterminate is_mes acc_inv (hrec:identifier) (f_constr:constr) (func:global_reference) base_leaf rec_leaf = let rec proveterminate (eqs:constr list) (expr:constr) = @@ -691,7 +651,7 @@ let whole_start is_mes func input_type relation rec_arg_num : tactic = let f_id = match f_name with | Name f_id -> next_global_ident_away true f_id ids - | Anonymous -> assert false + | Anonymous -> anomaly "Anonymous function" in let n_names_types,_ = decompose_lam body1 in let n_ids,ids = @@ -701,7 +661,7 @@ let whole_start is_mes func input_type relation rec_arg_num : tactic = | Name id -> let n_id = next_global_ident_away true id ids in n_id::n_ids,n_id::ids - | _ -> assert false + | _ -> anomaly "anonymous argument" ) ([],(f_id::ids)) n_names_types @@ -747,7 +707,7 @@ let build_and_l l = let mk_and p1 p2 = Term.mkApp(and_constr,[|p1;p2|]) in let rec f = function - | [] -> assert false + | [] -> anomaly "empty list of subgoals!" | [p] -> p,tclIDTAC,1 | p1::pl -> let c,tac,nb = f pl in @@ -765,43 +725,6 @@ let build_new_goal_type () = res - -let interpretable_as_section_decl d1 d2 = match d1,d2 with - | (_,Some _,_), (_,None,_) -> false - | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2 - | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 - - - - -(* let final_decompose lemma n : tactic = *) -(* fun gls -> *) -(* let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *) -(* tclTHENSEQ *) -(* [ *) -(* generalize [lemma]; *) -(* tclDO *) -(* n *) -(* (tclTHENSEQ *) -(* [h_intro hid; *) -(* h_case (mkVar hid,Rawterm.NoBindings); *) -(* clear [hid]; *) -(* intro_patterns [Genarg.IntroWildcard] *) -(* ] *) -(* ); *) -(* h_intro hid; *) -(* tclTRY *) -(* (tclTHENSEQ [h_case (mkVar hid,Rawterm.NoBindings); *) -(* clear [hid]; *) -(* h_intro hid; *) -(* intro_patterns [Genarg.IntroWildcard] *) -(* ]); *) -(* e_resolve_constr (mkVar hid); *) -(* e_assumption *) -(* ] *) -(* gls *) - - let prove_with_tcc lemma _ : tactic = fun gls -> @@ -823,20 +746,14 @@ let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal) = let name = match goal_name with | Some s -> s | None -> - try (add_suffix current_proof_name "_subproof") with _ -> assert false - + try (add_suffix current_proof_name "_subproof") + with _ -> anomaly "open_new_goal with an unamed theorem" in let sign = Global.named_context () in let sign = clear_proofs sign in let na = next_global_ident_away false name [] in if occur_existential gls_type then Util.error "\"abstract\" cannot handle existentials"; - (* let v = let lemme = mkConst (Lib.make_con na) in *) -(* Tactics.exact_no_check *) -(* (applist (lemme, *) -(* List.rev (Array.to_list (Sign.instance_from_named_context sign)))) *) -(* gls in *) - let hook _ _ = let lemma = mkConst (Lib.make_con na) in Array.iteri (fun i _ -> by (observe_tac "tac" (prove_with_tcc lemma i))) (Array.make nb_goal ()); @@ -850,10 +767,10 @@ let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal) = gls_type hook ; by (decompose_and_tac); - pp (Printer.pr_open_subgoals()); + if Options.is_verbose () then (pp (Printer.pr_open_subgoals())); () -let com_terminate ref is_mes fonctional_ref input_type relation rec_arg_num +let com_terminate tcc_lemma_name tcc_lemma_ref is_mes fonctional_ref input_type relation rec_arg_num thm_name hook = let (evmap, env) = Command.get_current_context() in start_proof thm_name @@ -861,9 +778,9 @@ let com_terminate ref is_mes fonctional_ref input_type relation rec_arg_num (hyp_terminates fonctional_ref) hook; by (observe_tac "whole_start" (whole_start is_mes fonctional_ref input_type relation rec_arg_num )); - open_new_goal ref - None - (build_new_goal_type ()) + open_new_goal tcc_lemma_ref + (Some tcc_lemma_name) + (build_new_goal_type ()) @@ -1115,10 +1032,10 @@ let (com_eqn : identifier -> Command.save_named true);; -let recursive_definition is_mes f type_of_f r rec_arg_num eq +let recursive_definition is_mes function_name type_of_f r rec_arg_num eq generate_induction_principle : unit = let function_type = interp_constr Evd.empty (Global.env()) type_of_f in - let env = push_rel (Name f,None,function_type) (Global.env()) in + let env = push_rel (Name function_name,None,function_type) (Global.env()) in let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in let res = (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) @@ -1126,17 +1043,16 @@ let recursive_definition is_mes f type_of_f r rec_arg_num eq (* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) match kind_of_term eq' with | App(e,[|_;_;eq_fix|]) -> - mkLambda (Name f,function_type,compose_lam res_vars eq_fix) + mkLambda (Name function_name,function_type,compose_lam res_vars eq_fix) | _ -> failwith "Recursive Definition (res not eq)" in let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in - let equation_id = add_suffix f "_equation" in - let functional_id = add_suffix f "_F" in - let term_id = add_suffix f "_terminate" in + let equation_id = add_suffix function_name "_equation" in + let functional_id = add_suffix function_name "_F" in + let term_id = add_suffix function_name "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Definition) res in -(* let _ = Pp.msgnl (str "res := " ++ Printer.pr_lconstr res) in *) let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = interp_constr @@ -1144,242 +1060,61 @@ let recursive_definition is_mes f type_of_f r rec_arg_num eq env_with_pre_rec_args r in + let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = let term_ref = Nametab.locate (make_short_qualid term_id) in - let f_ref = declare_f f (IsProof Lemma) arg_types term_ref in -(* let _ = message "start second proof" in *) - com_eqn equation_id functional_ref f_ref term_ref eq; + let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in +(* message "start second proof"; *) + begin + try com_eqn equation_id functional_ref f_ref term_ref eq + with e -> + begin + ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); + raise e + end + end; let eq_ref = Nametab.locate (make_short_qualid equation_id ) in - generate_induction_principle tcc_lemma_constr + let f_ref = destConst (constr_of_reference f_ref) + and functional_ref = destConst (constr_of_reference functional_ref) + and eq_ref = destConst (constr_of_reference eq_ref) in + generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; () in - com_terminate - tcc_lemma_constr - is_mes functional_ref - rec_arg_type - relation rec_arg_num - term_id - hook -;; - - - -(* let observe_tac = do_observe_tac *) - -let base_leaf_princ eq_cst functional_ref eqs expr = - tclTHENSEQ - [rewriteLR (mkConst eq_cst); - tclTRY (list_rewrite true eqs); - gen_eauto(* default_eauto *) false (false,5) [] (Some []) - ] - - - -let prove_with_tcc tcc_lemma_constr eqs : tactic = - match !tcc_lemma_constr with - | None -> tclIDTAC_MESSAGE (str "No tcc proof !!") - | Some lemma -> - fun gls -> - let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in - tclTHENSEQ - [ - generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); - tclTRY(list_rewrite true eqs); - gen_eauto(* default_eauto *) false (false,5) [] (Some []) - (* default_auto *) - ] - gls - - - -let finalize_rec_leaf_princ_with tcc_lemma_constr is_mes hrec acc_inv eqs br = - fun g -> - tclTHENSEQ [ - Eauto.e_resolve_constr (mkVar br); - tclFIRST - [ - e_assumption; - reflexivity; - tclTHEN (apply (mkVar hrec)) - (tclTHENS - (* (try *) (observe_tac "applying inversion" (apply (Lazy.force acc_inv))) -(* with e -> Pp.msgnl (Printer.pr_lconstr (Lazy.force acc_inv));raise e *) -(* ) *) - [ h_assumption - ; - tclTHEN - (fun g -> - tclUSER - is_mes - (Some (hrec::(retrieve_acc_var g))) - g - ) - (fun g -> prove_with_tcc tcc_lemma_constr eqs g) - ] - ); - gen_eauto(* default_eauto *) false (false,5) [] (Some []); - (fun g -> tclIDTAC_MESSAGE (str "here" ++ Printer.pr_goal (sig_it g)) g) - ] - ] - g - -let rec_leaf_princ - tcc_lemma_constr - eq_cst - branches_names - is_mes - acc_inv - hrec - (functional_ref:global_reference) - eqs - expr - = - fun g -> - tclTHENSEQ - [ rewriteLR (mkConst eq_cst); - list_rewrite true eqs; - tclFIRST - (List.map (finalize_rec_leaf_princ_with tcc_lemma_constr is_mes hrec acc_inv eqs) branches_names) - ] - g - -let fresh_id avoid na = - let id = - match na with - | Name id -> id - | Anonymous -> h_id - in - next_global_ident_away true id avoid - - - -let prove_principle tcc_lemma_ref is_mes functional_ref - eq_ref rec_arg_num rec_arg_type nb_args relation = -(* f_ref eq_ref rec_arg_num rec_arg_type nb_args relation *) - let eq_cst = - match eq_ref with - ConstRef sp -> sp - | _ -> assert false - in - fun g -> - let type_of_goal = pf_concl g in - let goal_ids = pf_ids_of_hyps g in - let goal_elim_infos = compute_elim_sig type_of_goal in - let params_names,ids = List.fold_left - (fun (params_names,avoid) (na,_,_) -> - let new_id = fresh_id avoid na in - (new_id::params_names,new_id::avoid) - ) - ([],goal_ids) - goal_elim_infos.params - in - let predicates_names,ids = - List.fold_left - (fun (predicates_names,avoid) (na,_,_) -> - let new_id = fresh_id avoid na in - (new_id::predicates_names,new_id::avoid) - ) - ([],ids) - goal_elim_infos.predicates - in - let branches_names,ids = - List.fold_left - (fun (branches_names,avoid) (na,_,_) -> - let new_id = fresh_id avoid na in - (new_id::branches_names,new_id::avoid) - ) - ([],ids) - goal_elim_infos.branches - in - let to_intro = params_names@predicates_names@branches_names in - let nparams = List.length params_names in - let rec_arg_num = rec_arg_num - nparams in - begin - tclTHEN - (h_intros to_intro) - (observe_tac (string_of_int (rec_arg_num)) - (fun g -> - let ids = ids_of_named_context (pf_hyps g) in - let func_body = (def_of_const (constr_of_reference functional_ref)) in -(* let _ = Pp.msgnl (Printer.pr_lconstr func_body) in *) - let (f_name, _, body1) = destLambda func_body in - let f_id = - match f_name with - | Name f_id -> next_global_ident_away true f_id ids - | Anonymous -> assert false - in - let n_names_types,_ = decompose_lam body1 in - let n_ids,ids = - List.fold_left - (fun (n_ids,ids) (n_name,_) -> - match n_name with - | Name id -> - let n_id = next_global_ident_away true id ids in - n_id::n_ids,n_id::ids - | _ -> assert false - ) - ([],(f_id::ids)) - n_names_types - in - let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in - let expr = - instantiate_lambda func_body - (mkVar f_id::(List.map mkVar n_ids)) - in - start - is_mes - rec_arg_type - ids - (snd (list_chop nparams n_ids)) - (substl (List.map mkVar params_names) relation) - (rec_arg_num) - rec_arg_id - (fun hrec acc_inv g -> - (proveterminate - is_mes - acc_inv - hrec - (mkVar f_id) - functional_ref - (base_leaf_princ eq_cst) - (rec_leaf_princ tcc_lemma_ref eq_cst branches_names) - [] - expr - ) - g - ) - (if is_mes - then - tclUSER_if_not_mes - else fun _ -> prove_with_tcc tcc_lemma_ref []) - - g - ) - ) + try + com_terminate + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + rec_arg_type + relation rec_arg_num + term_id + hook + with e -> + begin + try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> (); + raise e end - g - VERNAC COMMAND EXTEND RecursiveDefinition [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf) constr(proof) integer_opt(rec_arg_num) constr(eq) ] -> - [ ignore(proof);ignore(wf); + [ + warning "Recursive Definition is obsolete. Use Function instead"; + ignore(proof);ignore(wf); let rec_arg_num = match rec_arg_num with | None -> 1 | Some n -> n in - recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _ _ _ -> ())] + recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _ _ _ _ -> ())] | [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf) "[" ne_constr_list(proof) "]" constr(eq) ] -> - [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq (fun _ _ _ _ _ _ _ -> ())] + [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq (fun _ _ _ _ _ _ _ _ -> ())] END diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index dc521cc55a..e4e61c5540 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -52,3 +52,5 @@ val set_pcoq_hook : pcoq_hook -> unit val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit + +val vernac_reset_name : identifier Util.located -> unit |