diff options
| -rw-r--r-- | .depend | 111 | ||||
| -rw-r--r-- | .depend.coq | 5 | ||||
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | states/MakeInitial.v | 1 | ||||
| -rw-r--r-- | tactics/Tauto.v | 12 | ||||
| -rw-r--r-- | tactics/tauto.ml | 1901 | ||||
| -rw-r--r-- | tactics/tauto.mli | 127 |
9 files changed, 2124 insertions, 49 deletions
@@ -32,6 +32,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/constant.cmi kernel/environ.cmi \ kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi library/global.cmi: kernel/constant.cmi kernel/environ.cmi \ @@ -47,8 +49,6 @@ library/library.cmi: lib/pp.cmi library/nametab.cmi: kernel/names.cmi library/redinfo.cmi: kernel/names.cmi kernel/term.cmi library/summary.cmi: kernel/names.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ @@ -71,10 +71,6 @@ parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi -pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ - kernel/evd.cmi kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi \ - lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi pretyping/class.cmi: pretyping/classops.cmi library/declare.cmi \ @@ -159,6 +155,7 @@ tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ tactics/tacticals.cmi kernel/term.cmi +tactics/tauto.cmi: proofs/tacmach.cmi kernel/term.cmi tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi proofs/proof_trees.cmi kernel/sign.cmi \ @@ -177,11 +174,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \ toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ proofs/proof_trees.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi @@ -298,22 +295,30 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi lib/dyn.cmx: lib/util.cmx lib/dyn.cmi lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.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/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/profile.cmo: lib/system.cmi lib/profile.cmi lib/profile.cmx: lib/system.cmx lib/profile.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi library/impargs.cmi \ library/indrec.cmi kernel/inductive.cmi library/lib.cmi \ @@ -386,14 +391,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \ @@ -560,20 +557,6 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ pretyping/pretype_errors.cmx kernel/reduction.cmx pretyping/retyping.cmx \ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ pretyping/evarutil.cmi -pretyping/oldcases.cmo: kernel/environ.cmi pretyping/evarconv.cmi \ - pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \ - library/global.cmi library/indrec.cmi kernel/inductive.cmi \ - kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ - pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi -pretyping/oldcases.cmx: kernel/environ.cmx pretyping/evarconv.cmx \ - pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \ - library/global.cmx library/indrec.cmx kernel/inductive.cmx \ - kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ - pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx pretyping/pretype_errors.cmo: kernel/environ.cmi library/global.cmi \ kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \ kernel/type_errors.cmi pretyping/pretype_errors.cmi @@ -808,6 +791,32 @@ tactics/hiddentac.cmo: proofs/proof_trees.cmi tactics/tacentries.cmi \ proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi tactics/hiddentac.cmx: proofs/proof_trees.cmx tactics/tacentries.cmx \ proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi +tactics/inv.cmo: tactics/auto.cmi proofs/clenv.cmi tactics/elim.cmi \ + kernel/environ.cmi tactics/equality.cmi kernel/generic.cmi \ + library/indrec.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi tactics/wcclausenv.cmi +tactics/inv.cmx: tactics/auto.cmx proofs/clenv.cmx tactics/elim.cmx \ + kernel/environ.cmx tactics/equality.cmx kernel/generic.cmx \ + library/indrec.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx tactics/wcclausenv.cmx +tactics/leminv.cmo: proofs/clenv.cmi library/declare.cmi \ + toplevel/discharge.cmi kernel/environ.cmi tactics/equality.cmi \ + kernel/evd.cmi kernel/generic.cmi tactics/inv.cmo kernel/names.cmi \ + tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi toplevel/vernacinterp.cmi tactics/wcclausenv.cmi +tactics/leminv.cmx: proofs/clenv.cmx library/declare.cmx \ + toplevel/discharge.cmx kernel/environ.cmx tactics/equality.cmx \ + kernel/evd.cmx kernel/generic.cmx tactics/inv.cmx kernel/names.cmx \ + tactics/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/nbtermdn.cmo: tactics/btermdn.cmi kernel/generic.cmi lib/gmap.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ kernel/term.cmi tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi @@ -864,6 +873,18 @@ tactics/tactics.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx lib/util.cmx \ tactics/tactics.cmi +tactics/tauto.cmo: tactics/auto.cmi proofs/clenv.cmi library/declare.cmi \ + kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ + library/nametab.cmi tactics/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ + kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ + tactics/tauto.cmi +tactics/tauto.cmx: tactics/auto.cmx proofs/clenv.cmx library/declare.cmx \ + kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ + library/nametab.cmx tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ + kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ + tactics/tauto.cmi tactics/termdn.cmo: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi \ lib/util.cmi tactics/termdn.cmi tactics/termdn.cmx: tactics/dn.cmx kernel/generic.cmx kernel/term.cmx \ @@ -878,8 +899,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coqdep.cmo: config/coq_config.cmi -tools/coqdep.cmx: config/coq_config.cmx +tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo +tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx +tools/gallina.cmo: tools/gallina_lexer.cmo +tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \ parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi library/indrec.cmi \ @@ -990,6 +1015,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \ toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: toplevel/usage.cmi toplevel/usage.cmx: toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \ + lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ + library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ + lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ + library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \ library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \ @@ -1026,11 +1059,3 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \ toplevel/himsg.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_trees.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \ - lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ - library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ - lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ - library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi diff --git a/.depend.coq b/.depend.coq index 946d02c0e..06349fb1c 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,7 +1,7 @@ theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v tactics/Equality.vo theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo -theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo +theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/g_zsyntax.cmo theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo @@ -50,9 +50,10 @@ theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theorie theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/g_natsyntax.cmo test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v +tactics/Tauto.vo: tactics/Tauto.v tactics/Equality.vo: tactics/Equality.v syntax/PPTactic.vo: syntax/PPTactic.v syntax/PPConstr.vo: syntax/PPConstr.v syntax/PPCases.vo: syntax/PPCases.v syntax/MakeBare.vo: syntax/MakeBare.v -states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo +states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo tactics/Tauto.vo @@ -108,7 +108,8 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \ toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo -HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo +HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ + tactics/tauto.cmo CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -199,12 +200,12 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) -q -I theories/Init -is states/barestate.coq $< -TACTICSVO=tactics/Equality.vo +TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) -q -I tactics -is states/barestate.coq $< -states/initial.coq: states/barestate.coq $(INITVO) $(TACTICSVO) +states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) ./coqtop.byte -q -batch -silent -is states/barestate.coq -I tactics -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: @@ -234,7 +235,11 @@ ZARITHVO=theories/Zarith/Wf_Z.vo theories/Zarith/Zsyntax.vo \ theories/Zarith/ZArith_dec.vo theories/Zarith/fast_integer.vo \ theories/Zarith/Zmisc.vo theories/Zarith/zarith_aux.vo -theories: $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) +THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) + +$(THEORIESVO): states/initial.coq + +theories: $(THEORIESVO) init: $(INITVO) logic: $(LOGICVO) diff --git a/kernel/environ.ml b/kernel/environ.ml index e203af98e..b58145fc3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -197,6 +197,8 @@ let prod_name env (n,a,b) = mkProd (named_hd env a n) a b let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous) a b +let lambda_name env (n,a,b) = mkLambda (named_hd env a n) a b + (* Abstractions. *) let evaluable_abst env = function diff --git a/kernel/environ.mli b/kernel/environ.mli index 31edb0d7f..f9b17b76d 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -54,6 +54,7 @@ val id_of_name_using_hdchar : env -> constr -> name -> identifier val named_hd : env -> constr -> name -> name val prod_name : env -> name * constr * constr -> constr val lambda_create : env -> constr * constr -> constr +val lambda_name : env -> name * constr * constr -> constr val translucent_abst : env -> constr -> bool val evaluable_abst : env -> constr -> bool diff --git a/states/MakeInitial.v b/states/MakeInitial.v index 24bad16b7..608437bfc 100644 --- a/states/MakeInitial.v +++ b/states/MakeInitial.v @@ -2,3 +2,4 @@ Require Export Prelude. Require Export Logic_Type. Require Export Logic_TypeSyntax. Require Export Equality. +Require Export Tauto. diff --git a/tactics/Tauto.v b/tactics/Tauto.v new file mode 100644 index 000000000..2f7cbb0ea --- /dev/null +++ b/tactics/Tauto.v @@ -0,0 +1,12 @@ + +(* $Id$ *) + +Declare ML Module "Tauto". + +Grammar tactic simple_tactic := + tauto [ "Tauto" ] -> [(Tauto)] +| intuition [ "Intuition" ] -> [(Intuition)]. + +Syntax tactic level 0: + tauto [(Tauto)] -> ["Tauto"] +| intuition [(Intuition)] -> ["Intuition"]. diff --git a/tactics/tauto.ml b/tactics/tauto.ml new file mode 100644 index 000000000..dc69a9cf4 --- /dev/null +++ b/tactics/tauto.ml @@ -0,0 +1,1901 @@ + +(* $Id$ *) + +(* Autor: Cesar A. Munnoz H *) + +open Pp +open Util +open Names +open Generic +open Term +open Sign +open Environ +open Declare +open Tacmach +open Reduction +open Tacticals +open Tactics +open Pattern +open Auto +(* Chet's code *) +open Proof_trees +open Clenv +open Pattern + +let hlset_subset hls1 hls2 = + List.for_all (fun e -> List.exists (fun e' -> eq_constr e e') hls2) hls1 + +let hlset_eq hls1 hls2 = + hlset_subset hls1 hls2 & hlset_subset hls2 hls1 + +let eq_gls g1 g2 = + eq_constr (pf_concl g1) (pf_concl g2) + & (let hl1 = vals_of_sign (pf_untyped_hyps g1) + and hl2 = vals_of_sign (pf_untyped_hyps g2) in + hlset_eq hl1 hl2) + +let gls_memb bTS g = List.exists (eq_gls g) bTS + +let gls_add g bTS = + if gls_memb bTS g then error "backtrack in tauto"; + g::bTS + +let classically cltac = function + | (Some _ as cls) -> (tclTHEN (cltac cls) (clear_clause cls)) + | None -> cltac None + +let somatch m pat = somatch None (get_pat pat) m +let module_mark = ["#Logic.obj"] +let mmk = make_module_marker ["#Prelude.obj"] +let false_pattern = put_pat mmk "False" +let true_pattern = put_pat mmk "True" +let and_pattern = put_pat mmk "(and ? ?)" +let or_pattern = put_pat mmk "(or ? ?)" +let eq_pattern = put_pat mmk "(eq ? ? ?)" +let pi_pattern = put_pat mmk "(x:?)((?)@[x])" +let imply_pattern = put_pat mmk "?1->?2" +let iff_pattern = put_pat mmk "(iff ? ?)" +let not_pattern = put_pat mmk "(not ?1)" +let mkIMP a b = soinstance imply_pattern [a;b] + +let is_atomic m = + (not (is_conjunction m) || + (is_disjunction m) || + (somatches m pi_pattern) || + (somatches m not_pattern)) + +let hypothesis = function Some id -> exact (VAR id) | None -> assert false + +(* Steps of the procedure *) + +(* 1. A,Gamma |- A *) +let dyck_hypothesis = compose hypothesis in_some + +(* 2. False,Gamma |- G *) +let dyck_absurdity_elim = contradiction_on_hyp + +(*3. A,B,Gamma |- G + --------------- + A/\B,Gamma |- G + *) +let dyck_and_elim = compose (classically dAnd) in_some + +(*4. Gamma |- A Gamma |- B + ----------------------- + Gamma |- A /\ B + *) +let dyck_and_intro = (dAnd None) + + +(*5. A,Gamma |- G B,Gamma|- G + --------------------------- + A\/B,Gamma |- G + *) + +let dyck_or_elim = compose (classically (dorE false)) in_some + +(*6. Gamma |- A + ---------- + Gamma |- A\/B + *) +let dyck_or_introleft = (dorE false) + + +(*7. Gamma |-B + --------- + Gamma |- A\/B + *) +let dyck_or_introright = (dorE true) + + +(*8. A,Gamma |- B + -------------- + Gamma |- A -> B + *) +let dyck_imply_intro = (dImp None) + + +(*9. + B,A,Gamma |- G + -------------- + A->B,A,Gamma |- G (A Atomique) + *) +let atomic_imply_bot_pattern = put_pat mmk "?1->?2" + +let atomic_imply_step cls gls = + let mvb = somatch (clause_type cls gls) atomic_imply_bot_pattern in + if not (is_atomic (List.assoc 1 mvb)) then + error "atomic_imply_step"; + (tclTHENS (dImp cls) ([clear_clause cls;assumption])) gls + +let dyck_atomic_imply_elim = compose (atomic_imply_step) in_some + +(*10. + C ->(D-> B),Gamma |- G + ----------------------- + (C/\D)->B,Gamma |- G + *) + +let and_imply_step cls gls = + let mvb = somatch (clause_type cls gls) imply_pattern in + let a = List.assoc 1 mvb + and b = List.assoc 2 mvb in + let l = match match_with_conjunction a with + | Some (_,l) -> l + | None -> error "and_imply_step" + in + (tclTHENS (cut_intro (List.fold_right mkIMP l b)) + [clear_clause cls ; + (tclTHENS (tclTHEN (tclDO (List.length l) intro) (dImp cls)) + [assumption; + (tclTHEN (dAnd None) assumption)])]) gls + +let dyck_and_imply_elim = compose (and_imply_step) in_some + +(*11. + C->B,D->B,Gamma |-G + -------------------- + (C\/D)->B,Gamma |- G +*) + +let or_imply_step cls gls = + let mvb = somatch (clause_type cls gls) imply_pattern in + let a = List.assoc 1 mvb + and b = List.assoc 2 mvb in + let l = match match_with_disjunction a with + | Some (_,l) -> l + | None -> error "and_imply_step" + in + (tclTHENS (cut_in_parallel (List.map (fun x -> (mkIMP x b)) l)) + (clear_clause cls:: + (List.map + (fun i -> (tclTHENS (tclTHEN intro (dImp cls)) + [assumption ; + (tclTHEN (one_constructor i []) assumption)])) + (interval 1 (List.length l))))) gls + +let dyck_or_imply_elim = compose (or_imply_step) in_some + +(*12. +B,Gamma|- G D->B,Gamma |- C->D +---------------------------------- +(C->D)->B,Gamma |- G +*) + +let back_thru_2 id = + applist(VAR id,[DOP0(Meta(new_meta()));DOP0(Meta(new_meta()))]) + +let back_thru_1 id = + applist(VAR id,[DOP0(Meta(new_meta()))]) + +let exact_last_hyp = onLastHyp (fun h -> exact (VAR (out_some h))) + +let imply_imply_bot_pattern = put_pat mmk "(?1->?2)->?3" + +let imply_imply_step cls gls = + let h0 = out_some cls in (* (C->D)->B *) + let mvb = somatch (clause_type cls gls) imply_imply_bot_pattern in + let c = List.assoc 1 mvb + and d = List.assoc 2 mvb + and b = List.assoc 3 mvb + in + tclTHENS (cut_intro b) + [clear_clause cls; (* B |- G *) + tclTHENS (cut_intro (mkIMP (mkIMP d b) (mkIMP c d))) + [onLastHyp + (fun h1opt (*(D->B)->(C->D)*) -> + let h1 = out_some h1opt in + (tclTHENS (refine (back_thru_1 h0)) + [tclTHENS (tclTHEN intro (* C *) (refine (back_thru_2 h1))) + [tclTHENS (tclTHEN intro (* D *) (refine (back_thru_1 h0))) + [tclTHEN intro (* C *) assumption]; + exact_last_hyp]])); + (tclTHEN (clear_clause cls) (intro)) + ] + ] gls + +let dyck_imply_imply_elim = compose (imply_imply_step) in_some + +(*14. + B,Gamma |-G + -------------------- + True->B,Gamma |- G +*) + +let true_imply_step cls gls = + let mvb = somatch (clause_type cls gls) imply_pattern in + let a = List.assoc 1 mvb + and b = List.assoc 2 mvb in + let l = match match_with_unit_type a with + (* match_with_unit_type retournait un constr list option avec un seul + element dans la liste; maintenant il renvoie un constr option *) + (* Some (_::l) -> l *) + | Some _ -> [] + | None -> error "true_imply_step" + in + let h0 = out_some cls in + (tclTHENS (cut_intro b) + [(clear_clause cls); + (tclTHEN (apply(VAR h0)) (one_constructor 1 []))]) gls + +let dyck_true_imply_elim = compose (true_imply_step) in_some + +(* Chet's original algorithm +let rec prove g = + tclCOMPLETE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tclORELSE + ((tryAllHyps (clauseTacThen ((comp(dyck_hypothesis) (out_some))) prove))) + ((tryAllHyps (clauseTacThen ((comp(dyck_absurdity_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_and_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_or_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_atomic_imply_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_and_imply_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_or_imply_elim) (out_some))) prove))))) + ((tryAllHyps (clauseTacThen ((comp(dyck_imply_imply_elim) (out_some))) prove))))) + (((tclTHEN (dyck_and_intro) (prove)))))) + (((tclTHEN (dyck_or_introleft) (prove)))))) + (((tclTHEN (dyck_or_introright) (prove)))))) + (((tclTHEN (dyck_imply_intro) (prove)))))) g + +*) + +(* Cesar's code *) + +let trans x = ([],Nametab.sp_of_id CCI (id_of_string x)) + +let flat_map f = + let rec flat_map_f = function + | [] -> [] + | x::l -> f x @ flat_map_f l + in + flat_map_f + +type formula = + | FVar of string + | FAnd of formula*formula + | FOr of formula*formula + | FImp of formula*formula + | FEqu of formula*formula + | FNot of formula + | FEq of formula*formula*formula + | FPred of constr (* Predicado proposicional *) + | FFalse + | FTrue + (* La siguiente no puede aparecer en una formula de entrada *) + (* Representa una formula atomica cuando aparece en un principal de una + regla *) + | FLis of formula list (* Lista de formulas *) + | FAto of string (* Formula atomica *) + | FLisfor of string (* Variable para una lista de formulas *) + (* En el antecedente se llama GAMA, + en el sucedente DELTA *) + +(* Terminos en calculo lambda *) +type termino = + | TVar of string + | TApl of formula*formula*termino*termino + | TFun of string*formula*termino + | TPar of formula*formula*termino*termino + | TInl of formula*formula*termino + | TInr of formula*formula*termino + | TFst of formula*formula*termino + | TSnd of formula*formula*termino + | TCase of formula list * termino list + | TZ of formula * termino + | TExi of string + | TRefl of formula * formula (*Reflexividad de la igualdad *) + | TSim of formula * formula * formula * termino + (*Simetria de la igualdad *) + | TTrue + (* Los siguientes terminos se usan solamente en las sustituciones *) + | TSum of termino*termino (* Suma de terminos *) + | TLis of termino list (* Lista de terminos *) + | TLister of string (* Variable para una lista de terminos *) + (* En el antecendete se llama Gama, + en el sucedente Delta *) + | TZero of formula (* Milagro *) + +(* Es una formula asociada con un termino del calculo lambda, o los + multiconjuntos Gama y Delta *) +type formulaT = termino*formula + +(* La primera componente es el antecedente, la segunda es sucedente *) +type sequente = formulaT list * formulaT list + +(* Substitucion de variable por una formula *) +type subsF = (string*formula) list + +(* Substitucion de variable por un lambda termino *) +type subsT = (string*termino) list + +type regla = { + tip: string; (* Tipo de la formula principal *) + heu: bool; (* Si es una regla heuristica o no *) + ant: bool; (* Si principal es antecedente o sucedente *) + pri: formulaT;(* Formula principal de la regla *) + pre: sequente list; (* Premisas de la regla *) + res: sequente;(* Restricciones para la aplicacion de una regla*) + def: subsT; (* Definicion de los terminos del lado derecho *) + sub: subsT; (* Substitucion que se aplica al lado derecho de la + conclusion para obetener el lambda termino *) + ren: string list; (* Variables que se deben renombrar *) + vardelta:bool; (* Si se usa la variable proposicional DELTA *) + ssi:bool; (* Si la regla es reversible o no *) + rendelta: string list } (* Renombramientos de delta *) + (* Note que si Res = A |- B, entonces la conclusion de la regla es + A,Gama,Pri' |- B, Pri'',Delta + Si ant = true Pri'= Pri + Si ant =false Pri''=Pri*) + +(* Substitucion Formula Termino para aplicar una regla *) +type sFT = { + sReg : regla ref; (*Apuntador a la regla *) + sFor : subsF; (*Substitucion de Formulas *) + sGam : formulaT list; (* Lista de formulas de Gamma *) + sDel : formulaT list; (* Lista de formulas de Delta *) + sRen : (string*subsT) list; (* Renombramientos de variables *) + sTer : subsT; (* Susbstitucion de terminos *) + sDef : subsT } (* Definicion de terminos *) + +type subsFT = SNil | SCons of sFT + +type reglaSub = RNil | RCons of (sFT*regla list*formulaT list*sequente) + +(* De un arbol de demostracion *) +type nodo = { + seq: sequente ref; (* Sequente que se resuelve *) + reg: regla ref; (* Regla usada para resolver *) + sd: subsT; (* Substitucion que define los lambda terminos *) + st: subsT } (* Substitucion que calcula el lambda termino *) + +(* Arbol de demostracion *) +type arbol = Nil | Cons of arbol * nodo * arbol + +(* Demostracion *) +(* Si el secuente es valido Arb es un arbol de demostracion y Lisbut + es vacio, sino Lisbut es un contexto en el cual Arb es valido *) +type demostracion = { arb : arbol; lisbut : formulaT list } + +(* Definicion de excepcion para rescribir terminos *) +exception NoAplica +exception TacticFailure + +(* ------------------ Sistema de Gentzen Intuisionista -------------------*) +(* Gama,Delta son metavariables de conjuntos de reglas + A,B son variables de formulas *) + +let gama = (TLister "Gama",FLisfor "GAMA") +let delta = (TLister "Delta",FLisfor "DELTA") +let delta' = (TLister "Delta'",FLisfor "DELTA") +let delta'' = (TLister "Delta''",FLisfor "DELTA") + +let curry(a,b,c,a_0,b_0,p) = TFun(a_0,a,TFun(b_0,b,TApl(FAnd(a,b),c,p, + TPar(a,b,TVar a_0,TVar b_0)))) +let left(a,b,c,a_0,p) = TFun(a_0,a,TApl(FOr(a,b),c,p,TInl(a,b,TVar a_0))) +let right(a,b,c,b_0,p) = TFun(b_0,b,TApl(FOr(a,b),c,p,TInr(a,b,TVar b_0))) +let imp2(a,b,c,a_0,b_0,p) = TFun(a_0,a,TApl(FImp(b,a),c,p,TFun(b_0,b,TVar a_0))) + +(* Regla inicial *) +(* / A,Gama |- A,Delta *) +let inic = { + tip="inic"; + heu=false; + ant=true; + pri= TVar "#x",FAto "#A"; + pre=[]; + res=([],[TVar "#x",FVar "#A"]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#x"]; + vardelta = true; + ssi = true; + rendelta=[] } + +(* Regla l_false *) +(* / Gama,False |- Delta *) +let l_false = { + tip="false"; + heu=false; + ant=true; + pri= TVar "#x",FFalse; + pre=[]; + res=([],[]); + def=["Delta",TZ(FLisfor "DELTA",TVar "#x")]; + sub=[]; + ren=["#x"]; + vardelta = true; + ssi = true; + rendelta=[]} + +(* Regla r_true *) +(* / Gama |- True,Delta *) +let r_true = { + tip="true"; + heu=false; + ant=false; + pri= TTrue,FTrue; + pre=[]; + res=([],[]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=[]; + vardelta = true; + ssi = true; + rendelta=[]} + +(* Regla l_and *) +(* A,B,Gama |- Delta / FAnd(A,B),Gama |- Delta *) +let l_and = { + tip="l_and"; + heu=false; + ant=true; + pri= TVar "#xy",FAnd(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#A";TVar "#y",FVar "#B";gama],[delta]]; + res=([],[]); + def=[]; + sub=["#x",TFst(FVar "#A",FVar "#B",TVar "#xy"); + "#y",TSnd(FVar "#A",FVar "#B",TVar "#xy")]; + ren=["#x";"#y"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_and *) +(* Gama |- A,Delta' Gama |- B,Delta'' / Gama |- A/\B,Delta *) +let r_and = { + tip="r_and"; + heu=false; + ant=false; + pri= TPar(FVar "#A",FVar "#B",TVar "#x",TVar "#y"), + FAnd(FVar "#A",FVar "#B"); + pre=[[gama],[TVar "#x",FVar "#A";delta'];[gama], + [TVar "#y",FVar "#B";delta'']]; + res=([],[]); + def=["Delta",TSum(TLister "Delta'",TLister "Delta''")]; + sub=[]; + ren=["#x";"#y"]; + vardelta = true; + ssi = true; + rendelta=["Delta'";"Delta''"]} + +(* Regla l_or *) +(* A,Gama |- Delta' B,Gama |- Delta'' / A\/B,Gama |- Delta *) +let l_or = { + tip="l_or"; + heu=false; + ant=true; + pri= TVar "#xy",FOr(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#A";gama],[delta']; + [TVar "#y",FVar "#B";gama],[delta'']]; + res=([],[]); + sub=[]; + def=["Delta", TCase([FVar "#A";FVar "#B";FLisfor "DELTA"], + [TFun("#x",FVar "#A",TLister "Delta'"); + TFun("#y",FVar "#B",TLister "Delta''"); + TVar "#xy"])]; + ren=["#x";"#y";"#xy"]; + vardelta = true; + ssi = true; + rendelta=["Delta'";"Delta''"]} + +(* Regla r_or *) +(* Gama |- A,B,Delta / Gama |- A\/B,Delta *) +let r_or = { + tip="r_or"; + heu=false; + ant=false; + pri= TSum(TInl(FVar "#A",FVar "#B",TVar "#x"), + TInr(FVar "#A",FVar "#B",TVar "#y")), + FOr(FVar "#A",FVar "#B"); + pre=[[gama], + [TVar "#x",FVar "#A";TVar "#y",FVar "#B";delta]]; + res=([],[]); + sub=[]; + def=[]; + ren=["#x";"#y"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp1 *) +(* A,B,Gama |- Delta / A->B,A,Gama |- Delta (A es un atomo) *) +let l_imp1 = { + tip="l_imp1"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FAto "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#B";gama], + [delta]]; + res=([TVar "#a",FVar "#A"],[]); + def=[]; + sub=["#x",TApl(FVar "#A",FVar "#B",TVar "#p",TVar "#a")]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp2 *) +(* C->(D->B),Gama |- Delta / C/\D->B,Gama |- Delta *) +let l_imp2 = { + tip="l_imp2"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FAnd(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x",FImp(FVar "#C",FImp(FVar "#D",FVar "#B"));gama], + [delta]]; + res=([],[]); + def=[]; + sub=["#x",curry(FVar "#C",FVar "#D",FVar "#B","#c","#d",TVar "#p")]; + ren=["#x";"#c";"#d"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp3 *) +(* C->B,D->B,Gama |- Delta / C\/D->B,Gama |- Delta *) +let l_imp3 = { + tip="l_imp3"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FOr(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x",FImp(FVar "#C",FVar "#B");TVar "#y", + FImp(FVar "#D",FVar "#B");gama], + [delta]]; + res=([],[]); + def=[]; + sub=["#x",left(FVar "#C",FVar "#D",FVar "#B","#c",TVar "#p"); + "#y",right(FVar "#C",FVar "#D",FVar "#B","#d",TVar "#p")]; + ren=["#x";"#y";"#c";"#d"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp4 *) +(* D->B,Gama |- C->D,Delta B,Gama |- Delta / (C->D)->B,Gama |- Delta *) +let l_imp4 = { + tip="l_imp4"; + heu=false; + ant=true; + pri= TVar "#p",FImp(FImp(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x",FVar "#B";gama],[delta]; + [TVar "#z",FImp(FVar "#D",FVar "#B");gama],[TVar "#y", + FImp(FVar "#C",FVar "#D")]]; + res=([],[]); + def=[]; + sub=["#x", + TApl(FImp(FVar "#C",FVar "#D"),FVar "#B",TVar "#p", + TApl(FVar "#D",FVar "#B", + TFun("#z",FImp(FVar "#D",FVar "#B"),TVar "#y"), + imp2(FVar "#D",FVar "#C",FVar "#B","#d","#c",TVar "#p")))]; + ren=["#x";"#y";"#z";"#d";"#c"]; + vardelta = false; + ssi = false; + rendelta=[]} + +(* Regla l_imp5 *) +(* (A->False)->B,Gama |- Delta / Not(A)->B,Gama |- Delta *) +let l_imp5 = { + tip="l_imp5"; + heu=false; + ant=true; + pri= TVar "#x",FImp(FNot(FVar "#A"),FVar "#B"); + pre=[[TVar "#x",FImp(FImp(FVar "#A",FFalse),FVar "#B");gama], + [delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp6 *) +(* (C->D/\D->C)->B,Gama |- Delta / (C<->D)->B,Gama |- Delta *) +let l_imp6 = { + tip="l_imp6"; + heu=false; + ant=true; + pri= TVar "#x",FImp(FEqu(FVar "#C",FVar "#D"),FVar "#B"); + pre=[[TVar "#x", + FImp(FAnd(FImp(FVar "#C",FVar "#D"), + FImp(FVar "#D",FVar "#C")),FVar "#B");gama],[delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_imp7 *) +(* B,Gama |- Delta / True->B,Gama |- Delta *) +let l_imp7 = { + tip="l_imp7"; + heu=false; + ant=true; + pri= TVar "#t",FImp(FTrue,FVar "#B"); + pre=[[TVar "#x",FVar "#B";gama],[delta]]; + res=([],[]); + def=[]; + sub=["#x",TApl(FTrue,FVar "#B",TVar "#t",TTrue)]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_imp *) +(* A,Gama |- B / Gama |- A->B,Delta *) +let r_imp = { + tip="r_imp"; + heu=false; + ant=false; + pri= TFun("#x",FVar "#A",TVar "#y"),FImp(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FVar "#A";gama],[TVar "#y",FVar "#B"]]; + res=([],[]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#x";"#y"]; + vardelta = true; + ssi = false; + rendelta=[]} + +(* Regla l_not *) +(* A->False,Gama |- Delta / Not(A),Gama |- Delta *) +let l_not = { + tip="l_not"; + heu=false; + ant=true; + pri= TVar "#x",FNot(FVar "#A"); + pre=[[TVar "#x",FImp(FVar "#A",FFalse);gama],[delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_not *) +(* Gama |- A->False,Delta / Gama |- Not(A),Delta *) +let r_not = { + tip="r_not"; + heu=false; + ant=false; + pri= TVar "#x",FNot(FVar "#A"); + pre=[[gama],[TVar "#x",FImp(FVar "#A",FFalse);delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla l_equ *) +(* A->B/\B->A,Gama |- Delta / A<->B,Gama |- Delta *) +let l_equ = { + tip="l_equ"; + heu=false; + ant=true; + pri= TVar "#x",FEqu(FVar "#A",FVar "#B"); + pre=[[TVar "#x",FAnd(FImp(FVar "#A",FVar "#B"), + FImp(FVar "#B",FVar "#A"));gama],[delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Regla r_equ *) +(* Gama |- A->B/\B->A,Delta / Gama |- A<->B,Delta *) +let r_equ = { + tip="r_equ"; + heu=false; + ant=false; + pri= TVar "#x",FEqu(FVar "#A",FVar "#B"); + pre=[[gama], + [TVar "#x",FAnd(FImp(FVar "#A",FVar "#B"), + FImp(FVar "#B",FVar "#A"));delta]]; + res=([],[]); + def=[]; + sub=[]; + ren=["#x"]; + vardelta = false; + ssi = true; + rendelta=[]} + +(* Definicion de la regla VACIA *) +let vACIA = { + tip="vacia"; + heu=false; + ant=false; + pri=gama; + pre=[]; + res=([],[]); + def=[]; + sub=[]; + ren=[]; + vardelta = false; + ssi = false; + rendelta=[]} + +(*---------------------- Reglas heuristicas ------------------------------*) + +(* Regla simetria de igualdad *) +(* / a=b,Gama |- b=a,Delta *) +let sim = { + tip="sim"; + heu=true; + ant=true; + pri= TVar "#x",FEq(FVar "#A",FVar "#a",FVar "#b"); + pre=[]; + res=([],[TSim(FVar "#A",FVar "#a",FVar"#b",TVar"#x"), + FEq(FVar "#A",FVar "#b",FVar "#a")]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#x";"#a";"#b"]; + vardelta = true; + ssi = true; + rendelta=[]} + +(* Regla r_refl *) +(* / Gama |- <t>a=a,Delta *) +let r_refl = { + tip="refl"; + heu=true; + ant=false; + pri= TRefl(FVar "#A",FVar "#a"),FEq(FVar "#A",FVar "#a",FVar "#a"); + pre=[]; + res=([],[]); + def=["Delta",TZero(FLisfor "DELTA")]; + sub=[]; + ren=["#a"]; + vardelta = true; + ssi = true; + rendelta=[]} + +let sistema = [inic;l_false;r_true;l_and;r_and;l_imp1;l_imp2;l_imp3; + l_imp5;l_imp6;l_imp7;l_not;r_not;l_equ;r_equ;r_imp; + l_or;r_or;l_imp4] + +(*----------- Proyecciones del tipos de datos Sequente ----------------------*) + +(* Antecedente de un sequente *) +let ante (a,_) = a + +(* Sucedente de un sequente *) +let suce (_,s) = s + +(*----------- Constructores de los tipos de datos ----------------------*) + +(* Simplifica una substitucion es decir elemina las substituciones + inutiles *) +let rec simple = function + | [] -> [] + | ((x,_) as a)::z -> + if String.get x 0 = '#' then simple z else a::simple z + +(* Construye un node de demostracion *) +let consd a l = {arb=a;lisbut=l} + +(* Construye un nodo de un arbol *) +let consa s r sd st = {seq = ref s;reg = ref r;sd = simple sd; + st= simple st} + +(* Construye un nodo de sustitucion *) +let conss r sf sg sd ren sdef ster = + SCons({sReg=ref r;sFor=sf;sGam=sg;sDel=sd; + sRen=ren;sDef=sdef;sTer=ster}) + +(*----------------------- Aplicacion de Reglas ------------------------------*) + +(* Buscar un nombre de variable en una sustitucion, retorna la lista + que contiene la formula que la variable sustituye *) +let rec busque n = function + | [] -> [] + | (x,f)::y -> if x=n then [f] else busque n y + +(* Aplicar una substitucion a una formula, retorna otra formula *) +let rec apl_f s = function + | (FVar y) as x -> (match busque y s with + | [] -> x + | a::_ -> a ) + | (FLisfor y) as x -> (match busque y s with + | [] -> x + | a::_ -> a) + | FAnd (a,b) -> FAnd(apl_f s a, apl_f s b) + | FOr (a,b) -> FOr(apl_f s a, apl_f s b) + | FImp (a,b) -> FImp(apl_f s a, apl_f s b) + | FEqu (a,b) -> FEqu(apl_f s a, apl_f s b) + | FEq (a,b,c) -> FEq(apl_f s a, apl_f s b,apl_f s c) + | FNot a -> FNot(apl_f s a) + | x -> x + +(* Aplicar una sustitucion a una lista de formulas *) +let apl_lf s l = List.map (apl_f s) l + +(* Encuentra un unificador de primer orden de dos formulas proposicionales, + retorna la pareja (e,u), donde e indica exito o fracaso + y u es el unificador principal (si no existe es [] vacia ) *) +let rec unif_f = function + | FAnd(a,b),FAnd(x,y) -> unif_lf([a;b],[x;y]) + | FOr(a,b),FOr(x,y) -> unif_lf([a;b],[x;y]) + | FImp(a,b),FImp(x,y) -> unif_lf([a;b],[x;y]) + | FEqu(a,b),FEqu(x,y) -> unif_lf([a;b],[x;y]) + | FEq(a,b,c),FEq(x,y,z) -> unif_lf([a;b;c],[x;y;z]) + | FVar(a),x -> (true,[a,x]) + | FAto(a),(FPred(_) as x) -> (true,[a,x]) + | FAto(a),(FEq(_) as x) -> (true,[a,x]) + | FPred(a),FPred(x) -> (eq_constr a x,[]) + | FNot(a),FNot(x) -> unif_f(a,x) + | FFalse,FFalse -> (true,[]) + | FTrue,FTrue -> (true,[]) + | _ -> (false,[]) + +and unif_lf = function + | ([],[]) -> (true,[]) + | (x::y,a::b) -> + let (e,u) = unif_f (x,a) in + if e then + let (e1,u1) = unif_lf (apl_lf u y,b) in + if e1 then (true,u@u1) else (false,[]) + else + (false,[]) + | _ -> (false,[]) + +(* Aplicar una substitucion a un lamda termino, retorna otro lambda termino *) +let rec apl_t st sf = function + | (TVar y) as x -> (match busque y st with + | [] -> x + | a::_ -> a ) + | (TLister y) as x -> (match busque y st with + | [] -> x + | a::_ -> a ) + | TApl(f1,f2,t1,t2) -> TApl (apl_f sf f1,apl_f sf f2, + apl_t st sf t1,apl_t st sf t2) + | TFun(x,f,y) -> (match busque x st with + | [] -> TFun(x,apl_f sf f,apl_t st sf y) + | [TVar n] -> TFun(n,apl_f sf f,apl_t st sf y) + | _ -> raise TacticFailure) + | TCase(lf,lt) -> TCase(List.map (apl_f sf) lf,List.map (apl_t st sf) lt) + | TPar(f1,f2,t1,t2) -> TPar(apl_f sf f1,apl_f sf f2, + apl_t st sf t1,apl_t st sf t2) + | TInl(f1,f2,t) -> TInl(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TInr(f1,f2,t) -> TInr(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TFst(f1,f2,t) -> TFst(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TSnd(f1,f2,t) -> TSnd(apl_f sf f1,apl_f sf f2,apl_t st sf t) + | TRefl(f1,f2) -> TRefl(apl_f sf f1,apl_f sf f2) + | TSim(f1,f2,f3,t) -> TSim(apl_f sf f1,apl_f sf f2, + apl_f sf f3,apl_t st sf t) + | TLis lt -> TLis (List.map (apl_t st sf) lt) + | TSum(t1,t2) -> TSum (apl_t st sf t1,apl_t st sf t2) + | TZ(f,t) -> TZ(apl_f sf f,apl_t st sf t) + | (TExi y) as x -> (match busque y st with + | [] -> x + | a::_ -> a ) + | TZero f -> TZero(apl_f sf f) + | t -> t + +(* Aplicar substitucion gama delta y una substitucion de terminos lambda + a una lista de formulasT, retorna una lista de formulasT *) +let rec apl_lft (s,gama_0,delta_0) st rendelta = + (* Aplicar una substitucion gama delta y una substitucion de terminos a una + formulaT, retorna una lista de formulasT *) + let apl_fm = function + | (_,FLisfor "GAMA") -> gama_0 + | (TLister x,FLisfor "DELTA") -> + (match busque x rendelta with + | [] -> delta_0 + | a::_ -> apl_lft ([],[],[]) a [] delta_0) + | (_,FLisfor "DELTA") -> delta_0 + | (t,f) -> [apl_t st [] t,apl_f s f] + in + flat_map apl_fm + +(* Aplicar substitucion gama delta y una substitucion de terminos lambda a un + sequente, retorna un nuevo sequente*) +let apl sf st rendelta = function + (l1,l2) -> (apl_lft sf st rendelta l1,apl_lft sf st rendelta l2) + +(* Aplicar la regla r, dada una substitucion. + Retorna una lista de sequentes *) +let aplr_s subs = List.map (apl (subs.sFor,subs.sGam,subs.sDel) + subs.sDef subs.sRen) !(subs.sReg).pre + +(* Componer dos substituciones de lambda terminos. Aplica la primera + sobre la segunda *) +let rec comp_st st = function + | [] -> st + | (x,y)::z -> (x,apl_t st [] y)::comp_st st z + +(* Renombrar las variables izquierdas de una sustitucion *) +let rec ren_izq ren = function + | [] -> [] + | ((x,y) as a)::z -> match busque x ren with + | [TVar a] -> (a,y)::ren_izq ren z + | _ -> a::ren_izq ren z + +(* Indica si dos formulas son iguales *) +let iguales_f f1 f2 = + let (e,u) = unif_f(f1,f2) in + e & u = [] + +(*------------------- Unificador para lambda terminos --------------------*) + +(* Encuentra un unificador de primer orden de dos lambda terminos, + retorna la pareja (e,u), donde e indica exito o fracaso + y u es el unificador principal (si no existe es [] vacia ). + TPara los terminos que contienen formulas recibe el unificador de + ellas *) +let rec unif_t sf = function + | (TVar x,((TVar y) as y_0)) -> + if (x = y) then (true,[]) else (true,[x,apl_t [] sf y_0]) + | (TVar x, y) -> (true,[x,apl_t [] sf y]) + | TApl(f,ff,t,tt),TApl(f1,ff1,t1,tt1) -> + unif_lft sf [f;ff][f1;ff1][t;tt][t1;tt1] + | TZ(f,t), TZ(f1,t1) -> unif_lft sf [f][f1][t][t1] + | (TExi x,((TExi y) as y_0)) -> + if (x = y) then (true,[]) else (true,[x,apl_t [] sf y_0]) + | TZero f, TZero f1 -> unif_lft sf [f][f1][][] + | TTrue,TTrue -> (true,[]) + | TFun(x,f,t),TFun(a,f1,t1) -> unif_lft sf [f][f1][t][t1] + | TPar(f,ff,t,tt),TPar(f1,ff1,t1,tt1) -> + unif_lft sf [f;ff][f1;ff1] [t;tt][t1;tt1] + | TInl(f,ff,t),TInl(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TInr(f,ff,t),TInr(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TFst(f,ff,t),TFst(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TSnd(f,ff,t),TSnd(f1,ff1,t1) -> unif_lft sf [f;ff][f1;ff1][t][t1] + | TRefl(f,ff),TRefl(f1,ff1) -> unif_lft sf [f;ff][f1;ff1][][] + | TSim(f1,f2,f3,t),TSim(f1',f2',f3',t') -> + unif_lft sf [f1;f2;f3] [f1';f2';f3'][t][t'] + | _ -> (false,[]) + +and iguales_lf sf = function + | ([],[]) -> true + | (x::y,a::b) -> + if iguales_f (apl_f sf x) (apl_f sf a) then + iguales_lf sf (y,b) + else + false + | _ -> false + +and unif_lt sf = function + | ([],[]) -> (true,[]) + | (x::y,a::b) -> + let (e,u) = unif_t sf (x,a) in + if e then + let (e1,u1) = unif_lt sf (y,b) in + if e1 then (true,u@u1) + else (false,[]) + else + (false,[]) + | _ -> (false,[]) + +and unif_lft sf lf lf1 lt lt1 = + if iguales_lf sf (lf,lf1) then + unif_lt sf (lt,lt1) + else + (false,[]) + +(* Indica si dos terminos son iguales *) +let iguales_t t1 t2 = + let (e,u) = unif_t [] (t1,t2) in + e & u = [] + +(* Indica si dos formulas son iguales. Retorna una pareja con el exito + y un unificador de los dos lambda terminos *) +let iguales_unif uf tr ts fr fs = + if iguales_f fr fs then + let (e,ut) = unif_t uf (ts,tr) in + if e then + (true,ut) + else + raise TacticFailure + else + (false,[]) + +(* Crear una nueva variable *) +let hipvar = ref ((id_of_string "#")::[]) + +let genvar () = + let id = next_ident_away + (id_of_string "H") + !hipvar in + (hipvar := id::(!hipvar); string_of_id id) + +(* Lista de terminos de una substitucion *) +let listerm = List.map snd + +(* Lista de variables de una lista de formulasS *) +let rec lisvar = function + | [] -> [] + | (TVar x,_)::y -> x::lisvar y + | (TExi x,_)::y -> x::lisvar y + | _::y -> lisvar y + +(* Lista de formulas de una lista de formulasS *) +let rec lisfor = function + | [] -> [] + | (TVar _,x)::y -> x::lisfor y + | (TExi _,x)::y -> x::lisfor y + | _::y -> lisfor y + +(* Recibe una lista de variables, retorna un renombramiento de ellas *) +let renombra = List.map (function x -> (x,TVar(genvar()))) + +(* Obtiene un renombramiento de todas las metavariables delta *) +let renombradelta s rend= + let l = lisvar (suce s) in + List.map (function x -> (x,renombra l)) rend + +(* Obtiene una substitucion de las metavariables delta, por lista de + terminos *) +let rec subsdelta = function + | [] -> [] + | (x,y)::y_0 -> match listerm y with + | [] -> [] + | [a] -> (x,a)::subsdelta y_0 + | a -> (x,TLis a)::subsdelta y_0 + +(* Indica si una formula pertenece a una lista de formulasT. + Retorna una pareja con el exito y una unificacion de los lambda terminos *) +let rec pertenece uf ant tr fr = function + | [] -> (false,[]) + | (TLister _,_)::y -> pertenece uf ant tr fr y + | (ts,fs)::y -> + let (e,ut) = + if ant then + iguales_unif uf ts tr fr fs + else + iguales_unif uf tr ts fr fs + in + if e then + (true,ut) + else + pertenece uf ant tr fr y + +(* Indica si la primera lista de formulasT contiene la segunda. + Retorna una pareja con el exito y una unificacion de los lambda terminos *) +let rec contiene uf ant l = function + | [] -> (true,[]) + | (TLister _,_)::y -> contiene uf ant l y + | (tr,fr)::y -> + let (e1,s1) = pertenece uf ant tr fr l in + if e1 then + let (e2,s2) = contiene uf ant l y in + if e2 then + (true,s1@s2) + else + (false,[]) + else + (false,[]) + +(* Decide si un secuente cumple con las restricciones de aplicacion de una + regla. Recibe el unificador de la regla con la restriccion. Retorna una + pareja con el exito y las unificaciones de lambda terminos del antecedente + y el sucedente del secuente *) +let cumple uf res = function (seql,seqr) -> + let (resl,resr) = apl (uf,[],[]) [] [] res in + let (e1,s1) = contiene uf true seql resl in + if e1 then + let (e2,s2) = contiene uf false seqr resr in + if e2 then + (true,s1,s2) + else + (false,[],[]) + else + (false,[],[]) + +(* Compone una substitucion de formulas con una substitucion de terminos *) +let rec comp_sfst uf = function + | [] -> [] + | (x,y)::z -> (x,apl_t [] uf y)::comp_sfst uf z + +(* Crea una substitucion para las variables de un lambda termino, basado + en la regla que aplica *) +let cree_sub s uf ter t ul ur r = + let lv = + if r.vardelta then ["DELTA",FLis(lisfor (suce s))] else [] + in + let rendelta = renombradelta s r.rendelta in + let ren = (renombra r.ren) @ (subsdelta rendelta) in + let sd0 = + if r.ant then + ur (* Calcular definicion basica *) + else + match unif_t uf (t,ter) with + | (false,_) -> raise(TacticFailure) + | (_,u) -> ur@u + in + let sd1 = comp_st r.def sd0 in + let sd2 = comp_sfst (uf@lv) sd1 in (*Susbstituir var. proposicionales *) + let sd = comp_st ren sd2 in (* Componer con un renombramiento *) + let st0 = + if r.ant then (* Calcular sustitucion basica *) + match unif_t uf (ter,t) with + | (false,_) -> raise(TacticFailure) + | (_,u) -> ul@u + else + ul + in + let st1 = comp_st st0 r.sub in + let st2 = comp_sfst (uf@lv) st1 in (*Susbstituir var. proposicionales *) + let st3 = ren_izq ren st2 in (* Componer con un renombramiento *) + let st = comp_st ren st3 in + (sd,st,rendelta) + +(* Decide se una regla dada es aplicable sobre un termino (tf) + de un secuente y un lado de reduccion o. Retorna la sustitucion + apropiada para la regla o SNil si no existe *) + +let rec aplicable s lf tf o = function + ({ant=ant;pri=ter,pri;res=res}) as r -> + if o<>ant then + SNil + else + (match tf with + | (TLister _,_) -> SNil + | (t,f) -> + let (ef,uf) = unif_f(pri,f) in + if ef then + let (et,ul,ur) = cumple uf res s in + if et then + let (gam,del) = if ant then (lf,suce s) + else (ante s,lf) in + let (sd,st,rn) = cree_sub s uf ter t ul ur r in + conss r uf gam del rn sd st + else SNil + else SNil) + +(* Dado una regla, retorna una posicion donde la regla sea aplicable. RNil + si no existe *) +let rec escoja_termino r s o rseq lacum = function + | [] -> + if o=0 then + escoja_termino r s 2 [] lacum rseq + else if o=1 then + escoja_termino r s 2 [] [] rseq + else + RNil + | t::y -> + let oo = if o=0 then 1 else o in + (match aplicable s (lacum@y) t (oo=1) r with + | SNil -> escoja_termino r s oo rseq (lacum@[t]) y + | SCons(s) -> + if oo=1 then RCons(s,[],lacum,(y,rseq)) + else RCons(s,[],lacum,([],y))) + +(* Dado un secuente y un sistema de reglas + retorna una sustitucion apropiada para la regla, o RNil si no existe *) +let rec escoja_regla s (lrseq,lac) = function + | [] -> RNil + | (r::y) as lreg -> + (match escoja_termino r s 0 (suce lrseq) lac (ante lrseq) with + | RNil -> escoja_regla s (s,[]) y + | RCons(subs,_,lanew,lrnew) -> RCons(subs,lreg,lanew,lrnew)) + +(* Si una formula proposicional existe en una lista de formulas *) +let rec existeprop f = function + | [] -> false + | x::y -> if iguales_f f x then true else existeprop f y + +(* Buscar una formula proposicional en una lista de formulasT, + retorna el termino o TZero si no la encuentra *) +let rec busqueprop f = function + | [] -> TZero(FFalse) + | (tt,ff)::y -> if iguales_f f ff then tt else busqueprop f y + +(* Crear un termino como aplicaciones sucesivas del subobjetivo sobre las + hipotesis *) +let rec ter_subobjetivo lisprop subobj = function + | [] -> (fst subobj) + | (x,f)::y -> + if existeprop f lisprop then + ter_subobjetivo lisprop subobj y + else + (match snd(subobj) with + | FImp(a,b) -> ter_subobjetivo (f::lisprop) + (TApl(a,b,fst(subobj),x),b) y + | _ -> TZero(FFalse)) + +(* Convierte la lista del succedente en una disyuncion *) +let rec disyuncion = function + | [] -> FFalse + | [a] -> a + | x::y -> FOr(x,disyuncion y) + +(* Convierte la lista del antecedente en una implicacion *) +let rec implicacion dis vp = function + | [] -> dis + | x::y -> + if (existeprop x vp) then + implicacion dis vp y + else + FImp(x,implicacion dis vp y) + +(* Lista de proposiciones de un secuente sin repetidos *) +let rec it_propos lisacum = function + | [] -> lisacum + | (_,f)::y -> + if (existeprop f lisacum) then + it_propos lisacum y + else + it_propos (lisacum@[f]) y + +let proposiciones = it_propos [] + +(* Generar una subobjetivo de la demostracion de tal manera que + la validez del sequente original sea equivalente a la validez del + subobjetivo *) +let subobjetivo s vp = + let dis = disyuncion (proposiciones (suce s)) in + let ter = TExi(genvar()) in + (ter,implicacion dis vp (proposiciones (ante s))),dis + +(* Crea una substitucion que supone un subobjetivo demostrado *) +let rec termino_caso fapp f = function + | FOr(a,b) -> + let id1 = genvar() in + let t1 = TVar(id1) in + let id2 = genvar() in + let t2 = TVar(id2) in + if iguales_f a f then + TCase([a;b;f],[TFun(id1,a,t1);TFun(id2,b,TZero(f));fapp]) + else + TCase([a;b;f],[TFun(id1,a,TZero(f));TFun(id2,b,termino_caso t2 f b); + fapp]) + | _ -> fapp + +let rec it_subs_subobj subs sec fapp tip = function + | [] -> subs + | ((TVar x,f) as a)::y -> + let t = busqueprop f sec in + if t <> TZero(FFalse) then + it_subs_subobj ((x,apl_t subs [] t)::subs) sec fapp tip y + else + it_subs_subobj ((x,termino_caso fapp f tip)::subs) (a::sec) + fapp tip y + | _ -> assert false + +let subs_subobj fapp tip s = it_subs_subobj [] [] fapp tip s + +let rec esta_en_case l = function + | TApl(_,_,t1,t2) -> + (esta_en_case l t1) or (esta_en_case l t2) + | TFun(_,_,t) -> + esta_en_case l t + | TPar(_,_,t1,t2) -> + (esta_en_case l t1) or (esta_en_case l t2) + | TInl(_,_,t) -> + esta_en_case l t + | TInr(_,_,t) -> + esta_en_case l t + | TFst(_,_,t) -> + esta_en_case l t + | TSnd(_,_,t) -> + esta_en_case l t + | TZ(_,t) -> + esta_en_case l t + | TSum(t1,t2) -> + (esta_en_case l t1) or (esta_en_case l t2) + | TCase([f1;f2;f3],[t1;t2;t3]) -> + (match l with + | [ff1;ff2;ff3] -> + if (iguales_f f1 ff1) & (iguales_f f2 ff2) & + (iguales_f f3 ff3) then + true + else + (esta_en_case l t1) or (esta_en_case l t2) + | _ -> assert false) + | _ -> false + +let rec busque_termino t = function + | [] -> (false,"",false) + | (x,v,o)::y -> if iguales_t t x then (true,v,o) else busque_termino t y + +(* Sistema de reglas para simplificar terminos *) +let rec sistreg lcase = function + | TApl(_,_,TFun (x,_,t),t1) -> apl_t [x,t1] [] t + | TFst(_,_,TPar(_,_,t,_)) -> t + | TSnd(_,_,TPar(_,_,_,t)) -> t + (* Simplificacion con TZero *) + | TApl(_,f,TZero _,t) -> TZero f + | TApl(_,f,t,TZero _) -> TZero f + | TFun(x,f1,TZero f2) -> TZero (FImp(f1,f2)) + | TPar(f1,f2,TZero _,t2) -> TZero (FAnd(f1,f2)) + | TPar(f1,f2,t1,TZero _) -> TZero (FAnd(f1,f2)) + | TInl(f1,f2,TZero _) -> TZero (FOr(f1,f2)) + | TInr(f1,f2,TZero _) -> TZero (FOr(f1,f2)) + | TFst(f1,f2,TZero _) -> TZero f1 + | TSnd(f1,f2,TZero _) -> TZero f2 + | TZ(f,TZero _) -> TZero f + | TSum(TZero _,t) -> t + | TSum(t,TZero _) -> t + | TCase([_;_;f],[_;_;TZero _]) -> TZero f + | TSum(TFun(v1,ff1,t1),TFun(v2,ff2,t2)) -> + TFun(v1,ff1,TSum(t1,apl_t [v2,(TVar v1)][] t2)) + (* Simplificacion del case *) + | TApl(f1,f2,TCase([a;b;FImp(c,d)],[TFun(v1,ff1,t1); + TFun(v2,ff2,t2);t3]),t) -> + TCase([a;b;f2],[TFun(v1,ff1,TApl(c,d,t1,t)); + TFun(v2,ff2,TApl(c,d,t2,t));t3]) + | TApl(f1,f2,t,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f2],[TFun(v1,ff1,TApl(f1,f2,t,t1)); + TFun(v2,ff2,TApl(f1,f2,t,t2));t3]) + | TPar(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3]),t) -> + TCase([a;b;FAnd(f1,f2)],[TFun(v1,ff1,TPar(f1,f2,t1,t)); + TFun(v2,ff2,TPar(f1,f2,t2,t));t3]) + | TPar(f1,f2,t,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;FAnd(f1,f2)],[TFun(v1,ff1,TPar(f1,f2,t,t1)); + TFun(v2,ff2,TPar(f1,f2,t,t2));t3]) + | TInl(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;FOr(f1,f2)],[TFun(v1,ff1,TInl(f1,f2,t1)); + TFun(v2,ff2,TInl(f1,f2,t2));t3]) + | TInr(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;FOr(f1,f2)],[TFun(v1,ff1,TInr(f1,f2,t1)); + TFun(v2,ff2,TInr(f1,f2,t2));t3]) + | TFst(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f1],[TFun(v1,ff1,TFst(f1,f2,t1)); + TFun(v2,ff2,TFst(f1,f2,t2));t3]) + | TSnd(f1,f2,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f2],[TFun(v1,ff1,TSnd(f1,f2,t1)); + TFun(v2,ff2,TSnd(f1,f2,t2));t3]) + | TZ(f,TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3])) -> + TCase([a;b;f],[TFun(v1,ff1,TZ(f,t1)); + TFun(v2,ff2,TZ(f,t2));t3]) + | TSum((TCase([a;b;c],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3]) as tC1), + (TCase([a';b';c'], + [TFun(v1',ff1',t1');TFun(v2',ff2',t2');t3']) as tC2)) -> + if (iguales_f a a') & (iguales_f b b') then + TCase([a;b;c],[TFun(v1,ff1,TSum(t1,apl_t [v1',(TVar v1)] [] t1')); + TFun(v2,ff2,TSum(t2,apl_t [v2',(TVar v2)] [] t2')); + TSum(t3,t3')]) + else if (esta_en_case [a;b;c] t1') or (esta_en_case [a;b;c] t2') then + TCase([a';b';c'],[TFun(v1',ff1',TSum(t1',tC1)); + TFun(v2',ff2',TSum(t2',tC1));t3']) + else + TCase([a;b;c],[TFun(v1,ff1,TSum(t1,tC2));TFun(v2,ff2,TSum(t2,tC2));t3]) + | TCase([_;_;f],[TFun(_,_,TZero _);TFun(_,_,TZero _);_]) -> TZero(f) + | TCase([a;b;f],[TFun(v1,f1,t1) as tt1;TFun(v2,f2,t2) as tt2;t]) -> + if iguales_t t1 t2 then t2 + else + let (exi,var,ori) = busque_termino t lcase in + if exi then + if ori then apl_t [v1,TVar var][] t1 + else apl_t [v1, TVar var] [] t2 + else raise(NoAplica) + | TSum(t1,t2)-> + if (iguales_t t1 t2) then t1 + else raise (NoAplica) + | TPar(_,_,TFst(_,_,t1),TSnd(_,_,t2)) -> + if iguales_t t1 t2 then + t1 + else raise(NoAplica) + | _ -> raise(NoAplica) + +(* Aplicacion de una regla sobre un termino, si no pudo aplicar retorna + NoAplica. Estrategia mas izquierdo, menos profundo *) + +let pr l = List.hd l + +let sn l = List.hd(List.tl l) + +let rec it_apl_listsistr lcase lacum siapl = function + | [] -> (lacum,siapl) + | x::y -> + let (xp,exi) = + try (apl_sistr lcase x,true) with NoAplica -> (x,false) + in + it_apl_listsistr lcase (lacum@[xp]) (exi or siapl) y + +and apl_listsistr lcase l = it_apl_listsistr lcase [] false l + +and apl_sistr_try lcase x = + try (apl_sistr lcase x,true) with NoAplica -> (x,false) + +and apl_sistr lcase a = + try + sistreg lcase a + with NoAplica -> + (match a with + | TApl(f1,f2,t1,t2) -> + let (lt,exi) = apl_listsistr lcase [t1;t2] in + if exi then TApl(f1,f2,pr lt,sn lt) + else raise(NoAplica) + | TFun(x,f,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TFun(x,f,pr lt) + else raise(NoAplica) + | TPar(f1,f2,t1,t2) -> + let (lt,exi) = apl_listsistr lcase [t1;t2] in + if exi then TPar(f1,f2,pr lt,sn lt) + else raise(NoAplica) + | TInl(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TInl(f1,f2,pr lt) + else raise(NoAplica) + | TInr(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TInr(f1,f2,pr lt) + else raise(NoAplica) + | TFst(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TFst(f1,f2,pr lt) + else raise(NoAplica) + | TSnd(f1,f2,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TSnd(f1,f2,pr lt) + else raise(NoAplica) + | TZ(f,t) -> + let (lt,exi) = apl_listsistr lcase [t] in + if exi then TZ(f,pr lt) + else raise(NoAplica) + | TSum(t1,t2) -> + let (lt,exi) = apl_listsistr lcase [t1;t2] in + if exi then TSum(pr lt,sn lt) + else raise(NoAplica) + | TCase([f1;f2;f3],[TFun(v1,ff1,t1);TFun(v2,ff2,t2);t3]) -> + let (t1',exi1) = apl_sistr_try ((t3,v1,true)::lcase) t1 in + let (t2',exi2) = apl_sistr_try ((t3,v2,false)::lcase) t2 in + let (t3',exi3) = apl_sistr_try lcase t3 in + if (exi1 or exi2 or exi3) then + TCase([f1;f2;f3],[TFun(v1,ff1,t1'); + TFun(v2,ff2,t2');t3']) + else raise(NoAplica) + | _ -> raise(NoAplica)) + +(* Indica si hay un zero en el termino *) +let rec tiene_zero = function + | TApl(_,_,t,t1) -> tiene_zero(t) or tiene_zero(t1) + | TFun(_,_,t) -> tiene_zero(t) + | TPar(_,_,t,t1) -> tiene_zero(t) or tiene_zero(t1) + | TInl(_,_,t) -> tiene_zero(t) + | TInr(_,_,t) -> tiene_zero(t) + | TFst(_,_,t) -> tiene_zero(t) + | TSnd(_,_,t) -> tiene_zero(t) + | TCase(_,[t;t1;t2]) -> tiene_zero (t) or tiene_zero (t1) or + tiene_zero(t2) + | TZ(_,t) -> tiene_zero(t) + | TZero(f) -> true + | a -> false + +(* Elemento de la posicion p de una lista *) +let rec lis_pos p = function + | [] -> raise(TacticFailure) + | x::y -> if (p=0) then x else lis_pos (p-1) y + +(* Genera una copia de una formula con reemplazo de los terminos de tipo + FLis por las formulas que aparecen en la posicion p'esima de las + listas respectivas *) +let rec copia_f p = function + | FAnd(a,b) -> FAnd(copia_f p a,copia_f p b) + | FEqu(a,b) -> FEqu(copia_f p a,copia_f p b) + | FOr(a,b) -> FOr(copia_f p a,copia_f p b) + | FImp(a,b) -> FImp(copia_f p a,copia_f p b) + | FNot(a) -> FNot(copia_f p a) + | FLis lf -> lis_pos p lf + | a -> a + +(* Genera una copia de un termino con reemplazo de los terminos de tipo + Lista por los terminos que aparecen en la posicion p'esima de las listas + respectivas *) +let rec copia_t sinplus p = function + | TApl(f,f1,t,t1) -> TApl(copia_f p f,copia_f p f1, + copia_t sinplus p t,copia_t sinplus p t1) + | TFun(x,f,t) -> TFun(x,copia_f p f,copia_t sinplus p t) + | TPar(f,f1,t,t1) -> TPar(copia_f p f,copia_f p f1, + copia_t sinplus p t,copia_t sinplus p t1) + | TInl(f,f1,t) -> TInl(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TInr(f,f1,t) -> TInr(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TFst(f,f1,t) -> TFst(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TSnd(f,f1,t) -> TSnd(copia_f p f,copia_f p f1,copia_t sinplus p t) + | TLis lt -> lis_pos p lt + | TSum(t,t1) -> let s = copia_t sinplus p t in + let s1 = copia_t sinplus p t1 in + if sinplus then + if tiene_zero s then s1 + else s + else TSum(s,s1) + | TCase(lf,lt) -> + TCase(List.map (copia_f p) lf,List.map (copia_t sinplus p) lt) + | TZ(f,t) -> TZ(copia_f p f,copia_t sinplus p t) + | TZero(f) -> TZero(copia_f p f) + | a -> a + +(* Reescribe un lambda termino con constructores TZero y TSum a un lambda + termino *) +let rec normal t = + try normal(apl_sistr [] t) with NoAplica -> copia_t true 0 t + +(*-------------------- Procedimiento de decision --------------------------*) + +(* Indica que no debe buscar mas en el arbol *) +let no_back rev = function + {arb=a;lisbut=l} -> (a <> Nil) & (l=[] or rev) + +(* Funcion que dice si un sequente es demostrable o no. Retorna + un arbol de demostracion del sequente, o vacio. *) +let rec naive intu vp = function + (l,r) as s -> naive_s s intu (s,[]) vp sistema + +(* Dado un secuente s y un subsecuente (en el cual busca una formula + para aplicarle una regla), encuentra un elemento de demostracion. + Si intu es true genera subojetivos equivalentes al original en caso + de no encontrar la demostracion. Si es false, retorna el arbol Vacio*) + +and naive_s s intu seq_acum vp listareg = + (match escoja_regla s seq_acum listareg with + | RNil -> + if intu then + let obj = subobjetivo s vp in + let fapp = ter_subobjetivo vp (fst obj) (ante s) in + let subs_sub = subs_subobj fapp (snd obj) (suce s) in + consd (Cons(Nil,consa s vACIA subs_sub [],Nil)) + [fst obj] + else consd Nil [] + | RCons(subs,lreg,lanew,lrnew) -> + let reversible = !(subs.sReg).ssi or subs.sDel = [] in + ( match aplr_s subs with + | [] -> + consd(Cons(Nil, + consa s !(subs.sReg) subs.sDef subs.sTer, + Nil)) [] + | [a] -> + let {arb=a1;lisbut=l1} as al = (naive intu vp a) in + if no_back reversible al then + consd (Cons(a1, + consa s !(subs.sReg) subs.sDef subs.sTer, + Nil)) l1 + else if (not (reversible)) then + naive_s s intu (lrnew,lanew) vp lreg + else + consd Nil [] + | a::(b::_) -> + let {arb=a1;lisbut=l1} as al1 = naive intu vp a in + let {arb=a2;lisbut=l2} as al2 = naive intu vp b in + if (no_back reversible al1) & (no_back reversible al2) then + consd (Cons(a1, + consa s !(subs.sReg) subs.sDef subs.sTer, + a2)) (l1@l2) + else if (not (reversible)) then + naive_s s intu (lrnew,lanew) vp lreg + else + consd Nil [])) + +(* Crea nuevas substituciones para cada variable del sucedente *) +let rec nuevas_subs t p = function + | [] -> [] + | x::y -> (x,copia_t false p t) :: nuevas_subs t (p+1) y + +(* Busca todos lo Delta que aparecen en el lado izquierdo de la + sustitucion y lo reemplaza por las variables del sucedente del secuente *) +let rec remplacedelta lisv = function + | [] -> [] + | ("Delta",t)::y -> nuevas_subs t 0 lisv @ remplacedelta lisv y + | x::y -> x :: remplacedelta lisv y + +(* Calcula una lista de susbtituciones sobre las variables que aparecen al + en el sucedente del secuente de un arbol de demostracion. De tal forma + que al componerlas y aplicarlas se obtienen los lambda terminos que expresan + la demostracion*) +let rec subs_t = function + | Nil -> [] + | Cons(a,{seq=seq;sd=sd0;st=st0;reg=r},b) -> + let sd = if (!r.rendelta <> []) or (!r.vardelta) then + remplacedelta (lisvar (suce !seq)) sd0 + else sd0 in + let st = if (!r.rendelta <> []) or (!r.vardelta) then + remplacedelta (lisvar (suce !seq)) st0 + else st0 in + [sd] @ (subs_t a) @ [st] @ (subs_t b) + +(* Funcion que compone recursivamente una substitucion con una lista + de substituciones *) +let rec componga_r s = function + | [] -> s + | x::y -> componga_r (comp_st x s) y + +(* Dado un arbol de demostracion de un secuente, calcula los lambda terminos + que expresan la demostracion *) +let lterm = function + | Nil -> [] + | (Cons(_,{seq=seq},_)) as a -> + List.map (function (x,y) -> (x,normal y)) (componga_r [] (subs_t a)) + +(*--------------------- Interface con Coq ---------------------------------*) +(*-- Convierte una formula cci a una formula notacion Tauto --*) + +let (tAUTOFAIL:tactic) = fun _ -> errorlabstrm "TAUTOFAIL" + [< 'sTR "Tauto failed.">] + +let is_imp_term t = + match t with + | DOP2(Prod,_,DLAM(_,b)) -> (not((dependent (Rel 1) b))) + | _ -> false + +(* Chet's code depends on the names of the logical constants. *) + +let tauto_of_cci_fmla gls cciterm = + let rec tradrec cciterm = + if matches gls cciterm and_pattern then + match dest_match gls cciterm and_pattern with + | [a;b] -> FAnd(tradrec a,tradrec b) + | _ -> assert false + else if matches gls cciterm or_pattern then + match dest_match gls cciterm or_pattern with + | [a;b] -> FOr(tradrec a,tradrec b) + | _ -> assert false + else if matches gls cciterm iff_pattern then + match dest_match gls cciterm iff_pattern with + | [a;b] -> FEqu(tradrec a,tradrec b) + | _ -> assert false + else if matches gls cciterm eq_pattern then + match dest_match gls cciterm eq_pattern with + | [a;b;c] -> FEq(FPred a,FPred b, FPred c) + | _ -> assert false + else if matches gls cciterm not_pattern then + match dest_match gls cciterm not_pattern with + | [a] -> FNot(tradrec a) + | _ -> assert false + else if matches gls cciterm false_pattern then + FFalse + else if matches gls cciterm true_pattern then + FTrue + else if is_imp_term cciterm then + match cciterm with + | DOP2(Prod,a,DLAM(_,b)) -> FImp(tradrec a,tradrec (Generic.pop b)) + | _ -> assert false + else FPred cciterm + in + tradrec (whd_betaiota (pf_env gls) (project gls) cciterm) + +(*-- Retorna una lista de todas las variables proposicionales que + aparescan en una lista de formulasS --*) +let rec lisvarprop = function + | [] -> [] + | (_,((FPred x) as fx))::y -> fx::lisvarprop y + | _::y -> lisvarprop y + +(*-- Dado el ambiente COQ construye el lado izquierdo de un secuente + (hipotesis) --*) +let rec constr_lseq gls = function + | ([],[]) -> [] + | (idx::idy,hx::hy) -> + (match (pf_type_of gls hx) with + | DOP0 (Sort (Prop Null)) -> + (TVar(string_of_id idx),tauto_of_cci_fmla gls hx) + :: constr_lseq gls (idy,hy) + |_-> constr_lseq gls (idy,hy)) + | _ -> [] + +(*-- Dado un estado COQ construye el lado derecho de un secuente + (conclusion) --*) +let constr_rseq gls but = [TVar(genvar()), + tauto_of_cci_fmla gls but] + +(*-- Calula la posicion de la lista de un elemento --*) +let rec pos_lis x = function + | [] -> raise TacticFailure + | a::r -> if (x=a) then 1 else 1 + (pos_lis x r) + +(*-- Construye un termino constr dado una formula tauto --*) +let rec cci_of_tauto_fml env = + let cAnd = global_reference CCI (id_of_string "and") + and cOr = global_reference CCI (id_of_string "or") + and cFalse = global_reference CCI (id_of_string "False") + and cTrue = global_reference CCI (id_of_string "True") + and cEq = global_reference CCI (id_of_string "eq") in + function + | FAnd(a,b) -> applistc cAnd + [cci_of_tauto_fml env a;cci_of_tauto_fml env b] + | FOr(a,b) -> applistc cOr + [cci_of_tauto_fml env a; cci_of_tauto_fml env b] + | FEq(a,b,c)-> applistc cEq + [cci_of_tauto_fml env a; cci_of_tauto_fml env b; + cci_of_tauto_fml env c] + | FImp(a,b) -> mkArrow (cci_of_tauto_fml env a) (cci_of_tauto_fml env b) + | FPred a -> a + | FFalse -> cFalse + | FTrue -> cTrue + | FLis lf -> raise TacticFailure + | FVar a -> raise TacticFailure + | FAto a -> raise TacticFailure + | FLisfor a -> raise TacticFailure + | _ -> anomaly "Tauto:cci_of_tauto_fml" + +let search env id = + try + (match lookup_id id (Environ.context env) with + | RELNAME (n,_) -> Rel n + | GLOBNAME _ -> VAR id) + with Not_found -> + global_reference CCI id + +(*-- Construye un termino constr de un termino tauto --*) +let cci_of_tauto_term env t = + let cFalse_ind = global_reference CCI (id_of_string "False_ind") + and cconj = global_reference CCI (id_of_string "conj") + and cor_ind = global_reference CCI (id_of_string "or_ind") + and cor_introl = global_reference CCI (id_of_string "or_introl") + and cor_intror = global_reference CCI (id_of_string "or_intror") + and cproj1 = global_reference CCI (id_of_string "proj1") + and cproj2 = global_reference CCI (id_of_string "proj2") + and crefl = global_reference CCI (id_of_string "refl_equal") + and csim = global_reference CCI (id_of_string "sym_eq") + and ci = global_reference CCI (id_of_string "I") + in + let rec ter_constr l = function + | TVar x -> (try (try Rel(pos_lis x l) + with TacticFailure -> + search env (id_of_string x)) + with _ -> raise TacticFailure) + | TZ(f,x) -> applistc cFalse_ind + [cci_of_tauto_fml env f;ter_constr l x] + | TSum(t1,t2) -> ter_constr l t1 + | TExi (x) -> (try search env (id_of_string x) with + _ -> raise TacticFailure) + | TApl(_,_,t1,t2) -> applistc (ter_constr l t1) [ter_constr l t2] + | TPar(f1,f2,t1,t2) -> applistc cconj + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2; + ter_constr l t1;ter_constr l t2] + | TInl(f1,f2,t) -> applistc cor_introl + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2; + ter_constr l t] + | TInr(f1,f2,t) -> applistc cor_intror + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2; + ter_constr l t] + | TFst(f1,f2,t) -> applistc cproj1 + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2; + ter_constr l t] + | TSnd(f1,f2,t) -> applistc cproj2 + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2; + ter_constr l t] + | TRefl(f1,f2) -> applistc crefl + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2] + | TSim(f1,f2,f3,t) -> applistc csim + [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2; + cci_of_tauto_fml env f3;ter_constr l t] + | TCase(lf,lt) -> applistc cor_ind + ((List.map (cci_of_tauto_fml env) lf)@ + (List.map (ter_constr l) lt)) + | TFun(n,f,t) -> + Environ.lambda_name env + (Name(id_of_string n ), cci_of_tauto_fml env f,ter_constr (n::l) t) + | TTrue -> ci + | TLis _ -> raise TacticFailure + | TLister _ -> raise TacticFailure + | TZero _ -> raise TacticFailure + in + ter_constr [] t + +let cutUsing id t = (tclTHENS (Tactics.cut t) ([intro_using id;tclIDTAC])) + +let cut_in_parallelUsing idlist l = + let rec prec l_0 = function + | [] -> tclIDTAC + | h::t -> + (tclTHENS (cutUsing (id_of_string (List.hd l_0)) h) + ([prec (List.tl l_0) t;tclIDTAC])) + in + prec (List.rev idlist) (List.rev l) + +let exacto tt gls = + match (try cci_of_tauto_term (pf_env gls) tt with + _ -> (DOP0 Prod)) with (* Efectivamente, es cualquier cosa!! *) + | (DOP0 Prod) -> tAUTOFAIL gls (* Esto confirma el comentario anterior *) + | t -> (exact t) gls + +let subbuts l hyp = cut_in_parallelUsing + (lisvar l) + (List.map (cci_of_tauto_fml (gLOB hyp)) (lisfor l)) + +let t_exacto = ref (TVar "#") + +let tautoOR ti gls = + let hyp = pf_untyped_hyps gls in + let thyp = pf_hyps gls in + hipvar := ids_of_sign hyp; + let but = pf_concl gls in + let seq = (constr_lseq gls (ids_of_sign hyp,vals_of_sign hyp), + constr_rseq gls but) in + let vp = lisvarprop (ante seq) in + match naive ti vp seq with + | {arb=Nil} -> + tAUTOFAIL gls + | {arb=arb;lisbut=l} -> + let se = apl ([],[],[]) (lterm arb) [] seq in + let tt = fst(List.hd(suce se)) in + (t_exacto := tt; + subbuts l thyp gls) + +let exact_Idtac = function + | 0 -> exacto (!t_exacto) + | _ -> tclIDTAC + +let tautoOR_0 gl = + tclORELSE + (tclTHEN_i (tautoOR false) exact_Idtac 0) + tAUTOFAIL gl + +let intuitionOR = + tclTRY (tclTHEN + (tclTHEN_i (tautoOR true) exact_Idtac 0) + default_full_auto) + +(*--- Mixed code Chet-Cesar ---*) + +let rec prove tauto_intu g = + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_hypothesis out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_absurdity_elim out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_and_elim out_some) (prove tauto_intu))) + (tclORELSE (tryAllHyps (flush stdout;clauseTacThen + (compose dyck_atomic_imply_elim out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_and_imply_elim out_some) + (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen + (compose dyck_or_imply_elim out_some) + (prove tauto_intu))) + (tclORELSE (tclTHEN dyck_and_intro (prove tauto_intu)) + (tclORELSE (tclTHEN dyck_imply_intro (prove tauto_intu)) + (tclORELSE (tryAllHyps (flush stdout;clauseTacThen + (compose dyck_or_elim out_some) (prove tauto_intu))) + (tclORELSE (tryAllHyps (clauseTacThen (* 28/5/99, ajout par HH *) + (compose dyck_imply_imply_elim out_some) + (prove tauto_intu))) + tauto_intu)))))))))) g + +let tauto gls = + let strToOccs x = ([],Nametab.sp_of_id CCI (id_of_string x)) in + (tclTHEN (onAllClausesLR + (unfold_option [strToOccs "not";strToOccs "iff"])) + (prove tautoOR_0)) gls + +let intuition gls = + let strToOccs x = ([],Nametab.sp_of_id CCI (id_of_string x)) in + (tclTHEN + ((tclTHEN (onAllClausesLR + (unfold_option [strToOccs "not";strToOccs "iff"])) + (prove intuitionOR))) intros) gls + +let tauto_tac = hide_atomic_tactic "Tauto" tauto + +let intuition_tac = hide_atomic_tactic "Intuition" intuition diff --git a/tactics/tauto.mli b/tactics/tauto.mli new file mode 100644 index 000000000..27bd8ee43 --- /dev/null +++ b/tactics/tauto.mli @@ -0,0 +1,127 @@ + +(* $Id$ *) + +(* Mars 1993 *) +(* Autor: Cesar A. Munnoz H *) + +open Tacmach +open Term + +(* Prototipo *) +(* Estructuras de Datos *) + +type formula = + | FVar of string + | FAnd of formula*formula + | FOr of formula*formula + | FImp of formula*formula + | FEqu of formula*formula + | FNot of formula + | FEq of formula*formula*formula + | FPred of constr (* Predicado proposicional *) + | FFalse + | FTrue + (* La siguiente no puede aparecer en una formula de entrada *) + (* Representa una formula atomica cuando aparece en un principal de una + regla *) + | FLis of formula list (* Lista de formulas *) + | FAto of string (* Formula atomica *) + | FLisfor of string (* Variable para una lista de formulas *) + (* En el antecedente se llama GAMA, + en el sucedente DELTA *) + +(* Terminos en calculo lambda *) +type termino = + | TVar of string + | TApl of formula*formula*termino*termino + | TFun of string*formula*termino + | TPar of formula*formula*termino*termino + | TInl of formula*formula*termino + | TInr of formula*formula*termino + | TFst of formula*formula*termino + | TSnd of formula*formula*termino + | TCase of formula list * termino list + | TZ of formula * termino + | TExi of string + | TRefl of formula * formula (*Reflexividad de la igualdad *) + | TSim of formula * formula * formula * termino + (*Simetria de la igualdad *) + | TTrue + (* Los siguientes terminos se usan solamente en las sustituciones *) + | TSum of termino*termino (* Suma de terminos *) + | TLis of termino list (* Lista de terminos *) + | TLister of string (* Variable para una lista de terminos *) + (* En el antecendete se llama Gama, + en el sucedente Delta *) + | TZero of formula (* Milagro *) + +(* Es una formula asociada con un termino del calculo lambda, o los + multiconjuntos Gama y Delta *) +type formulaT = termino*formula + +(* La primera componente es el antecedente, la segunda es sucedente *) +type sequente = formulaT list * formulaT list + +(* Substitucion de variable por una formula *) +type subsF = (string*formula) list + +(* Substitucion de variable por un lambda termino *) +type subsT = (string*termino) list + +type regla = { + tip: string; (* Tipo de la formula principal *) + heu: bool; (* Si es una regla heuristica o no *) + ant: bool; (* Si principal es antecedente o sucedente *) + pri: formulaT;(* Formula principal de la regla *) + pre: sequente list; (* Premisas de la regla *) + res: sequente;(* Restricciones para la aplicacion de una regla*) + def: subsT; (* Definicion de los terminos del lado derecho *) + sub: subsT; (* Substitucion que se aplica al lado derecho de la + conclusion para obetener el lambda termino *) + ren: string list; (* Variables que se deben renombrar *) + vardelta:bool; (* Si se usa la variable proposicional DELTA *) + ssi:bool; (* Si la regla es reversible o no *) + rendelta: string list} (* Renombramientos de delta *) + (* Note que si Res = A |- B, entonces la conclusion de la regla es + A,Gama,Pri' |- B, Pri'',Delta + Si ant = true Pri'= Pri + Si ant =false Pri''=Pri*) + +(* Substitucion Formula Termino para aplicar una regla *) +type sFT = { + sReg : regla ref; (*Apuntador a la regla *) + sFor : subsF; (*Substitucion de Formulas *) + sGam : formulaT list; (* Lista de formulas de Gamma *) + sDel : formulaT list; (* Lista de formulas de Delta *) + sRen : (string*subsT) list; (* Renombramientos de variables *) + sTer : subsT; (* Susbstitucion de terminos *) + sDef : subsT } (* Definicion de terminos *) + +type subsFT = SNil | SCons of sFT + +type reglaSub = RNil | RCons of (sFT*regla list*formulaT list*sequente) + +(* De un arbol de demostracion *) +type nodo = { + seq: sequente ref; (* Sequente que se resuelve *) + reg: regla ref; (* Regla usada para resolver *) + sd: subsT; (* Substitucion que define los lambda terminos *) + st: subsT } (* Substitucion que calcula el lambda termino *) + +(* Arbol de demostracion *) +type arbol = Nil | Cons of arbol * nodo * arbol + +(* Demostracion *) +(* Si el secuente es valido Arb es un arbol de demostracion y Lisbut + es vacio, sino Lisbut es un contexto en el cual Arb es valido *) +type demostracion = { arb : arbol; lisbut : formulaT list } + +(* Definicion de excepcion para rescribir terminos *) +exception NoAplica +exception TacticFailure + +val tauto_tac : tactic +val intuition : tactic +val intuition_tac : tactic +val tauto : tactic + |