diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-15 12:34:56 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-15 12:34:56 +0000 |
| commit | 93b9b88d8c9b01b062948997ba627a404e52585f (patch) | |
| tree | e8b7d09fd1388eb8353a44540c5a0d0ef99753cb | |
| parent | c9ced02e4d5d5d2855443e2ad0893e5101e38239 (diff) | |
reflexive tauto
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7233 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | .depend | 292 | ||||
| -rw-r--r-- | .depend.camlp4 | 1 | ||||
| -rw-r--r-- | .depend.coq | 2 | ||||
| -rw-r--r-- | Makefile | 17 | ||||
| -rw-r--r-- | contrib/rtauto/Bintree.v | 498 | ||||
| -rw-r--r-- | contrib/rtauto/Rtauto.v | 399 | ||||
| -rw-r--r-- | contrib/rtauto/g_rtauto.ml4 | 16 | ||||
| -rw-r--r-- | contrib/rtauto/proof_search.ml | 546 | ||||
| -rw-r--r-- | contrib/rtauto/proof_search.mli | 49 | ||||
| -rw-r--r-- | contrib/rtauto/refl_tauto.ml | 337 | ||||
| -rw-r--r-- | contrib/rtauto/refl_tauto.mli | 26 |
11 files changed, 2036 insertions, 147 deletions
@@ -53,12 +53,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \ kernel/declarations.cmi kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \ kernel/environ.cmi kernel/declarations.cmi -kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi -kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \ - kernel/declarations.cmi kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \ kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \ kernel/declarations.cmi +kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi +kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \ + kernel/declarations.cmi kernel/names.cmi: lib/predicate.cmi lib/pp.cmi kernel/reduction.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/environ.cmi @@ -82,9 +82,6 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \ kernel/cbytecodes.cmi lib/bigint.cmi: lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi lib/compat.cmo library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \ library/nametab.cmi kernel/names.cmi library/libnames.cmi \ kernel/indtypes.cmi kernel/entries.cmi kernel/declarations.cmi \ @@ -115,6 +112,9 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \ library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \ library/libnames.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi lib/compat.cmo parsing/ast.cmi: lib/util.cmi interp/topconstr.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi library/libnames.cmi \ interp/genarg.cmi lib/dyn.cmi parsing/coqast.cmi @@ -349,11 +349,11 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \ toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \ library/libobject.cmi toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi -toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ 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 toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ kernel/environ.cmi translate/ppconstrnew.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ @@ -374,9 +374,9 @@ contrib/cc/ccalgo.cmi: kernel/term.cmi kernel/names.cmi contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \ kernel/term.cmi kernel/names.cmi -contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi +contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \ @@ -396,8 +396,8 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \ kernel/names.cmi contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi contrib/correctness/pwp.cmi: kernel/term.cmi -contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi contrib/dp/dp_cvcl.cmi: contrib/dp/fol.cmi +contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi: contrib/dp/fol.cmi contrib/dp/dp_zenon.cmi: contrib/dp/fol.cmi @@ -469,6 +469,8 @@ contrib/jprover/jall.cmi: contrib/jprover/opname.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jlogic.cmi contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi +contrib/rtauto/refl_tauto.cmi: kernel/term.cmi proofs/tacmach.cmi \ + proofs/proof_type.cmi contrib/rtauto/proof_search.cmi kernel/names.cmi contrib/subtac/infer.cmi: lib/util.cmi kernel/term.cmi \ contrib/subtac/sast.cmo lib/pp.cmi contrib/subtac/natural.cmo \ kernel/names.cmi @@ -518,6 +520,14 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi 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 +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 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 \ @@ -542,14 +552,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.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 -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 ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi @@ -730,6 +732,14 @@ kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \ kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \ kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \ kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi +kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ + kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ + kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ + kernel/cbytegen.cmi kernel/modops.cmi +kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ + kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ + kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ + kernel/cbytegen.cmx kernel/modops.cmi kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \ @@ -744,14 +754,6 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \ kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \ kernel/cemitcodes.cmx kernel/cbytegen.cmx kernel/mod_typing.cmi -kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ - kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ - kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ - kernel/cbytegen.cmi kernel/modops.cmi -kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ - kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ - kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ - kernel/cbytegen.cmx kernel/modops.cmi kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/options.cmi \ lib/hashcons.cmi kernel/names.cmi kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/options.cmx \ @@ -846,10 +848,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmap.cmo: lib/gmap.cmi -lib/gmap.cmx: lib/gmap.cmi lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi +lib/gmap.cmo: lib/gmap.cmi +lib/gmap.cmx: lib/gmap.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi @@ -858,24 +860,14 @@ lib/heap.cmo: lib/heap.cmi lib/heap.cmx: lib/heap.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi -lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi +lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi +lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi -lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi -lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi -lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi -lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \ kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \ kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \ @@ -990,6 +982,16 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \ library/lib.cmx library/states.cmi library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi +lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi +lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi +lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi +lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \ interp/genarg.cmi parsing/ast.cmi @@ -2354,20 +2356,6 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.cmx \ toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi -toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi lib/system.cmi library/states.cmi \ - proofs/refiner.cmi translate/ppvernacnew.cmi lib/pp.cmi proofs/pfedit.cmi \ - parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/library.cmi \ - library/lib.cmi parsing/lexer.cmi parsing/coqast.cmi \ - interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx lib/system.cmx library/states.cmx \ - proofs/refiner.cmx translate/ppvernacnew.cmx lib/pp.cmx proofs/pfedit.cmx \ - parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/library.cmx \ - library/lib.cmx parsing/lexer.cmx parsing/coqast.cmx \ - interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \ kernel/typeops.cmi interp/topconstr.cmi kernel/term.cmi \ @@ -2430,6 +2418,20 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \ parsing/extend.cmx parsing/coqast.cmx parsing/ast.cmx \ toplevel/vernacinterp.cmi +toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi lib/system.cmi library/states.cmi \ + proofs/refiner.cmi translate/ppvernacnew.cmi lib/pp.cmi proofs/pfedit.cmi \ + parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/library.cmi \ + library/lib.cmi parsing/lexer.cmi parsing/coqast.cmi \ + interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx lib/system.cmx library/states.cmx \ + proofs/refiner.cmx translate/ppvernacnew.cmx lib/pp.cmx proofs/pfedit.cmx \ + parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/library.cmx \ + library/lib.cmx parsing/lexer.cmx parsing/coqast.cmx \ + interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi kernel/term.cmi \ lib/system.cmi interp/syntax_def.cmi pretyping/rawterm.cmi lib/pp.cmi \ parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ @@ -2532,6 +2534,12 @@ contrib/cc/cctac.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ pretyping/evd.cmx parsing/egrammar.cmx kernel/declarations.cmx \ interp/coqlib.cmx toplevel/cerrors.cmx contrib/cc/ccproof.cmx \ contrib/cc/ccalgo.cmx +contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \ + kernel/sign.cmi kernel/names.cmi library/global.cmi \ + contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \ + kernel/sign.cmx kernel/names.cmx library/global.cmx \ + contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \ @@ -2546,12 +2554,6 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ library/libnames.cmx kernel/indtypes.cmx library/global.cmx \ kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \ kernel/declarations.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \ - kernel/sign.cmi kernel/names.cmi library/global.cmi \ - contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \ - kernel/sign.cmx kernel/names.cmx library/global.cmx \ - contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \ library/nametab.cmi kernel/names.cmi library/global.cmi \ interp/constrintern.cmi contrib/correctness/pdb.cmi @@ -2674,6 +2676,8 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \ library/nametab.cmx kernel/names.cmx library/libnames.cmx \ tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \ contrib/correctness/pwp.cmi +contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi +contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi library/summary.cmi translate/ppconstrnew.cmi \ @@ -2692,8 +2696,6 @@ contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \ contrib/dp/dp_zenon.cmx contrib/dp/dp_sorts.cmx \ contrib/dp/dp_simplify.cmx contrib/dp/dp_cvcl.cmx kernel/declarations.cmx \ interp/coqlib.cmx contrib/dp/dp.cmi -contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi -contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi contrib/dp/dp_sorts.cmo: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi @@ -3178,6 +3180,14 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \ proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \ library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \ interp/coqlib.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \ + contrib/interface/vtp.cmi contrib/interface/translate.cmi \ + parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \ + parsing/esyntax.cmi contrib/interface/ascent.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ + contrib/interface/vtp.cmx contrib/interface/translate.cmx \ + parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ + parsing/esyntax.cmx contrib/interface/ascent.cmi contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi contrib/interface/translate.cmi \ pretyping/termops.cmi parsing/termast.cmi kernel/term.cmi \ @@ -3202,14 +3212,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \ parsing/coqast.cmx interp/constrintern.cmx pretyping/clenv.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \ - contrib/interface/vtp.cmi contrib/interface/translate.cmi \ - parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \ - parsing/esyntax.cmi contrib/interface/ascent.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ - contrib/interface/vtp.cmx contrib/interface/translate.cmx \ - parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ - parsing/esyntax.cmx contrib/interface/ascent.cmi contrib/interface/translate.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \ parsing/termast.cmi kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi \ @@ -3390,6 +3392,22 @@ contrib/romega/refl_omega.cmx: lib/util.cmx kernel/term.cmx \ parsing/printer.cmx lib/pp.cmx lib/options.cmx contrib/omega/omega.cmx \ kernel/names.cmx proofs/logic.cmx interp/coqlib.cmx \ contrib/romega/const_omega.cmx lib/bigint.cmx +contrib/rtauto/proof_search.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \ + library/goptions.cmi contrib/rtauto/proof_search.cmi +contrib/rtauto/proof_search.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \ + library/goptions.cmx contrib/rtauto/proof_search.cmi +contrib/rtauto/refl_tauto.cmo: lib/util.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tactics.cmi proofs/tactic_debug.cmi \ + proofs/tacmach.cmi tactics/tacinterp.cmi lib/system.cmi \ + pretyping/retyping.cmi contrib/rtauto/proof_search.cmi lib/pp.cmi \ + kernel/names.cmi library/goptions.cmi lib/explore.cmi pretyping/evd.cmi \ + interp/coqlib.cmi kernel/closure.cmi contrib/rtauto/refl_tauto.cmi +contrib/rtauto/refl_tauto.cmx: lib/util.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tactics.cmx proofs/tactic_debug.cmx \ + proofs/tacmach.cmx tactics/tacinterp.cmx lib/system.cmx \ + pretyping/retyping.cmx contrib/rtauto/proof_search.cmx lib/pp.cmx \ + kernel/names.cmx library/goptions.cmx lib/explore.cmx pretyping/evd.cmx \ + interp/coqlib.cmx kernel/closure.cmx contrib/rtauto/refl_tauto.cmi contrib/subtac/infer.cmo: lib/util.cmi toplevel/toplevel.cmi kernel/term.cmi \ contrib/subtac/scoq.cmo contrib/subtac/sast.cmo pretyping/rawterm.cmi \ translate/ppconstrnew.cmi lib/pp.cmi contrib/subtac/natural.cmo \ @@ -3444,18 +3462,12 @@ contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \ lib/pp.cmx parsing/pcoq.cmx lib/options.cmx kernel/names.cmx \ library/nameops.cmx library/libnames.cmx interp/genarg.cmx \ parsing/egrammar.cmx parsing/coqast.cmx toplevel/cerrors.cmx -contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi -contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \ kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \ kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx -contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \ - tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ - contrib/xml/acic.cmo -contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \ - tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \ - contrib/xml/acic.cmx +contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi +contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \ kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \ @@ -3474,6 +3486,12 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \ kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \ library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \ contrib/xml/acic.cmx +contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \ + tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/acic.cmo +contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \ + tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \ + contrib/xml/acic.cmx contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \ kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ @@ -3516,8 +3534,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \ contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \ lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \ kernel/sign.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \ @@ -3548,10 +3564,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \ interp/genarg.cmx parsing/extend.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx -ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \ - ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi -ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \ - ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi ide/utils/configwin_html_config.cmo: ide/utils/uoptions.cmi \ ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo \ ide/utils/configwin_ihm.cmo @@ -3562,6 +3576,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/uoptions.cmi ide/utils/okey.cmi \ ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmx: ide/utils/uoptions.cmx ide/utils/okey.cmx \ ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx +ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \ + ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi +ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \ + ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi ide/utils/configwin_types.cmo: ide/utils/uoptions.cmi \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmx: ide/utils/uoptions.cmx \ @@ -3624,6 +3642,8 @@ contrib/first-order/g_ground.cmo: parsing/grammar.cma contrib/first-order/g_ground.cmx: parsing/grammar.cma contrib/subtac/sparser.cmo: parsing/grammar.cma contrib/subtac/sparser.cmx: parsing/grammar.cma +contrib/rtauto/g_rtauto.cmo.cmo: +contrib/rtauto/g_rtauto.cmo.cmx: contrib/interface/debug_tac.cmo: parsing/grammar.cma contrib/interface/debug_tac.cmx: parsing/grammar.cma contrib/interface/centaur.cmo: parsing/grammar.cma @@ -3695,72 +3715,58 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/3.08.3/caml/config.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/misc.h /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/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 \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h + /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/config.h /usr/lib/ocaml/3.08.3/caml/misc.h \ + /usr/lib/ocaml/3.08.3/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/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 \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h + /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/config.h /usr/lib/ocaml/3.08.3/caml/misc.h \ + /usr/lib/ocaml/3.08.3/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /home/logical/local/lib/ocaml/caml/alloc.h + /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/config.h /usr/lib/ocaml/3.08.3/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/caml/memory.h \ + kernel/byterun/coq_values.h /usr/lib/ocaml/3.08.3/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h \ + /usr/lib/ocaml/3.08.3/caml/config.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/misc.h /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/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 \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h + /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/config.h /usr/lib/ocaml/3.08.3/caml/misc.h \ + /usr/lib/ocaml/3.08.3/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/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 \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h \ - /home/logical/local/lib/ocaml/caml/alloc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h + /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/config.h /usr/lib/ocaml/3.08.3/caml/misc.h \ + /usr/lib/ocaml/3.08.3/caml/alloc.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local/lib/ocaml/caml/mlvalues.h \ - /home/logical/local/lib/ocaml/caml/compatibility.h \ - /home/logical/local/lib/ocaml/caml/config.h \ - /home/logical/local/lib/ocaml/caml/misc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_memory.h /home/logical/local/lib/ocaml/caml/fail.h \ - /home/logical/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /home/logical/local/lib/ocaml/caml/alloc.h + /usr/lib/ocaml/3.08.3/caml/mlvalues.h \ + /usr/lib/ocaml/3.08.3/caml/compatibility.h \ + /usr/lib/ocaml/3.08.3/caml/config.h /usr/lib/ocaml/3.08.3/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /usr/lib/ocaml/3.08.3/caml/fail.h /usr/lib/ocaml/3.08.3/caml/memory.h \ + kernel/byterun/coq_values.h /usr/lib/ocaml/3.08.3/caml/alloc.h diff --git a/.depend.camlp4 b/.depend.camlp4 index 1a74b42a2..e6618560e 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -18,6 +18,7 @@ contrib/cc/cctac.ml: parsing/grammar.cma contrib/funind/tacinv.ml: parsing/grammar.cma contrib/first-order/g_ground.ml: parsing/grammar.cma contrib/subtac/sparser.ml: parsing/grammar.cma +contrib/rtauto/g_rtauto.cmo.ml: contrib/interface/debug_tac.ml: parsing/grammar.cma contrib/interface/centaur.ml: parsing/grammar.cma parsing/lexer.ml: diff --git a/.depend.coq b/.depend.coq index da1504451..e8b250d67 100644 --- a/.depend.coq +++ b/.depend.coq @@ -278,3 +278,5 @@ contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contr contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo contrib/cc/CCSolve.vo: contrib/cc/CCSolve.v +contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theories/NArith/BinPos.vo +contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/cc/CCSolve.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo @@ -73,7 +73,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I contrib/interface -I contrib/fourier \ -I contrib/jprover -I contrib/cc \ -I contrib/funind -I contrib/first-order \ - -I contrib/field -I contrib/subtac + -I contrib/field -I contrib/subtac -I contrib/rtauto MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -301,13 +301,16 @@ SUBTACCMO=\ contrib/subtac/rewrite.cmo \ contrib/subtac/sparser.cmo +RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ + contrib/rtauto/g_rtauto.cmo + ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \ contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \ - contrib/subtac/sparser.ml4 + contrib/subtac/sparser.ml4 contrib/rtauto/g_rtauto.cmo CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(DPCMO) $(FIELDCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) + $(CCCMO) $(FUNINDCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -1003,8 +1006,13 @@ CCVO=\ SUBTACVO= +RTAUTOVO = \ + contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo + + CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ - $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) + $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \ + $(RTAUTOVO) $(CONTRIBVO): states/initial.coq @@ -1020,6 +1028,7 @@ jprover: $(JPROVERVO) $(JPROVERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) subtac: $(SUBTACVO) $(SUBTACCMO) +rtauto: $(RTAUTOVO) $(RTAUTOCMO) NEWINITVO=$(INITVO) NEWTHEORIESVO=$(THEORIESVO) diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v new file mode 100644 index 000000000..ee66f02a9 --- /dev/null +++ b/contrib/rtauto/Bintree.v @@ -0,0 +1,498 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +Require Export List. +Require Export BinPos. + +Unset Boxed Definitions. + +Open Scope positive_scope. + +Ltac clean := try (simpl; congruence). +Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. + +Functional Scheme Pcompare_ind := Induction for Pcompare. + +Lemma Prect : forall P : positive -> Type, + P 1 -> + (forall n : positive, P n -> P (Psucc n)) -> forall p : positive, P p. +intros P H1 Hsucc n; induction n. +rewrite <- plus_iter_xI; apply Hsucc; apply iterate_add; assumption. +rewrite <- plus_iter_xO; apply iterate_add; assumption. +assumption. +Qed. + +Lemma Gt_Eq_Gt : forall p q cmp, + (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt. +apply (Pcompare_ind (fun p q cmp => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt)); +simpl;auto;congruence. +Qed. + +Lemma Gt_Lt_Gt : forall p q cmp, + (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt. +apply (Pcompare_ind (fun p q cmp => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt)); +simpl;auto;congruence. +Qed. + +Lemma Gt_Psucc_Eq: forall p q, + (p ?= Psucc q) Gt = Gt -> (p ?= q) Eq = Gt. +intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence. +intro;apply Gt_Eq_Gt;auto. +apply Gt_Lt_Gt. +Qed. + +Lemma Eq_Psucc_Gt: forall p q, + (p ?= Psucc q) Eq = Eq -> (p ?= q) Eq = Gt. +intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence. +intro H;elim (Pcompare_not_Eq p (Psucc q));tauto. +intro H;apply Gt_Eq_Gt;auto. +intro H;rewrite Pcompare_Eq_eq with p q;auto. +generalize q;clear q IHq p H;induction q;simpl;auto. +intro H;elim (Pcompare_not_Eq p q);tauto. +Qed. + +Lemma Gt_Psucc_Gt : forall n p cmp cmp0, + (n?=p) cmp = Gt -> (Psucc n?=p) cmp0 = Gt. +induction n;intros [ | p | p];simpl;try congruence. +intros; apply IHn with cmp;trivial. +intros; apply IHn with Gt;trivial. +intros;apply Gt_Lt_Gt;trivial. +intros [ | | ] _ H. +apply Gt_Eq_Gt;trivial. +apply Gt_Lt_Gt;trivial. +trivial. +Qed. + +Lemma Gt_Psucc: forall p q, + (p ?= Psucc q) Eq = Gt -> (p ?= q) Eq = Gt. +intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence. +apply Gt_Psucc_Eq. +intro;apply Gt_Eq_Gt;apply IHq;auto. +apply Gt_Eq_Gt. +apply Gt_Lt_Gt. +Qed. + +Lemma Psucc_Gt : forall p, + (Psucc p ?= p) Eq = Gt. +induction p;simpl. +apply Gt_Eq_Gt;auto. +generalize p;clear p IHp. +induction p;simpl;auto. +reflexivity. +Qed. + +Fixpoint pos_eq (m n:positive) {struct m} :bool := +match m, n with + xI mm, xI nn => pos_eq mm nn +| xO mm, xO nn => pos_eq mm nn +| xH, xH => true +| _, _ => false +end. + +Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n. +induction m;simpl;intro n;destruct n;congruence || +(intro e;apply f_equal with positive;auto). +Defined. + +Theorem refl_pos_eq : forall m, pos_eq m m = true. +induction m;simpl;auto. +Qed. + +Definition pos_eq_dec (m n:positive) :{m=n}+{m<>n} . +fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence). +case (pos_eq_dec mm nn). +intro e;left;apply (f_equal xI e). +intro ne;right;congruence. +case (pos_eq_dec mm nn). +intro e;left;apply (f_equal xO e). +intro ne;right;congruence. +left;reflexivity. +Defined. + +Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (m<>m) (refl_equal m) . +fix 1;intros [mm|mm|]. +simpl; rewrite pos_eq_dec_refl; reflexivity. +simpl; rewrite pos_eq_dec_refl; reflexivity. +reflexivity. +Qed. + +Theorem pos_eq_dec_ex : forall m n, + pos_eq m n =true -> exists h:m=n, + pos_eq_dec m n = left (m<>n) h. +fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence). +simpl;intro e. +elim (pos_eq_dec_ex _ _ e). +intros x ex; rewrite ex. +exists (f_equal xI x). +reflexivity. +simpl;intro e. +elim (pos_eq_dec_ex _ _ e). +intros x ex; rewrite ex. +exists (f_equal xO x). +reflexivity. +simpl. +exists (refl_equal xH). +reflexivity. +Qed. + +Fixpoint nat_eq (m n:nat) {struct m}: bool:= +match m, n with +O,O => true +| S mm,S nn => nat_eq mm nn +| _,_ => false +end. + +Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n. +induction m;simpl;intro n;destruct n;congruence || +(intro e;apply f_equal with nat;auto). +Defined. + +Theorem refl_nat_eq : forall n, nat_eq n n = true. +induction n;simpl;trivial. +Defined. + +Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A := +match l with nil => None +| x::q => +match n with O => Some x +| S m => Lget A m q +end end . + +Implicit Arguments Lget [A]. + +Lemma map_app : forall (A B:Set) (f:A -> B) l m, +List.map f (l ++ m) = List.map f l ++ List.map f m. +induction l. +reflexivity. +simpl. +intro m ; apply f_equal with (list B);apply IHl. +Qed. + +Lemma length_map : forall (A B:Set) (f:A -> B) l, +length (List.map f l) = length l. +induction l. +reflexivity. +simpl; apply f_equal with nat;apply IHl. +Qed. + +Lemma Lget_map : forall (A B:Set) (f:A -> B) i l, +Lget i (List.map f l) = +match Lget i l with Some a => +Some (f a) | None => None end. +induction i;intros [ | x l ] ;trivial. +simpl;auto. +Qed. + +Lemma Lget_app : forall (A:Set) (a:A) l i, +Lget i (l ++ a :: nil) = if nat_eq i (length l) then Some a else Lget i l. +induction l;simpl Lget;simpl length. +intros [ | i];simpl;reflexivity. +intros [ | i];simpl. +reflexivity. +auto. +Qed. + +Lemma Lget_app_Some : forall (A:Set) l delta i (a: A), +Lget i l = Some a -> +Lget i (l ++ delta) = Some a. +induction l;destruct i;simpl;try congruence;auto. +Qed. + +Section Store. + +Variable A:Type. + +Inductive Poption : Type:= + PSome : A -> Poption +| PNone : Poption. + +Inductive Tree : Type := + Tempty : Tree + | Branch0 : Tree -> Tree -> Tree + | Branch1 : A -> Tree -> Tree -> Tree. + +Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := + match T with + Tempty => PNone + | Branch0 T1 T2 => + match p with + xI pp => Tget pp T2 + | xO pp => Tget pp T1 + | xH => PNone + end + | Branch1 a T1 T2 => + match p with + xI pp => Tget pp T2 + | xO pp => Tget pp T1 + | xH => PSome a + end +end. + +Fixpoint Tadd (p:positive) (a:A) (T:Tree) {struct p}: Tree := + match T with + | Tempty => + match p with + | xI pp => Branch0 Tempty (Tadd pp a Tempty) + | xO pp => Branch0 (Tadd pp a Tempty) Tempty + | xH => Branch1 a Tempty Tempty + end + | Branch0 T1 T2 => + match p with + | xI pp => Branch0 T1 (Tadd pp a T2) + | xO pp => Branch0 (Tadd pp a T1) T2 + | xH => Branch1 a T1 T2 + end + | Branch1 b T1 T2 => + match p with + | xI pp => Branch1 b T1 (Tadd pp a T2) + | xO pp => Branch1 b (Tadd pp a T1) T2 + | xH => Branch1 a T1 T2 + end + end. + +Definition mkBranch0 (T1 T2:Tree) := + match T1,T2 with + Tempty ,Tempty => Tempty + | _,_ => Branch0 T1 T2 + end. + +Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree := + match T with + | Tempty => Tempty + | Branch0 T1 T2 => + match p with + | xI pp => mkBranch0 T1 (Tremove pp T2) + | xO pp => mkBranch0 (Tremove pp T1) T2 + | xH => T + end + | Branch1 b T1 T2 => + match p with + | xI pp => Branch1 b T1 (Tremove pp T2) + | xO pp => Branch1 b (Tremove pp T1) T2 + | xH => mkBranch0 T1 T2 + end + end. + + +Theorem Tget_Tempty: forall (p : positive), Tget p (Tempty) = PNone. +destruct p;reflexivity. +Qed. + +Theorem Tget_Tadd: forall i j a T, + Tget i (Tadd j a T) = + match (i ?= j) Eq with + Eq => PSome a + | Lt => Tget i T + | Gt => Tget i T + end. +intros i j. +caseq ((i ?= j) Eq). +intro H;rewrite (Pcompare_Eq_eq _ _ H);intros a;clear i H. +induction j;destruct T;simpl;try (apply IHj);congruence. +generalize i;clear i;induction j;destruct T;simpl in H|-*; +destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. +generalize i;clear i;induction j;destruct T;simpl in H|-*; +destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence. +Qed. + +Record Store : Type := +mkStore {index:positive;contents:Tree}. + +Definition empty := mkStore xH Tempty. + +Definition push a S := +mkStore (Psucc (index S)) (Tadd (index S) a (contents S)). + +Definition get i S := Tget i (contents S). + +Lemma get_empty : forall i, get i empty = PNone. +intro i; case i; unfold empty,get; simpl;reflexivity. +Qed. + +Inductive Full : Store -> Type:= + F_empty : Full empty + | F_push : forall a S, Full S -> Full (push a S). + +Theorem get_Full_Gt : forall S, Full S -> + forall i, (i ?= index S) Eq = Gt -> get i S = PNone. +intros S W;induction W. +unfold empty,index,get,contents;intros;apply Tget_Tempty. +unfold index,get,push;simpl contents. +intros i e;rewrite Tget_Tadd. +rewrite (Gt_Psucc _ _ e). +unfold get in IHW. +apply IHW;apply Gt_Psucc;assumption. +Qed. + +Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone. +intros [index0 contents0] F. +case F. +unfold empty,index,get,contents;intros;apply Tget_Tempty. +unfold index,get,push;simpl contents. +intros a S. +rewrite Tget_Tadd. +rewrite Psucc_Gt. +intro W. +change (get (Psucc (index S)) S =PNone). +apply get_Full_Gt; auto. +apply Psucc_Gt. +Qed. + +Theorem get_push_Full : + forall i a S, Full S -> + get i (push a S) = + match (i ?= index S) Eq with + Eq => PSome a + | Lt => get i S + | Gt => PNone +end. +intros i a S F. +caseq ((i ?= index S) Eq). +intro e;rewrite (Pcompare_Eq_eq _ _ e). +destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd. +rewrite Pcompare_refl;reflexivity. +intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd. +simpl index in H;rewrite H;reflexivity. +intro H;generalize H;clear H. +unfold get,push;simpl index;simpl contents. +rewrite Tget_Tadd;intro e;rewrite e. +change (get i S=PNone). +apply get_Full_Gt;auto. +Qed. + +Lemma Full_push_compat : forall i a S, Full S -> +forall x, get i S = PSome x -> + get i (push a S) = PSome x. +intros i a S F x H. +caseq ((i ?= index S) Eq);intro test. +rewrite (Pcompare_Eq_eq _ _ test) in H. +rewrite (get_Full_Eq _ F) in H;congruence. +rewrite <- H. +rewrite (get_push_Full i a). +rewrite test;reflexivity. +assumption. +rewrite (get_Full_Gt _ F) in H;congruence. +Qed. + +Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty. +intros [ind cont] F one; inversion F. +reflexivity. +simpl index in one;assert (h:=Psucc_not_one (index S)). +congruence. +Qed. + +Lemma push_not_empty: forall a S, (push a S) <> empty. +intros a [ind cont];unfold push,empty. +simpl;intro H;injection H; intros _ ; apply Psucc_not_one. +Qed. + +Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop := +match F with +F_empty => False +| F_push a SS FF => x=a \/ In x SS FF +end. + +Lemma get_In : forall (x:A) (S:Store) (F:Full S) i , +get i S = PSome x -> In x S F. +induction F. +intro i;rewrite get_empty; congruence. +intro i;rewrite get_push_Full;trivial. +caseq ((i ?= index S) Eq);simpl. +left;congruence. +right;eauto. +congruence. +Qed. + +End Store. + +Implicit Arguments PNone [A]. +Implicit Arguments PSome [A]. + +Implicit Arguments Tempty [A]. +Implicit Arguments Branch0 [A]. +Implicit Arguments Branch1 [A]. + +Implicit Arguments Tget [A]. +Implicit Arguments Tadd [A]. + +Implicit Arguments Tget_Tempty [A]. +Implicit Arguments Tget_Tadd [A]. + +Implicit Arguments mkStore [A]. +Implicit Arguments index [A]. +Implicit Arguments contents [A]. + +Implicit Arguments empty [A]. +Implicit Arguments get [A]. +Implicit Arguments push [A]. + +Implicit Arguments get_empty [A]. +Implicit Arguments get_push_Full [A]. + +Implicit Arguments Full [A]. +Implicit Arguments F_empty [A]. +Implicit Arguments F_push [A]. +Implicit Arguments In [A]. + +Section Map. + +Variables A B:Set. + +Variable f: A -> B. + +Fixpoint Tmap (T: Tree A) : Tree B := +match T with +Tempty => Tempty +| Branch0 t1 t2 => Branch0 (Tmap t1) (Tmap t2) +| Branch1 a t1 t2 => Branch1 (f a) (Tmap t1) (Tmap t2) +end. + +Lemma Tget_Tmap: forall T i, +Tget i (Tmap T)= match Tget i T with PNone => PNone +| PSome a => PSome (f a) end. +induction T;intro i;case i;simpl;auto. +Defined. + +Lemma Tmap_Tadd: forall i a T, +Tmap (Tadd i a T) = Tadd i (f a) (Tmap T). +induction i;intros a T;case T;simpl;intros;try (rewrite IHi);simpl;reflexivity. +Defined. + +Definition map (S:Store A) : Store B := +mkStore (index S) (Tmap (contents S)). + +Lemma get_map: forall i S, +get i (map S)= match get i S with PNone => PNone +| PSome a => PSome (f a) end. +destruct S;unfold get,map,contents,index;apply Tget_Tmap. +Defined. + +Lemma map_push: forall a S, +map (push a S) = push (f a) (map S). +intros a S. +case S. +unfold push,map,contents,index. +intros;rewrite Tmap_Tadd;reflexivity. +Defined. + +Theorem Full_map : forall S, Full S -> Full (map S). +intros S F. +induction F. +exact F_empty. +rewrite map_push;constructor 2;assumption. +Defined. + +End Map. + +Implicit Arguments Tmap [A B]. +Implicit Arguments map [A B]. +Implicit Arguments Full_map [A B f]. + +Notation "hyps \ A" := (push A hyps) (at level 72,left associativity). diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v new file mode 100644 index 000000000..0e3d697c1 --- /dev/null +++ b/contrib/rtauto/Rtauto.v @@ -0,0 +1,399 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + + +Require Export List. +Require Export CCSolve. +Require Export Bintree. +Require Import Bool. +Unset Boxed Definitions. + +Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. +Ltac clean:=try (simpl;congruence). + +Inductive form:Set:= +Atom : positive -> form +| Arrow : form -> form -> form +| Bot +| Conjunct : form -> form -> form +| Disjunct : form -> form -> form. + +Notation "[ n ]":=(Atom n). +Notation "A =>> B":= (Arrow A B) (at level 59, right associativity). +Notation "#" := Bot. +Notation "A //\\ B" := (Conjunct A B) (at level 57, left associativity). +Notation "A \\// B" := (Disjunct A B) (at level 58, left associativity). + +Definition ctx := Store form. + +Fixpoint pos_eq (m n:positive) {struct m} :bool := +match m with + xI mm => match n with xI nn => pos_eq mm nn | _ => false end +| xO mm => match n with xO nn => pos_eq mm nn | _ => false end +| xH => match n with xH => true | _ => false end +end. + +Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n. +induction m;simpl;destruct n;congruence || +(intro e;apply f_equal with positive;auto). +Qed. + +Fixpoint form_eq (p q:form) {struct p} :bool := +match p with + Atom m => match q with Atom n => pos_eq m n | _ => false end +| Arrow p1 p2 => +match q with + Arrow q1 q2 => form_eq p1 q1 && form_eq p2 q2 +| _ => false end +| Bot => match q with Bot => true | _ => false end +| Conjunct p1 p2 => +match q with + Conjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 +| _ => false +end +| Disjunct p1 p2 => +match q with + Disjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 +| _ => false +end +end. + +Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q. +induction p;destruct q;simpl;clean. +intro h;generalize (pos_eq_refl _ _ h);congruence. +caseq (form_eq p1 q1);clean. +intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. +caseq (form_eq p1 q1);clean. +intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. +caseq (form_eq p1 q1);clean. +intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. +Qed. + +Implicit Arguments form_eq_refl [p q]. + +Section with_env. + +Variable env:Store Prop. + +Fixpoint interp_form (f:form): Prop := +match f with +[n]=> match get n env with PNone => True | PSome P => P end +| A =>> B => (interp_form A) -> (interp_form B) +| # => False +| A //\\ B => (interp_form A) /\ (interp_form B) +| A \\// B => (interp_form A) \/ (interp_form B) +end. + +Notation "[[ A ]]" := (interp_form A). + +Fixpoint interp_ctx (hyps:ctx) (F:Full hyps) (G:Prop) {struct F} : Prop := +match F with + F_empty => G +| F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) +end. + +Require Export BinPos. + +Ltac wipe := intros;simpl;constructor. + +Lemma compose0 : +forall hyps F (A:Prop), + A -> + (interp_ctx hyps F A). +induction F;intros A H;simpl;auto. +Qed. + +Lemma compose1 : +forall hyps F (A B:Prop), + (A -> B) -> + (interp_ctx hyps F A) -> + (interp_ctx hyps F B). +induction F;intros A B H;simpl;auto. +apply IHF;auto. +Qed. + +Theorem compose2 : +forall hyps F (A B C:Prop), + (A -> B -> C) -> + (interp_ctx hyps F A) -> + (interp_ctx hyps F B) -> + (interp_ctx hyps F C). +induction F;intros A B C H;simpl;auto. +apply IHF;auto. +Qed. + +Theorem compose3 : +forall hyps F (A B C D:Prop), + (A -> B -> C -> D) -> + (interp_ctx hyps F A) -> + (interp_ctx hyps F B) -> + (interp_ctx hyps F C) -> + (interp_ctx hyps F D). +induction F;intros A B C D H;simpl;auto. +apply IHF;auto. +Qed. + +Lemma weaken : forall hyps F f G, + (interp_ctx hyps F G) -> + (interp_ctx (hyps\f) (F_push f hyps F) G). +induction F;simpl;intros;auto. +apply compose1 with ([[a]]-> G);auto. +Qed. + +Theorem project_In : forall hyps F g, +In g hyps F -> +interp_ctx hyps F [[g]]. +induction F;simpl. +contradiction. +intros g H;destruct H. +subst;apply compose0;simpl;trivial. +apply compose1 with [[g]];auto. +Qed. + +Theorem project : forall hyps F p g, +get p hyps = PSome g-> +interp_ctx hyps F [[g]]. +intros hyps F p g e; apply project_In. +apply get_In with p;assumption. +Qed. + +Implicit Arguments project [hyps p g]. + +Inductive proof:Set := + Ax : positive -> proof +| I_Arrow : proof -> proof +| E_Arrow : positive -> positive -> proof -> proof +| D_Arrow : positive -> proof -> proof -> proof +| E_False : positive -> proof +| I_And: proof -> proof -> proof +| E_And: positive -> proof -> proof +| D_And: positive -> proof -> proof +| I_Or_l: proof -> proof +| I_Or_r: proof -> proof +| E_Or: positive -> proof -> proof -> proof +| D_Or: positive -> proof -> proof +| Cut: form -> proof -> proof -> proof. + +Notation "hyps \ A" := (push A hyps) (at level 72,left associativity). + +Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool := + match P with + Ax i => + match get i hyps with + PSome F => form_eq F gl + | _ => false + end +| I_Arrow p => + match gl with + A =>> B => check_proof (hyps \ A) B p + | _ => false + end +| E_Arrow i j p => + match get i hyps,get j hyps with + PSome A,PSome (B =>>C) => + form_eq A B && check_proof (hyps \ C) (gl) p + | _,_ => false + end +| D_Arrow i p1 p2 => + match get i hyps with + PSome ((A =>>B)=>>C) => + (check_proof ( hyps \ B =>> C \ A) B p1) && (check_proof (hyps \ C) gl p2) + | _ => false + end +| E_False i => + match get i hyps with + PSome # => true + | _ => false + end +| I_And p1 p2 => + match gl with + A //\\ B => + check_proof hyps A p1 && check_proof hyps B p2 + | _ => false + end +| E_And i p => + match get i hyps with + PSome (A //\\ B) => check_proof (hyps \ A \ B) gl p + | _=> false + end +| D_And i p => + match get i hyps with + PSome (A //\\ B =>> C) => check_proof (hyps \ A=>>B=>>C) gl p + | _=> false + end +| I_Or_l p => + match gl with + (A \\// B) => check_proof hyps A p + | _ => false + end +| I_Or_r p => + match gl with + (A \\// B) => check_proof hyps B p + | _ => false + end +| E_Or i p1 p2 => + match get i hyps with + PSome (A \\// B) => + check_proof (hyps \ A) gl p1 && check_proof (hyps \ B) gl p2 + | _=> false + end +| D_Or i p => + match get i hyps with + PSome (A \\// B =>> C) => + (check_proof (hyps \ A=>>C \ B=>>C) gl p) + | _=> false + end +| Cut A p1 p2 => + check_proof hyps A p1 && check_proof (hyps \ A) gl p2 +end. + +Theorem interp_proof: +forall p hyps F gl, +check_proof hyps gl p = true -> interp_ctx hyps F [[gl]]. + +induction p;intros hyps F gl. + +(* cas Axiom *) +Focus 1. +simpl;caseq (get p hyps);clean. +intros f nth_f e;rewrite <- (form_eq_refl e). +apply project with p;trivial. + +(* Cas Arrow_Intro *) +Focus 1. +destruct gl;clean. +simpl;intros. +change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). +apply IHp;try constructor;trivial. + +(* Cas Arrow_Elim *) +Focus 1. +simpl check_proof;caseq (get p hyps);clean. +intros f ef;caseq (get p0 hyps);clean. +intros f0 ef0;destruct f0;clean. +caseq (form_eq f f0_1);clean. +simpl;intros e check_p1. +generalize (project F ef) (project F ef0) +(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); +clear check_p1 IHp p p0 p1 ef ef0. +simpl. +apply compose3. +rewrite (form_eq_refl e). +auto. + +(* cas Arrow_Destruct *) +Focus 1. +simpl;caseq (get p1 hyps);clean. +intros f ef;destruct f;clean. +destruct f1;clean. +caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean. +intros check_p1 check_p2. +generalize (project F ef) +(IHp1 (hyps \ f1_2 =>> f2 \ f1_1) +(F_push f1_1 (hyps \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) +(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). +simpl;apply compose3;auto. + +(* Cas False_Elim *) +Focus 1. +simpl;caseq (get p hyps);clean. +intros f ef;destruct f;clean. +intros _; generalize (project F ef). +apply compose1;apply False_ind. + +(* Cas And_Intro *) +Focus 1. +simpl;destruct gl;clean. +caseq (check_proof hyps gl1 p1);clean. +intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). +apply compose2 ;simpl;auto. + +(* cas And_Elim *) +Focus 1. +simpl;caseq (get p hyps);clean. +intros f ef;destruct f;clean. +intro check_p;generalize (project F ef) +(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). +simpl;apply compose2;intros [h1 h2];auto. + +(* cas And_Destruct *) +Focus 1. +simpl;caseq (get p hyps);clean. +intros f ef;destruct f;clean. +destruct f1;clean. +intro H;generalize (project F ef) +(IHp (hyps \ f1_1 =>> f1_2 =>> f2) +(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl. +apply compose2;auto. + +(* cas Or_Intro_left *) +Focus 1. +destruct gl;clean. +intro Hp;generalize (IHp hyps F gl1 Hp). +apply compose1;simpl;auto. + +(* cas Or_Intro_right *) +Focus 1. +destruct gl;clean. +intro Hp;generalize (IHp hyps F gl2 Hp). +apply compose1;simpl;auto. + +(* cas Or_elim *) +Focus 1. +simpl;caseq (get p1 hyps);clean. +intros f ef;destruct f;clean. +caseq (check_proof (hyps \ f1) gl p2);clean. +intros check_p1 check_p2;generalize (project F ef) +(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) +(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); +simpl;apply compose3;simpl;intro h;destruct h;auto. + +(* cas Or_Destruct *) +Focus 1. +simpl;caseq (get p hyps);clean. +intros f ef;destruct f;clean. +destruct f1;clean. +intro check_p0;generalize (project F ef) +(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) +(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) + (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl. +apply compose2;auto. + +(* cas Cut *) +Focus 1. +simpl;caseq (check_proof hyps f p1);clean. +intros check_p1 check_p2; +generalize (IHp1 hyps F f check_p1) +(IHp2 (hyps\f) (F_push f hyps F) gl check_p2); +simpl; apply compose2;auto. +Qed. + +Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True. +intros gl prf;caseq (check_proof empty gl prf);intro check_prf. +change (interp_ctx empty F_empty [[gl]]) ; +apply interp_proof with prf;assumption. +trivial. +Qed. + +End with_env. + +(* +(* A small example *) +Parameters A B C D:Prop. +Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C). +exact (Reflect (empty \ A \ B \ C) +([1] //\\ ([2] \\// [3]) =>> [1] //\\ [2] \\// [1] //\\ [3]) +(I_Arrow (E_And 1 (E_Or 3 + (I_Or_l (I_And (Ax 2) (Ax 4))) + (I_Or_r (I_And (Ax 2) (Ax 4))))))). +Qed. +Print toto. +*)
\ No newline at end of file diff --git a/contrib/rtauto/g_rtauto.ml4 b/contrib/rtauto/g_rtauto.ml4 new file mode 100644 index 000000000..ee47d0b02 --- /dev/null +++ b/contrib/rtauto/g_rtauto.ml4 @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$*) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +TACTIC EXTEND Rtauto + [ "Rtauto" ] -> [ Refl_tauto.rtauto_tac ] +END + diff --git a/contrib/rtauto/proof_search.ml b/contrib/rtauto/proof_search.ml new file mode 100644 index 000000000..9d9d66bb2 --- /dev/null +++ b/contrib/rtauto/proof_search.ml @@ -0,0 +1,546 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Term +open Util +open Goptions + +type s_info= + {mutable created_steps : int; (* node count*) + mutable pruned_steps : int; + mutable created_branches : int; (* path count *) + mutable pruned_branches : int; + mutable created_hyps : int; (* hyps count *) + mutable pruned_hyps : int; + mutable branch_failures : int; + mutable branch_successes : int; + mutable nd_branching : int} + +let s_info= + {created_steps = 0; (* node count*) + pruned_steps = 0; + created_branches = 0; (* path count *) + pruned_branches = 0; + created_hyps = 0; (* hyps count *) + pruned_hyps = 0; + branch_failures = 0; + branch_successes = 0; + nd_branching = 0} + +let reset_info () = + s_info.created_steps <- 0; (* node count*) + s_info.pruned_steps <- 0; + s_info.created_branches <- 0; (* path count *) + s_info.pruned_branches <- 0; + s_info.created_hyps <- 0; (* hyps count *) + s_info.pruned_hyps <- 0; + s_info.branch_failures <- 0; + s_info.branch_successes <- 0; + s_info.nd_branching <- 0 + +let pruning = ref true + +let opt_pruning= + {optsync=true; + optname="Rtauto Pruning"; + optkey=SecondaryTable("Rtauto","Pruning"); + optread=(fun () -> !pruning); + optwrite=(fun b -> pruning:=b)} + +let _ = declare_bool_option opt_pruning + +type form= + Atom of int + | Arrow of form * form + | Bot + | Conjunct of form * form + | Disjunct of form * form + +type tag=int + +let decomp_form=function + Atom i -> Some (i,[]) + | Arrow (f1,f2) -> Some (-1,[f1;f2]) + | Bot -> Some (-2,[]) + | Conjunct (f1,f2) -> Some (-3,[f1;f2]) + | Disjunct (f1,f2) -> Some (-4,[f1;f2]) + +module Fmap=Map.Make(struct type t=form let compare=compare end) + +type sequent = + {rev_hyps: form Intmap.t; + norev_hyps: form Intmap.t; + size:int; + left:int Fmap.t; + right:(int*form) list Fmap.t; + cnx:(int*int*form*form) list; + abs:int option; + gl:form} + +let add_one_arrow i f1 f2 m= + try Fmap.add f1 ((i,f2)::(Fmap.find f1 m)) m with + Not_found -> + Fmap.add f1 [i,f2] m + +type proof = + Ax of int + | I_Arrow of proof + | E_Arrow of int*int*proof + | D_Arrow of int*proof*proof + | E_False of int + | I_And of proof*proof + | E_And of int*proof + | D_And of int*proof + | I_Or_l of proof + | I_Or_r of proof + | E_Or of int*proof*proof + | D_Or of int*proof + | Pop of int*proof + +type rule = + SAx of int + | SI_Arrow + | SE_Arrow of int*int + | SD_Arrow of int + | SE_False of int + | SI_And + | SE_And of int + | SD_And of int + | SI_Or_l + | SI_Or_r + | SE_Or of int + | SD_Or of int + +let add_step s sub = + match s,sub with + SAx i,[] -> Ax i + | SI_Arrow,[p] -> I_Arrow p + | SE_Arrow(i,j),[p] -> E_Arrow (i,j,p) + | SD_Arrow i,[p1;p2] -> D_Arrow (i,p1,p2) + | SE_False i,[] -> E_False i + | SI_And,[p1;p2] -> I_And(p1,p2) + | SE_And i,[p] -> E_And(i,p) + | SD_And i,[p] -> D_And(i,p) + | SI_Or_l,[p] -> I_Or_l p + | SI_Or_r,[p] -> I_Or_r p + | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) + | SD_Or i,[p] -> D_Or(i,p) + | _,_ -> anomaly "add_step: wrong arity" + +type 'a with_deps = + {dep_it:'a; + dep_goal:bool; + dep_hyps:Intset.t} + +type slice= + {proofs_done:proof list; + proofs_todo:sequent with_deps list; + step:rule; + needs_goal:bool; + needs_hyps:Intset.t; + changes_goal:bool; + creates_hyps:Intset.t} + +type state = + Complete of proof + | Incomplete of sequent * slice list + +let project = function + Complete prf -> prf + | Incomplete (_,_) -> anomaly "not a successful state" + +let pop n prf = + let nprf= + match prf.dep_it with + Pop (i,p) -> Pop (i+n,p) + | p -> Pop(n,p) in + {prf with dep_it = nprf} + +let rec fill stack proof = + match stack with + [] -> Complete proof.dep_it + | slice::super -> + if + !pruning && + slice.proofs_done=[] && + not (slice.changes_goal && proof.dep_goal) && + not (Intset.exists + (fun i -> Intset.mem i proof.dep_hyps) + slice.creates_hyps) + then + begin + s_info.pruned_steps<-s_info.pruned_steps+1; + s_info.pruned_branches<- s_info.pruned_branches + + List.length slice.proofs_todo; + let created_here=Intset.cardinal slice.creates_hyps in + s_info.pruned_hyps<-s_info.pruned_hyps+ + List.fold_left + (fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps) + created_here slice.proofs_todo; + fill super (pop (Intset.cardinal slice.creates_hyps) proof) + end + else + let dep_hyps= + Intset.union slice.needs_hyps + (Intset.diff proof.dep_hyps slice.creates_hyps) in + let dep_goal= + slice.needs_goal || + ((not slice.changes_goal) && proof.dep_goal) in + let proofs_done= + proof.dep_it::slice.proofs_done in + match slice.proofs_todo with + [] -> + fill super {dep_it = + add_step slice.step (List.rev proofs_done); + dep_goal = dep_goal; + dep_hyps = dep_hyps} + | current::next -> + let nslice= + {proofs_done=proofs_done; + proofs_todo=next; + step=slice.step; + needs_goal=dep_goal; + needs_hyps=dep_hyps; + changes_goal=current.dep_goal; + creates_hyps=current.dep_hyps} in + Incomplete (current.dep_it,nslice::super) + +let append stack (step,subgoals) = + s_info.created_steps<-s_info.created_steps+1; + match subgoals with + [] -> + s_info.branch_successes<-s_info.branch_successes+1; + fill stack {dep_it=add_step step.dep_it []; + dep_goal=step.dep_goal; + dep_hyps=step.dep_hyps} + | hd :: next -> + s_info.created_branches<- + s_info.created_branches+List.length next; + let slice= + {proofs_done=[]; + proofs_todo=next; + step=step.dep_it; + needs_goal=step.dep_goal; + needs_hyps=step.dep_hyps; + changes_goal=hd.dep_goal; + creates_hyps=hd.dep_hyps} in + Incomplete(hd.dep_it,slice::stack) + +let embed seq= + {dep_it=seq; + dep_goal=false; + dep_hyps=Intset.empty} + +let change_goal seq gl= + {seq with + dep_it={seq.dep_it with gl=gl}; + dep_goal=true} + +let add_hyp seqwd f= + s_info.created_hyps<-s_info.created_hyps+1; + let seq=seqwd.dep_it in + let num = seq.size+1 in + let left = Fmap.add f num seq.left in + let cnx,right= + try + let l=Fmap.find f seq.right in + List.fold_right (fun (i,f0) l0 -> (num,i,f,f0)::l0) l seq.cnx, + Fmap.remove f seq.right + with Not_found -> seq.cnx,seq.right in + let nseq= + match f with + Bot -> + {seq with + left=left; + right=right; + size=num; + abs=Some num; + cnx=cnx} + | Atom _ -> + {seq with + size=num; + left=left; + right=right; + cnx=cnx} + | Conjunct (_,_) | Disjunct (_,_) -> + {seq with + rev_hyps=Intmap.add num f seq.rev_hyps; + size=num; + left=left; + right=right; + cnx=cnx} + | Arrow (f1,f2) -> + let ncnx,nright= + try + let i = Fmap.find f1 seq.left in + (i,num,f1,f2)::cnx,right + with Not_found -> + cnx,(add_one_arrow num f1 f2 right) in + match f1 with + Conjunct (_,_) | Disjunct (_,_) -> + {seq with + rev_hyps=Intmap.add num f seq.rev_hyps; + size=num; + left=left; + right=nright; + cnx=ncnx} + | Arrow(_,_) -> + {seq with + norev_hyps=Intmap.add num f seq.norev_hyps; + size=num; + left=left; + right=nright; + cnx=ncnx} + | _ -> + {seq with + size=num; + left=left; + right=nright; + cnx=ncnx} in + {seqwd with + dep_it=nseq; + dep_hyps=Intset.add num seqwd.dep_hyps} + +exception Here_is of (int*form) + +let choose m= + try + Intmap.iter (fun i f -> raise (Here_is (i,f))) m; + raise Not_found + with + Here_is (i,f) -> (i,f) + + +let search_or seq= + match seq.gl with + Disjunct (f1,f2) -> + [{dep_it = SI_Or_l; + dep_goal = true; + dep_hyps = Intset.empty}, + [change_goal (embed seq) f1]; + {dep_it = SI_Or_r; + dep_goal = true; + dep_hyps = Intset.empty}, + [change_goal (embed seq) f2]] + | _ -> [] + +let search_norev seq= + let goals=ref (search_or seq) in + let add_one i f= + match f with + Arrow (Arrow (f1,f2),f3) -> + let nseq = + {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in + goals:= + ({dep_it=SD_Arrow(i); + dep_goal=false; + dep_hyps=Intset.singleton i}, + [add_hyp + (add_hyp + (change_goal (embed nseq) f2) + (Arrow(f2,f3))) + f1; + add_hyp (embed nseq) f3]):: !goals + | _ -> anomaly "search_no_rev: can't happen" in + Intmap.iter add_one seq.norev_hyps; + List.rev !goals + +let search_in_rev_hyps seq= + try + let i,f=choose seq.rev_hyps in + let make_step step= + {dep_it=step; + dep_goal=false; + dep_hyps=Intset.singleton i} in + let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in + match f with + Conjunct (f1,f2) -> + [make_step (SE_And(i)), + [add_hyp (add_hyp (embed nseq) f1) f2]] + | Disjunct (f1,f2) -> + [make_step (SE_Or(i)), + [add_hyp (embed nseq) f1;add_hyp (embed nseq) f2]] + | Arrow (Conjunct (f1,f2),f0) -> + [make_step (SD_And(i)), + [add_hyp (embed nseq) (Arrow (f1,Arrow (f2,f0)))]] + | Arrow (Disjunct (f1,f2),f0) -> + [make_step (SD_Or(i)), + [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] + | _ -> anomaly "search_in_rev_hyps: can't happen" + with + Not_found -> search_norev seq + +let search_rev seq= + match seq.cnx with + (i,j,f1,f2)::next -> + let nseq= + match f1 with + Conjunct (_,_) | Disjunct (_,_) -> + {seq with cnx=next; + rev_hyps=Intmap.remove j seq.rev_hyps} + | Arrow (_,_) -> + {seq with cnx=next; + norev_hyps=Intmap.remove j seq.norev_hyps} + | _ -> + {seq with cnx=next} in + [{dep_it=SE_Arrow(i,j); + dep_goal=false; + dep_hyps=Intset.add i (Intset.singleton j)}, + [add_hyp (embed nseq) f2]] + | [] -> + match seq.gl with + Arrow (f1,f2) -> + [{dep_it=SI_Arrow; + dep_goal=true; + dep_hyps=Intset.empty}, + [add_hyp (change_goal (embed seq) f2) f1]] + | Conjunct (f1,f2) -> + [{dep_it=SI_And; + dep_goal=true; + dep_hyps=Intset.empty},[change_goal (embed seq) f1; + change_goal (embed seq) f2]] + | _ -> search_in_rev_hyps seq + +let search_all seq= + match seq.abs with + Some i -> + [{dep_it=SE_False (i); + dep_goal=false; + dep_hyps=Intset.singleton i},[]] + | None -> + try + let ax = Fmap.find seq.gl seq.left in + [{dep_it=SAx (ax); + dep_goal=true; + dep_hyps=Intset.singleton ax},[]] + with Not_found -> search_rev seq + +let bare_sequent = embed + {rev_hyps=Intmap.empty; + norev_hyps=Intmap.empty; + size=0; + left=Fmap.empty; + right=Fmap.empty; + cnx=[]; + abs=None; + gl=Bot} + +let init_state hyps gl= + let init = change_goal bare_sequent gl in + let goal=List.fold_right (fun (_,f,_) seq ->add_hyp seq f) hyps init in + Incomplete (goal.dep_it,[]) + +let success= function + Complete _ -> true + | Incomplete (_,_) -> false + +let branching = function + Incomplete (seq,stack) -> + check_for_interrupt (); + let successors = search_all seq in + let _ = + match successors with + [] -> s_info.branch_failures<-s_info.branch_failures+1 + | _::next -> + s_info.nd_branching<-s_info.nd_branching+List.length next in + List.map (append stack) successors + | Complete prf -> anomaly "already succeeded" + +open Pp + +let rec pp_form = + function + Arrow(f1,f2) -> (pp_or f1) ++ (str " -> ") ++ (pp_form f2) + | f -> pp_or f +and pp_or = function + Disjunct(f1,f2) -> + (pp_or f1) ++ (str " \\/ ") ++ (pp_and f2) + | f -> pp_and f +and pp_and = function + Conjunct(f1,f2) -> + (pp_and f1) ++ (str " /\\ ") ++ (pp_atom f2) + | f -> pp_atom f +and pp_atom= function + Bot -> str "#" + | Atom n -> int n + | f -> str "(" ++ hv 2 (pp_form f) ++ str ")" + +let pr_form f = msg (pp_form f) + +let pp_intmap map = + let pp=ref (str "") in + Intmap.iter (fun i obj -> pp:= (!pp ++ + pp_form obj ++ cut ())) map; + str "{ " ++ v 0 (!pp) ++ str " }" + +let pp_list pp_obj l= +let pp=ref (str "") in + List.iter (fun o -> pp := !pp ++ (pp_obj o) ++ str ", ") l; + str "[ " ++ !pp ++ str "]" + +let pp_mapint map = + let pp=ref (str "") in + Fmap.iter (fun obj l -> pp:= (!pp ++ + pp_form obj ++ str " => " ++ + pp_list (fun (i,f) -> pp_form f) l ++ + cut ()) ) map; + str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () + +let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 + +let pp_gl gl= cut () ++ + str "{ " ++ vb 0 ++ + begin + match gl.abs with + None -> str "" + | Some i -> str "ABSURD" ++ cut () + end ++ + str "rev =" ++ pp_intmap gl.rev_hyps ++ cut () ++ + str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ + str "arrows=" ++ pp_mapint gl.right ++ cut () ++ + str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ + str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () + +let pp = + function + Incomplete(gl,ctx) -> msgnl (pp_gl gl) + | _ -> msg (str "<complete>") + +let pp_info () = + let count_info = + if !pruning then + str "Proof steps : " ++ + int s_info.created_steps ++ str " created / " ++ + int s_info.pruned_steps ++ str " pruned" ++ fnl () ++ + str "Proof branches : " ++ + int s_info.created_branches ++ str " created / " ++ + int s_info.pruned_branches ++ str " pruned" ++ fnl () ++ + str "Hypotheses : " ++ + int s_info.created_hyps ++ str " created / " ++ + int s_info.pruned_hyps ++ str " pruned" ++ fnl () + else + str "Pruning is off" ++ fnl () ++ + str "Proof steps : " ++ + int s_info.created_steps ++ str " created" ++ fnl () ++ + str "Proof branches : " ++ + int s_info.created_branches ++ str " created" ++ fnl () ++ + str "Hypotheses : " ++ + int s_info.created_hyps ++ str " created" ++ fnl () in + msgnl + ( str "Proof-search statistics :" ++ fnl () ++ + count_info ++ + str "Branch ends: " ++ + int s_info.branch_successes ++ str " successes / " ++ + int s_info.branch_failures ++ str " failures" ++ fnl () ++ + str "Non-deterministic choices : " ++ + int s_info.nd_branching ++ str " branches") + + + diff --git a/contrib/rtauto/proof_search.mli b/contrib/rtauto/proof_search.mli new file mode 100644 index 000000000..a0e86b8d6 --- /dev/null +++ b/contrib/rtauto/proof_search.mli @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +type form= + Atom of int + | Arrow of form * form + | Bot + | Conjunct of form * form + | Disjunct of form * form + +type proof = + Ax of int + | I_Arrow of proof + | E_Arrow of int*int*proof + | D_Arrow of int*proof*proof + | E_False of int + | I_And of proof*proof + | E_And of int*proof + | D_And of int*proof + | I_Or_l of proof + | I_Or_r of proof + | E_Or of int*proof*proof + | D_Or of int*proof + | Pop of int*proof + +type state + +val project: state -> proof + +val init_state : ('a * form * 'b) list -> form -> state + +val branching: state -> state list + +val success: state -> bool + +val pp: state -> unit + +val pr_form : form -> unit + +val reset_info : unit -> unit + +val pp_info : unit -> unit diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml new file mode 100644 index 000000000..0865a825c --- /dev/null +++ b/contrib/rtauto/refl_tauto.ml @@ -0,0 +1,337 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +module Search = Explore.Make(Proof_search) + +open Util +open Term +open Termops +open Names +open Evd +open Tacmach +open Proof_search + +let force count lazc = incr count;Lazy.force lazc + +let step_count = ref 0 + +let node_count = ref 0 + +let logic_constant = + Coqlib.gen_constant "refl_tauto" ["Init";"Logic"] + +let li_False = lazy (destInd (logic_constant "False")) +let li_and = lazy (destInd (logic_constant "and")) +let li_or = lazy (destInd (logic_constant "or")) + +let data_constant = + Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"] + +let l_true_equals_true = + lazy (mkApp(logic_constant "refl_equal", + [|data_constant "bool";data_constant "true"|])) + +let pos_constant = + Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"] + +let l_xI = lazy (pos_constant "xI") +let l_xO = lazy (pos_constant "xO") +let l_xH = lazy (pos_constant "xH") + +let store_constant = + Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"] + +let l_empty = lazy (store_constant "empty") +let l_push = lazy (store_constant "push") + +let constant= + Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"] + +let l_Reflect = lazy (constant "Reflect") + +let l_Atom = lazy (constant "Atom") +let l_Arrow = lazy (constant "Arrow") +let l_Bot = lazy (constant "Bot") +let l_Conjunct = lazy (constant "Conjunct") +let l_Disjunct = lazy (constant "Disjunct") + +let l_Ax = lazy (constant "Ax") +let l_I_Arrow = lazy (constant "I_Arrow") +let l_E_Arrow = lazy (constant "E_Arrow") +let l_D_Arrow = lazy (constant "D_Arrow") +let l_E_False = lazy (constant "E_False") +let l_I_And = lazy (constant "I_And") +let l_E_And = lazy (constant "E_And") +let l_D_And = lazy (constant "D_And") +let l_I_Or_l = lazy (constant "I_Or_l") +let l_I_Or_r = lazy (constant "I_Or_r") +let l_E_Or = lazy (constant "E_Or") +let l_D_Or = lazy (constant "D_Or") + + +let special_whd gl= + let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let special_nf gl= + let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +type atom_env= + {mutable next:int; + mutable env:(constr*int) list} + +let make_atom atom_env term= + try + let (_,i)= + List.find (fun (t,_)-> eq_constr term t) atom_env.env + in Atom i + with Not_found -> + let i=atom_env.next in + atom_env.env <- (term,i)::atom_env.env; + atom_env.next<- i + 1; + Atom i + +let rec make_form atom_env gls term = + let normalize=special_nf gls in + let cciterm=special_whd gls term in + match kind_of_term cciterm with + Prod(_,a,b) -> + if not (dependent (mkRel 1) b) && + Retyping.get_sort_family_of + (pf_env gls) (Tacmach.project gls) a = InProp + then + let fa=make_form atom_env gls a in + let fb=make_form atom_env gls b in + Arrow (fa,fb) + else + make_atom atom_env (normalize term) + | Cast(a,b) -> + make_form atom_env gls a + | Ind ind -> + if ind = Lazy.force li_False then + Bot + else + make_atom atom_env (normalize term) + | App(hd,argv) when Array.length argv = 2 -> + begin + try + let ind = destInd hd in + if ind = Lazy.force li_and then + let fa=make_form atom_env gls argv.(0) in + let fb=make_form atom_env gls argv.(1) in + Conjunct (fa,fb) + else if ind = Lazy.force li_or then + let fa=make_form atom_env gls argv.(0) in + let fb=make_form atom_env gls argv.(1) in + Disjunct (fa,fb) + else make_atom atom_env (normalize term) + with Invalid_argument _ -> make_atom atom_env (normalize term) + end + | _ -> make_atom atom_env (normalize term) + +let rec make_hyps atom_env gls lenv = function + [] -> [] + | (_,Some body,typ)::rest -> + make_hyps atom_env gls (typ::body::lenv) rest + | (id,None,typ)::rest -> + let hrec= + make_hyps atom_env gls (typ::lenv) rest in + if List.exists (dependent (mkVar id)) lenv || + (Retyping.get_sort_family_of + (pf_env gls) (Tacmach.project gls) typ <> InProp) + then + hrec + else + (id,make_form atom_env gls typ)::hrec + +let rec build_pos n = + if n<=1 then force node_count l_xH + else if n land 1 = 0 then + mkApp (force node_count l_xO,[|build_pos (n asr 1)|]) + else + mkApp (force node_count l_xI,[|build_pos (n asr 1)|]) + +let rec build_form = function + Atom n -> mkApp (force node_count l_Atom,[|build_pos n|]) + | Arrow (f1,f2) -> + mkApp (force node_count l_Arrow,[|build_form f1;build_form f2|]) + | Bot -> force node_count l_Bot + | Conjunct (f1,f2) -> + mkApp (force node_count l_Conjunct,[|build_form f1;build_form f2|]) + | Disjunct (f1,f2) -> + mkApp (force node_count l_Disjunct,[|build_form f1;build_form f2|]) + +let rec decal k = function + [] -> k + | (start,delta)::rest -> + if k>start then + k - delta + else + decal k rest + +let add_pop size d pops= + match pops with + [] -> [size+d,d] + | (_,sum)::_ -> (size+sum,sum+d)::pops + +let rec build_proof pops size = + function + Ax i -> + mkApp (force step_count l_Ax, + [|build_pos (decal i pops)|]) + | I_Arrow p -> + mkApp (force step_count l_I_Arrow, + [|build_proof pops (size + 1) p|]) + | E_Arrow(i,j,p) -> + mkApp (force step_count l_E_Arrow, + [|build_pos (decal i pops); + build_pos (decal j pops); + build_proof pops (size + 1) p|]) + | D_Arrow(i,p1,p2) -> + mkApp (force step_count l_D_Arrow, + [|build_pos (decal i pops); + build_proof pops (size + 2) p1; + build_proof pops (size + 1) p2|]) + | E_False i -> + mkApp (force step_count l_E_False, + [|build_pos (decal i pops)|]) + | I_And(p1,p2) -> + mkApp (force step_count l_I_And, + [|build_proof pops size p1; + build_proof pops size p2|]) + | E_And(i,p) -> + mkApp (force step_count l_E_And, + [|build_pos (decal i pops); + build_proof pops (size + 2) p|]) + | D_And(i,p) -> + mkApp (force step_count l_D_And, + [|build_pos (decal i pops); + build_proof pops (size + 1) p|]) + | I_Or_l(p) -> + mkApp (force step_count l_I_Or_l, + [|build_proof pops size p|]) + | I_Or_r(p) -> + mkApp (force step_count l_I_Or_r, + [|build_proof pops size p|]) + | E_Or(i,p1,p2) -> + mkApp (force step_count l_E_Or, + [|build_pos (decal i pops); + build_proof pops (size + 1) p1; + build_proof pops (size + 1) p2|]) + | D_Or(i,p) -> + mkApp (force step_count l_D_Or, + [|build_pos (decal i pops); + build_proof pops (size + 2) p|]) + | Pop(d,p) -> + build_proof (add_pop size d pops) size p + +let build_env gamma= + List.fold_right (fun (p,_) e -> + mkApp(force node_count l_push,[|mkProp;p;e|])) + gamma.env (mkApp (force node_count l_empty,[|mkProp|])) + +open Goptions + +let verbose = ref false + +let opt_verbose= + {optsync=true; + optname="Rtauto Verbose"; + optkey=SecondaryTable("Rtauto","Verbose"); + optread=(fun () -> !verbose); + optwrite=(fun b -> verbose:=b)} + +let _ = declare_bool_option opt_verbose + +let check = ref false + +let opt_check= + {optsync=true; + optname="Rtauto Check"; + optkey=SecondaryTable("Rtauto","Check"); + optread=(fun () -> !check); + optwrite=(fun b -> check:=b)} + +let _ = declare_bool_option opt_check + +open Pp + +let rtauto_tac gls= + Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; + let gamma={next=1;env=[]} in + let gl=gls.it.evar_concl in + let _= + if Retyping.get_sort_family_of + (pf_env gls) (Tacmach.project gls) gl <> InProp + then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in + let glf=make_form gamma gls gl in + let hyps=make_hyps gamma gls [gl] gls.it.evar_hyps in + let formula= + List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in + let search_fun = + if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then + Search.debug_depth_first + else + Search.depth_first in + let _ = + begin + reset_info (); + if !verbose then + msgnl (str "Starting proof-search ..."); + end in + let search_start_time = System.get_time () in + let prf = + try project (search_fun (init_state [] formula)) + with Not_found -> + errorlabstrm "rtauto" (Pp.str "rtauto could'nt find any proof") in + let search_end_time = System.get_time () in + let _ = if !verbose then + begin + msgnl (str "Proof tree found in " ++ + System.fmt_time_difference search_start_time search_end_time); + pp_info (); + msgnl (str "Building proof term ... ") + end in + let build_start_time=System.get_time () in + let _ = step_count := 0; node_count := 0 in + let nhyps = List.length hyps in + let main = mkApp (force node_count l_Reflect, + [|build_env gamma; + build_form formula; + build_proof [] 0 prf|]) in + let term= + Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in + let build_end_time=System.get_time () in + let _ = if !verbose then + begin + msgnl (str "Proof term built in " ++ + System.fmt_time_difference build_start_time build_end_time ++ + fnl () ++ + str "Proof size : " ++ int !step_count ++ + str " steps" ++ fnl () ++ + str "Proof term size : " ++ int (!step_count+ !node_count) ++ + str " nodes (constants)" ++ fnl () ++ + str "Giving proof term to Coq ... ") + end in + let tac_start_time = System.get_time () in + let result= + if !check then + Tactics.exact_check term gls + else + Tactics.exact_no_check term gls in + let tac_end_time = System.get_time () in + let _ = + if !check then msgnl (str "Proof term type-checking is on"); + if !verbose then + msgnl (str "Internal tactic executed in " ++ + System.fmt_time_difference tac_start_time tac_end_time) in + result + diff --git a/contrib/rtauto/refl_tauto.mli b/contrib/rtauto/refl_tauto.mli new file mode 100644 index 000000000..a6d68a226 --- /dev/null +++ b/contrib/rtauto/refl_tauto.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id$ *) + +(* raises Not_found if no proof is found *) + +type atom_env= + {mutable next:int; + mutable env:(Term.constr*int) list} + +val make_form : atom_env -> + Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form + +val make_hyps : + atom_env -> + Proof_type.goal Tacmach.sigma -> + Term.types list -> + (Names.identifier * Term.types option * Term.types) list -> + (Names.identifier * Proof_search.form) list + +val rtauto_tac : Proof_type.tactic |