diff options
43 files changed, 3096 insertions, 128 deletions
@@ -135,6 +135,10 @@ tactics/dhyp.cmi: kernel/names.cmi proofs/tacmach.cmi tactics/dn.cmi: lib/tlm.cmi tactics/elim.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ tactics/tacticals.cmi kernel/term.cmi +tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/names.cmi tactics/pattern.cmi proofs/proof_trees.cmi \ + kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi tactics/wcclausenv.cmi tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_trees.cmi \ tactics/tacentries.cmi proofs/tacmach.cmi kernel/term.cmi tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi kernel/term.cmi \ @@ -152,8 +156,9 @@ tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \ kernel/reduction.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ tactics/tacticals.cmi kernel/term.cmi tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi -tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \ - proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.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 \ + proofs/tacmach.cmi kernel/term.cmi toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \ pretyping/tacred.cmi kernel/term.cmi toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi @@ -364,11 +369,11 @@ library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \ library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \ library/libobject.cmi library/library.cmo: kernel/environ.cmi library/global.cmi library/lib.cmi \ - library/libobject.cmi kernel/names.cmi lib/pp.cmi lib/system.cmi \ - lib/util.cmi library/library.cmi + library/libobject.cmi kernel/names.cmi lib/pp.cmi library/summary.cmi \ + lib/system.cmi lib/util.cmi library/library.cmi library/library.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \ - library/libobject.cmx kernel/names.cmx lib/pp.cmx lib/system.cmx \ - lib/util.cmx library/library.cmi + library/libobject.cmx kernel/names.cmx lib/pp.cmx library/summary.cmx \ + lib/system.cmx lib/util.cmx library/library.cmi library/nametab.cmo: kernel/names.cmi library/summary.cmi library/nametab.cmi library/nametab.cmx: kernel/names.cmx library/summary.cmx library/nametab.cmi library/redinfo.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \ @@ -396,7 +401,7 @@ parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \ pretyping/pretype_errors.cmi pretyping/pretyping.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ pretyping/syntax_def.cmi pretyping/tacred.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi + pretyping/typing.cmi kernel/univ.cmi lib/util.cmi parsing/astterm.cmi parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \ @@ -404,7 +409,7 @@ parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \ pretyping/pretype_errors.cmx pretyping/pretyping.cmx \ pretyping/rawterm.cmx kernel/reduction.cmx kernel/sign.cmx \ pretyping/syntax_def.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi + pretyping/typing.cmx kernel/univ.cmx lib/util.cmx parsing/astterm.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ @@ -759,6 +764,26 @@ tactics/elim.cmx: proofs/clenv.cmx kernel/generic.cmx tactics/hiddentac.cmx \ kernel/names.cmx tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx tactics/elim.cmi +tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \ + kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \ + lib/gmapl.cmi kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \ + library/libobject.cmi proofs/logic.cmi kernel/names.cmi \ + tactics/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ + kernel/reduction.cmi library/summary.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi kernel/typeops.cmi \ + pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi +tactics/equality.cmx: parsing/astterm.cmx parsing/coqast.cmx \ + kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \ + lib/gmapl.cmx kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \ + library/libobject.cmx proofs/logic.cmx kernel/names.cmx \ + tactics/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ + kernel/reduction.cmx library/summary.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx kernel/typeops.cmx \ + pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx tactics/wcclausenv.cmx tactics/equality.cmi 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 \ @@ -826,15 +851,19 @@ tactics/termdn.cmx: tactics/dn.cmx kernel/generic.cmx kernel/term.cmx \ tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi proofs/logic.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi lib/util.cmi tactics/wcclausenv.cmi + proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + tactics/wcclausenv.cmi tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx library/global.cmx proofs/logic.cmx kernel/names.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi + proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + tactics/wcclausenv.cmi 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 \ @@ -870,15 +899,15 @@ toplevel/discharge.cmo: pretyping/class.cmi pretyping/classops.cmi \ kernel/generic.cmi library/global.cmi kernel/inductive.cmi \ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \ kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/recordops.cmi \ - kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \ - kernel/typeops.cmi lib/util.cmi toplevel/discharge.cmi + kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi \ + lib/util.cmi toplevel/discharge.cmi toplevel/discharge.cmx: pretyping/class.cmx pretyping/classops.cmx \ kernel/constant.cmx library/declare.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/generic.cmx library/global.cmx kernel/inductive.cmx \ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/recordops.cmx \ - kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \ - kernel/typeops.cmx lib/util.cmx toplevel/discharge.cmi + kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx kernel/typeops.cmx \ + lib/util.cmx toplevel/discharge.cmi toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/inductive.cmi \ parsing/lexer.cmi proofs/logic.cmi lib/options.cmi lib/pp.cmi \ kernel/type_errors.cmi lib/util.cmi toplevel/errors.cmi diff --git a/.depend.coq b/.depend.coq index 1f1fc0a93..784b0e979 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,16 +1,23 @@ +theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v +theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v +theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo +theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo +theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v +theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo +theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo -theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo +theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo -theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo +theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo +theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo -theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo -theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo theories/Init/Datatypes.vo: theories/Init/Datatypes.v -test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v +theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v +test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v syntax/PPTactic.vo: syntax/PPTactic.v syntax/PPConstr.vo: syntax/PPConstr.v syntax/PPCommand.vo: syntax/PPCommand.v @@ -20,7 +20,7 @@ noargument: @echo " ./configure" @echo " make world" @echo " make install" - @echo " make cleanall" + @echo " make clean" @echo "or make archclean" ########################################################################### @@ -41,7 +41,7 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE) -COQINCLUDES=-I theories/Init +COQINCLUDES=-I theories/Init -I theories/Logic ########################################################################### # Objects files @@ -107,7 +107,7 @@ 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 +HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -163,6 +163,9 @@ $(COQC): $(COQCCMO) scripts/coqc.cmo: scripts/coqc.ml4 $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< +archclean:: + rm -f scripts/coqc scripts/coqmktop + # we provide targets for each subdirectories lib: $(LIB) @@ -174,27 +177,48 @@ parsing: $(PARSING) pretyping: $(PRETYPING) toplevel: $(TOPLEVEL) -# states +########################################################################### +# theories and states +########################################################################### -states: states/barestate.coq +states: states/barestate.coq states/initial.coq SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v states/barestate.coq: $(SYNTAXPP) coqtop.byte ./coqtop.byte -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq -########################################################################### -# theories -########################################################################### +INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ + theories/Init/DatatypesSyntax.vo theories/Init/Prelude.vo \ + theories/Init/Logic.vo theories/Init/Specif.vo \ + theories/Init/LogicSyntax.vo theories/Init/SpecifSyntax.vo \ + theories/Init/Logic_Type.vo theories/Init/Wf.vo \ + theories/Init/Logic_TypeSyntax.vo + +theories/Init/%.vo: theories/Init/%.v states/barestate.coq + $(COQC) -q -I theories/Init -is states/barestate.coq $< + +TACTICSVO=tactics/Equality.vo + +tactics/%.vo: tactics/%.v states/barestate.coq + $(COQC) -q -I tactics -is states/barestate.coq $< -INIT=theories/Init/Datatypes.vo theories/Init/Peano.vo \ - theories/Init/DatatypesSyntax.vo theories/Init/Prelude.vo \ - theories/Init/Logic.vo theories/Init/Specif.vo \ - theories/Init/LogicSyntax.vo theories/Init/SpecifSyntax.vo \ - theories/Init/Logic_Type.vo theories/Init/Wf.vo \ - theories/Init/Logic_TypeSyntax.vo +states/initial.coq: states/barestate.coq $(INITVO) $(TACTICSVO) + ./coqtop.byte -q -batch -silent -is states/barestate.coq -I tactics -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq -theories: $(INIT) +clean:: + rm -f states/barestate.coq states/initial.coq + +LOGICVO=theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ + theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ + theories/Logic/Classical_Pred_Type.vo theories/Logic/Eqdep_dec.vo \ + theories/Logic/Classical_Prop.vo + +theories: $(INITVO) $(LOGICVO) + +clean:: + rm -f theories/*/*.vo theories/*/*~ + rm -f tactics/*.vo tactics/*~ ########################################################################### # tools @@ -223,6 +247,9 @@ tools/coq-tex: tools/coq-tex.ml $(OCAMLOPT) $(OPTFLAGS) -o tools/coq-tex str.cmxa tools/coq-tex.ml \ $(STRLIB) +archclean:: + rm -f tools/coqdep tools/gallina tools/coq-tex tools/coq_makefile + ########################################################################### # minicoq ########################################################################### @@ -279,6 +306,9 @@ doc/coq.tex: doc/preamble.tex $(LPFILES) ocamlweb --no-preamble $(LPFILES) >> doc/coq.tex echo "\end{document}" >> doc/coq.tex +clean:: + rm -f doc/*~ doc/coq.tex + ########################################################################### # Emacs tags ########################################################################### @@ -302,7 +332,7 @@ tags: parsing/lexer.cmo: parsing/lexer.ml $(OCAMLC_P4O) -c $< -cleanall:: +clean:: rm -f parsing/lexer.ml beforedepend:: parsing/lexer.ml @@ -327,6 +357,9 @@ GRAMMARCMO=./lib/pp_control.cmo ./lib/pp.cmo ./lib/util.cmo ./lib/dyn.cmo \ parsing/grammar.cma: $(GRAMMARCMO) $(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ +clean:: + rm -f parsing/grammar.cma + CAMLP4GRAMMAR=camlp4o -I parsing pa_extend.cmo grammar.cma OPTCAMLP4GRAMMAR=camlp4o -I parsing pa_extend.cmo grammar.cma $(OSDEPP4OPTFLAGS) @@ -407,11 +440,11 @@ archclean:: rm -f toplevel/*.cmx toplevel/*.[so] rm -f tools/*.cmx tools/*.[so] rm -f coqtop.opt coqtop.byte minicoq - rm -f tools/coqdep tools/gallina tools/coq-tex tools/coq_makefile + rm -f scripts/*.cmx scripts/*~ -cleanall:: archclean +clean:: archclean rm -f *~ - rm -f doc/*~ + rm -f gmon.out core rm -f config/*.cm[io] config/*~ rm -f lib/*.cm[io] lib/*~ rm -f kernel/*.cm[io] kernel/*~ @@ -422,6 +455,7 @@ cleanall:: archclean rm -f pretyping/*.cm[io] pretyping/*~ rm -f toplevel/*.cm[io] toplevel/*~ rm -f tools/*.cm[io] tools/*~ + rm -f scripts/*.cm[io] scripts/*~ cleanconfig:: rm -f config/Makefile config/coq_config.ml diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7 index dc6c2279d..5e9b2aa02 100755 --- a/dev/ocamldebug-v7 +++ b/dev/ocamldebug-v7 @@ -3,7 +3,7 @@ # wrap around ocamldebug for Coq # export COQTOP=`coqtop -where` -export COQTOP=/users/homepc89/jcf/coq/V7 +export COQTOP=/home/jc/coq/V7 export COQLIB=$COQTOP export COQTH=$COQLIB/theories export CAMLP4LIB=`camlp4 -where` diff --git a/kernel/environ.ml b/kernel/environ.ml index c8c85c76e..7507be838 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -193,6 +193,8 @@ let named_hd env a = function 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 + (* Abstractions. *) let evaluable_abst env = function diff --git a/kernel/environ.mli b/kernel/environ.mli index 6d38ad819..31edb0d7f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -53,6 +53,7 @@ val id_of_global : env -> sorts oper -> identifier 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 translucent_abst : env -> constr -> bool val evaluable_abst : env -> constr -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d7f8b8386..b2c5df74f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -434,6 +434,19 @@ let add_mind sp mie env = let add_constraints = add_constraints +let pop_vars idl env = + let rec remove n sign = + if n = 0 then + sign + else + match sign with + | (id::ids,_::tys) -> + if not (List.mem id idl) then anomaly "pop_vars"; + remove (pred n) (ids,tys) + | _ -> anomaly "pop_vars" + in + change_hyps (remove (List.length idl)) env + let export = export let import = import diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index afa8d3ef9..07e95197c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -40,6 +40,8 @@ val add_mind : -> safe_environment val add_constraints : constraints -> safe_environment -> safe_environment +val pop_vars : identifier list -> safe_environment -> safe_environment + val lookup_var : identifier -> safe_environment -> name * typed_type val lookup_rel : int -> safe_environment -> name * typed_type val lookup_constant : section_path -> safe_environment -> constant_body diff --git a/kernel/term.ml b/kernel/term.ml index 56dd87f8f..411326106 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -424,6 +424,10 @@ let destEvar = function | DOPN (Evar n, a) -> (n,a) | _ -> invalid_arg "destEvar" +let num_of_evar = function + | DOPN (Evar n, _) -> n + | _ -> anomaly "num_of_evar called with bad args" + (* Destructs an abstract term *) let destAbst = function | DOPN (Abst sp, a) -> (sp, a) diff --git a/kernel/term.mli b/kernel/term.mli index a7f2e6180..ab1db881a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -288,6 +288,7 @@ val args_of_const : constr -> constr array (* Destructs an existential variable *) val destEvar : constr -> int * constr array +val num_of_evar : constr -> int (* Destrucy an abstract term *) val destAbst : constr -> section_path * constr array diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1254d5ef9..4b20f3b0a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -84,7 +84,7 @@ let check_hyps id env sigma hyps = let type_of_constant env sigma (sp,args) = let cb = lookup_constant sp env in let hyps = cb.const_hyps in - check_hyps (basename sp) env sigma hyps; + (* TODO: check args *) instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) (* Inductive types. *) @@ -99,7 +99,7 @@ let instantiate_arity mis = let type_of_inductive env sigma i = let mis = lookup_mind_specif i env in let hyps = mis.mis_mib.mind_hyps in - check_hyps (basename mis.mis_sp) env sigma hyps; + (* TODO: check args *) instantiate_arity mis (* Constructors. *) @@ -112,7 +112,7 @@ let instantiate_lc mis = let type_of_constructor env sigma ((ind_sp,j),args as cstr) = let mind = inductive_of_constructor cstr in let mis = lookup_mind_specif mind env in - check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps); + (* TODO: check args *) let specif = instantiate_lc mis in let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in if j > mis_nconstr mis then @@ -161,7 +161,7 @@ let type_of_existential env sigma c = let evi = Evd.map sigma ev in let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in - check_hyps id env sigma hyps; + (* TODO: check args *) instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) diff --git a/lib/util.ml b/lib/util.ml index 567c8edb6..363e13b1a 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -119,6 +119,14 @@ let list_map_i f = in map_i_rec +let list_map2_i f i l1 l2 = + let rec map_i i = function + | ([], []) -> [] + | ((h1::t1), (h2::t2)) -> (f i h1 h2) :: (map_i (succ i) (t1,t2)) + | (_, _) -> invalid_arg "map2_i" + in + map_i i (l1,l2) + let list_index x = let rec index_x n = function | y::l -> if x = y then n else index_x (succ n) l @@ -233,6 +241,13 @@ let list_except_assoc e = let list_join_map f l = List.flatten (List.map f l) +let list_try_find f = + let rec try_find_f = function + | [] -> failwith "try_find" + | h::t -> try f h with Failure _ -> try_find_f t + in + try_find_f + (* Arrays *) @@ -331,6 +346,18 @@ let array_map2 f v1 v2 = res end +let array_map2_i f v1 v2 = + if Array.length v1 <> Array.length v2 then invalid_arg "array_map2"; + if Array.length v1 == 0 then + [| |] + else begin + let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in + for i = 1 to pred (Array.length v1) do + res.(i) <- f i v1.(i) v2.(i) + done; + res + end + let array_map3 f v1 v2 v3 = if Array.length v1 <> Array.length v2 || Array.length v1 <> Array.length v3 then invalid_arg "array_map3"; diff --git a/lib/util.mli b/lib/util.mli index e0743627d..77c87d33f 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -52,6 +52,8 @@ val list_tabulate : (int -> 'a) -> int -> 'a list val list_assign : 'a list -> int -> 'a -> 'a list val list_distinct : 'a list -> bool val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list +val list_map2_i : + (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list val list_index : 'a -> 'a list -> int val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a @@ -73,7 +75,7 @@ val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list val list_except_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list val list_join_map : ('a -> 'b list) -> 'a list -> 'b list - +val list_try_find : ('a -> 'b) -> 'a list -> 'b (*s Arrays. *) @@ -95,6 +97,7 @@ val array_list_of_tl : 'a array -> 'a list val array_map_to_list : ('a -> 'b) -> 'a array -> 'b list val array_chop : int -> 'a array -> 'a array * 'a array val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array +val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val array_map3 : ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array diff --git a/library/declare.ml b/library/declare.ml index ff46ad72a..5e87c1a74 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -57,12 +57,11 @@ let cache_variable (sp,(id,(ty,_,_) as vd,imps)) = if imps then declare_var_implicits id; vartab := Spmap.add sp vd !vartab -let load_variable _ = anomaly "we shouldn't load a variable" +let load_variable _ = () -let open_variable _ = anomaly "we shouldn't open a variable" +let open_variable _ = () -let specification_variable _ = - anomaly "we shouldn't extract the specification of a variable" +let specification_variable x = x let (in_variable, out_variable) = let od = { diff --git a/library/global.ml b/library/global.ml index af9dbe1d5..924267288 100644 --- a/library/global.ml +++ b/library/global.ml @@ -37,6 +37,8 @@ let add_parameter sp c = global_env := add_parameter sp c !global_env let add_mind sp mie = global_env := add_mind sp mie !global_env let add_constraints c = global_env := add_constraints c !global_env +let pop_vars ids = global_env := pop_vars ids !global_env + let lookup_var id = lookup_var id !global_env let lookup_rel n = lookup_rel n !global_env let lookup_constant sp = lookup_constant sp !global_env diff --git a/library/global.mli b/library/global.mli index e9e42cf5e..fbf034527 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,6 +30,8 @@ val add_parameter : section_path -> constr -> unit val add_mind : section_path -> mutual_inductive_entry -> unit val add_constraints : constraints -> unit +val pop_vars : identifier list -> unit + val lookup_var : identifier -> name * typed_type val lookup_rel : int -> name * typed_type val lookup_constant : section_path -> constant_body diff --git a/library/lib.ml b/library/lib.ml index 75caa4816..8d91666a3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -9,7 +9,8 @@ open Summary type node = | Leaf of obj | Module of string - | OpenedSection of string * Summary.frozen + | OpenedSection of string + | ClosedSection of string * library_segment | FrozenState of Summary.frozen and library_entry = section_path * node @@ -101,8 +102,7 @@ let contents_after = function let open_section s = let sp = make_path (id_of_string s) OBJ in - let fs = freeze_summaries () in - add_entry sp (OpenedSection (s,fs)); + add_entry sp (OpenedSection s); path_prefix := !path_prefix @ [s]; sp @@ -123,18 +123,19 @@ let start_module s = let is_opened_section = function (_,OpenedSection _) -> true | _ -> false let close_section s = - let (sp,frozen) = + let sp = try match find_entry_p is_opened_section with - | sp,OpenedSection (s',fs) -> - if s <> s' then error "this is not the last opened section"; (sp,fs) + | sp,OpenedSection s' -> + if s <> s' then error "this is not the last opened section"; sp | _ -> assert false with Not_found -> error "no opened section" in let (after,_,before) = split_lib sp in lib_stk := before; + add_entry (make_path (id_of_string s) OBJ) (ClosedSection (s,after)); pop_path_prefix (); - (sp,after,frozen) + (sp,after) (* The following function exports the whole library segment, that will be saved as a module. Objects are presented in chronological order, and @@ -145,6 +146,7 @@ let export_module () = let rec export acc = function | (_,Module _) :: _ -> acc | (_,Leaf _) as node :: stk -> export (node::acc) stk + | (_,ClosedSection _) as node :: stk -> export (node::acc) stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,FrozenState _) :: stk -> export acc stk | _ -> assert false diff --git a/library/lib.mli b/library/lib.mli index 36b49bbeb..1d601f7b6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -14,7 +14,8 @@ open Summary type node = | Leaf of obj | Module of string - | OpenedSection of string * Summary.frozen + | OpenedSection of string + | ClosedSection of string * library_segment | FrozenState of Summary.frozen and library_entry = section_path * node @@ -34,7 +35,7 @@ val contents_after : section_path option -> library_segment (*s Opening and closing a section. *) val open_section : string -> section_path -val close_section : string -> section_path * library_segment * Summary.frozen +val close_section : string -> section_path * library_segment val make_path : identifier -> path_kind -> section_path val cwd : unit -> string list diff --git a/library/library.ml b/library/library.ml index 913f396d9..893a44921 100644 --- a/library/library.ml +++ b/library/library.ml @@ -29,30 +29,31 @@ type module_t = { module_deps : (string * Digest.t * bool) list; module_digest : Digest.t } -let modules_table = - (Hashtbl.create 17 : (string, module_t) Hashtbl.t) +let modules_table = ref Stringmap.empty + +let _ = + Summary.declare_summary "MODULES" + { Summary.freeze_function = (fun () -> !modules_table); + Summary.unfreeze_function = (fun ft -> modules_table := ft); + Summary.init_function = (fun () -> modules_table := Stringmap.empty) } let find_module s = try - Hashtbl.find modules_table s + Stringmap.find s !modules_table with Not_found -> error ("Unknown module " ^ s) let module_is_loaded s = - try let _ = Hashtbl.find modules_table s in true with Not_found -> false + try let _ = Stringmap.find s !modules_table in true with Not_found -> false -let module_is_opened s = - (find_module s).module_opened +let module_is_opened s = (find_module s).module_opened let loaded_modules () = - let l = ref [] in - Hashtbl.iter (fun s _ -> l := s :: !l) modules_table; - !l + Stringmap.fold (fun s _ l -> s :: l) !modules_table [] let opened_modules () = - let l = ref [] in - Hashtbl.iter (fun s m -> if m.module_opened then l := s :: !l) modules_table; - !l + Stringmap.fold (fun s m l -> if m.module_opened then s :: l else l) + !modules_table [] let vo_magic_number = 0700 @@ -63,6 +64,7 @@ let segment_iter f = let rec apply = function | sp,Leaf obj -> f (sp,obj) | _,OpenedSection _ -> assert false + | _,ClosedSection (_,seg) -> iter seg | _,(FrozenState _ | Module _) -> () and iter seg = List.iter apply seg @@ -106,7 +108,7 @@ let rec load_module_from doexp s f = List.iter (load_mandatory_module doexp s) m.module_deps; Global.import m.module_compiled_env; load_objects m.module_declarations; - Hashtbl.add modules_table s m; + modules_table := Stringmap.add s m !modules_table; m and load_mandatory_module doexp caller (s,d,export) = @@ -116,8 +118,10 @@ and load_mandatory_module doexp caller (s,d,export) = if doexp && export then open_module s and find_module doexp s f = - try Hashtbl.find modules_table s with Not_found -> load_module_from doexp s f - + try + Stringmap.find s !modules_table + with Not_found -> + load_module_from doexp s f let load_module s = function | None -> let _ = load_module_from true s s in () @@ -138,11 +142,9 @@ let require_module spec name fileopt export = (* [save_module s] saves the module [m] to the disk. *) let current_imports () = - let l = ref [] in - Hashtbl.iter - (fun _ m -> l := (m.module_name, m.module_digest, m.module_exported) :: !l) - modules_table; - !l + Stringmap.fold + (fun _ m l -> (m.module_name, m.module_digest, m.module_exported) :: l) + !modules_table [] let save_module_to s f = let seg = export_module () in diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 989b78638..087cdb711 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -513,9 +513,6 @@ let constr_of_com sigma env com = let constr_of_com_sort sigma sign com = constr_of_com1 true sigma sign com -let constr_of_com_pattern sigma sign com = - constr_of_com1 true sigma sign com - let fconstr_of_com1 is_ass sigma env com = fconstr_of_com_env1 is_ass sigma env com @@ -560,13 +557,61 @@ let fconstruct_with_univ sigma sign com = j *) -open Closure -open Tacred +(* To process patterns, we need a translation from AST to term + without typing at all. *) + +let ctxt_of_ids ids = + Array.of_list (List.map (function id -> VAR id) ids) + +let constr_of_ref vars = function + | RConst (sp,ids) -> DOPN (Const sp, ctxt_of_ids ids) + | RInd (ip,ids) -> DOPN (MutInd ip, ctxt_of_ids ids) + | RConstruct (cp,ids) -> DOPN (MutConstruct cp, ctxt_of_ids ids) + | RAbst sp -> DOPN (Abst sp, [||]) + | RVar id -> + (try Rel (list_index (Name id) vars) with Not_found -> VAR id) + | REVar (n,ids) -> DOPN (Evar n, ctxt_of_ids ids) + | RMeta n -> DOP0 (Meta n) + +let constr_of_rawconstr c = + let rec glob vars = function + | RRef (_,r) -> + constr_of_ref vars r + | RApp (_,c,cl) -> + let l = List.map (glob vars) (c::cl) in + DOPN (AppL, Array.of_list l) + | RBinder (_,BProd,na,c1,c2) -> + DOP2 (Prod, glob vars c1, DLAM (na, glob (na::vars) c2)) + | RBinder (_,BLambda,na,c1,c2) -> + DOP2 (Lambda, glob vars c1, DLAM (na, glob (na::vars) c2)) + | RSort (_,RProp c) -> + DOP0 (Sort (Prop c)) + | RSort (_,RType) -> + DOP0 (Sort (Type (Univ.dummy_univ))) + | RHole _ -> + DOP0 (Meta (new_meta())) + | RCast (_,c1,c2) -> + DOP2 (Cast, glob vars c1, glob vars c2) + | _ -> + error "constr_of_rawconstr: not implemented" + in + glob [] c + +let constr_of_com_pattern sigma env com = + let c = raw_constr_of_com sigma (context env) com in + try + constr_of_rawconstr c + with e -> + Stdpp.raise_with_loc (Ast.loc com) e + (* Translation of reduction expression: we need trad because of Fold * Moreover, reduction expressions are used both in tactics and in * vernac. *) +open Closure +open Tacred + let glob_nvar com = let s = nvar_of_ast com in try diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 3e522f95c..2fc706337 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -289,8 +289,10 @@ let rec print_library_entry with_values ent = match ent with | (sp,Lib.Leaf lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >] - | (_,Lib.OpenedSection (str,_)) -> + | (_,Lib.OpenedSection str) -> [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >] + | (_,Lib.ClosedSection (str,_)) -> + [< 'sTR(" >>>>>>> Closed Section " ^ str); 'fNL >] | (_,Lib.Module str) -> [< 'sTR(" >>>>>>> Module " ^ str); 'fNL >] | (_,Lib.FrozenState _) -> @@ -386,6 +388,8 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name = | (_, (Lib.OpenedSection _ | Lib.FrozenState _ | Lib.Module _))::rest -> crible_rec rest + | (_, Lib.ClosedSection _) :: rest -> + crible_rec rest | [] -> () in try @@ -400,7 +404,7 @@ let print_crible name = let read_sec_context sec = let rec get_cxt in_cxt = function - | ((sp,Lib.OpenedSection (str,_)) as hd)::rest -> + | ((sp,Lib.OpenedSection str) as hd)::rest -> if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 34cf69ac2..b114e1b54 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -75,8 +75,8 @@ let inh_app_fun env isevars j = (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *) let inh_tosort_force env isevars j = - let t,i1 = class_of1 env !isevars j.uj_type in try + let t,i1 = class_of1 env !isevars j.uj_type in let p = lookup_path_to_sort_from i1 in apply_pcoercion env p j t with Not_found -> @@ -85,20 +85,17 @@ let inh_tosort_force env isevars j = let inh_tosort env isevars j = let typ = whd_betadeltaiota env !isevars j.uj_type in match typ with - | DOP0(Sort(_)) -> j (* idem inh_app_fun *) + | DOP0(Sort _) -> j (* idem inh_app_fun *) | _ -> (try inh_tosort_force env isevars j with _ -> j) let inh_ass_of_j env isevars j = let typ = whd_betadeltaiota env !isevars j.uj_type in match typ with - | DOP0(Sort s) -> {body=j.uj_val;typ=s} + | DOP0(Sort s) -> + { body = j.uj_val; typ = s } | _ -> - (try - let j1 = inh_tosort_force env isevars j in - assumption_of_judgment env !isevars j1 - with _ -> - error_assumption CCI env (nf_ise1 !isevars j.uj_val)) - (* try ... with _ -> ... is BAD *) + let j1 = inh_tosort_force env isevars j in + assumption_of_judgment env !isevars j1 let inh_coerce_to1 env isevars c1 v t k = let t1,i1 = class_of1 env !isevars c1 in diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index c510299ac..1c80cdb9f 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -17,12 +17,13 @@ val inh_tosort_force : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment val inh_tosort : env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -val inh_ass_of_j : env -> 'a evar_defs -> - unsafe_judgment -> typed_type -val inh_coerce_to : env -> 'a evar_defs -> - constr -> unsafe_judgment -> unsafe_judgment -val inh_cast_rel : env -> 'a evar_defs -> - unsafe_judgment -> unsafe_judgment -> unsafe_judgment +val inh_ass_of_j : + env -> 'a evar_defs -> unsafe_judgment -> typed_type +val inh_coerce_to : + env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment +val inh_cast_rel : + env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment + val inh_apply_rel_list : bool -> env -> 'a evar_defs -> unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) -> unsafe_judgment diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 53bcbc8ce..2f0757412 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -77,11 +77,11 @@ let split_evar_to_arrow sigma c = let prod = prod_create nevenv (incast_type dom, subst_var nvar (body_of_type rng)) in let sigma3 = Evd.define sigma2 ev prod in - let dsp = path_of_const (body_of_type dom) in - let rsp = path_of_const (body_of_type rng) in + let dsp = num_of_evar (body_of_type dom) in + let rsp = num_of_evar (body_of_type rng) in (sigma3, - mkCast (mkConst (dsp,args)) dummy_sort, - mkCast (mkConst (rsp,array_cons (mkRel 1) args)) dummy_sort) + mkCast (mkEvar dsp args) dummy_sort, + mkCast (mkEvar rsp (array_cons (mkRel 1) args)) dummy_sort) (* Redefines an evar with a smaller context (i.e. it may depend on less @@ -193,7 +193,7 @@ let real_clean isevars sp args rhs = | DLAM(n,a) -> DLAM(n, subs (k+1) a) | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v) in let body = subs 0 rhs in - if not (closed0 body) then error_not_clean CCI empty_env sp body; + (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *) body @@ -303,7 +303,7 @@ let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) = else match (ise_undefined isevars t1, ise_undefined isevars t2) with | (true,true) -> - if path_of_const t1 = path_of_const t2 then + if num_of_evar t1 = num_of_evar t2 then solve_refl conv_algo isevars t1 t2 else if Array.length(args_of_const t1) < Array.length(args_of_const t2) then diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1854e7eeb..4ce29088d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -509,8 +509,10 @@ let ise_resolve_nocheck sigma metamap env c = let ise_resolve1 is_ass sigma env c = - if is_ass then body_of_type (ise_resolve_type true sigma [] env c) - else (ise_resolve true sigma [] env c).uj_val + if is_ass then + body_of_type (ise_resolve_type true sigma [] env c) + else + (ise_resolve true sigma [] env c).uj_val (* Keeping universe constraints *) (* diff --git a/states/.cvsignore b/states/.cvsignore index ffd00ec56..ccc79cdf7 100644 --- a/states/.cvsignore +++ b/states/.cvsignore @@ -1 +1,2 @@ barestate.coq +initial.coq diff --git a/states/MakeInitial.v b/states/MakeInitial.v new file mode 100644 index 000000000..73ad27a0d --- /dev/null +++ b/states/MakeInitial.v @@ -0,0 +1,4 @@ +Require Prelude. +Require Logic_Type. +Require Logic_TypeSyntax. +Require Equality. diff --git a/tactics/Equality.v b/tactics/Equality.v new file mode 100644 index 000000000..9d6d34370 --- /dev/null +++ b/tactics/Equality.v @@ -0,0 +1,178 @@ + +(* $Id$: *) + +Declare ML Module "equality". + +Grammar vernac orient_rule:= + lr ["LR"] -> ["LR"] + |rl ["RL"] -> ["RL"] +with rule_list: List := + single_rlt [ constrarg($com) orient_rule($ort) ] -> + [(VERNACARGLIST $com $ort)] + |recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] -> + [(VERNACARGLIST $com $ort) ($LIST $tail)] +with base_list: List := + single_blt [identarg($rbase) "[" rule_list($rlt) "]"] -> + [(VERNACARGLIST $rbase ($LIST $rlt))] + |recursive_blt [identarg($rbase) "[" rule_list($rlt) "]" + base_list($blt)] -> + [(VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt)] +with vernac:= + addrule ["HintRewrite" base_list($blt) "."] -> + [(HintRewrite ($LIST $blt))]. + +Grammar tactic list_tactics: List := + single_lt [tactic($tac)] -> [$tac] + |recursive_lt [tactic($tac) "|" list_tactics($tail)] -> + [$tac ($LIST $tail)] + +with step_largs: List := + nil_step [] -> [] + |solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))] + |use_step ["with" "Use"] -> [(REDEXP (Use))] + |all_step ["with" "All"] -> [(REDEXP (All))] + +with rest_largs: List := + nil_rest [] -> [] + |solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))] + |cond_rest ["with" "Cond"] -> [(REDEXP (Cond))] + +with autorew_largs: List := + step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] -> + [(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)] + |rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] -> + [(REDEXP (Rest ($LIST $ltac))) ($LIST $llargs)] + |depth_arg ["Depth" "=" numarg($dth)] -> + [(REDEXP (Depth $dth))] + +with list_args_autorew: List := + nil_laa [] -> [] + |recursive_laa [autorew_largs($largs) list_args_autorew($laa)] -> + [($LIST $largs) ($LIST $laa)] + +with hintbase_list: List := + nil_hintbase [] -> [] +| base_by_name [identarg($id) hintbase_list($tail)] -> + [ (REDEXP (ByName $id)) ($LIST $tail)] +| explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] -> + [(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ] + +with hintbase: List := + onehint_lr [ comarg($c) "LR" ] -> [(REDEXP (LR $c))] +| onehint_rl [ comarg($c) "RL" ] -> [(REDEXP (RL $c))] +| conshint_lr [ comarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)] +| conshint_rl [ comarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)] + +with simple_tactic := + AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]" + list_args_autorew($laa)] -> + [(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))]. + +Grammar tactic simple_tactic := + replace [ "Replace" comarg($c1) "with" comarg($c2) ] -> [(Replace $c1 $c2)] + +| deqhyp [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)] +| deqconcl [ "Simplify_eq" ] -> [(DEqConcl)] + +| discr_id [ "Discriminate" identarg($id) ] -> [(DiscrHyp $id)] +| discr [ "Discriminate" ] -> [(Discr)] + +| inj [ "Injection" ] -> [(Inj)] +| inj_id [ "Injection" identarg($id) ] -> [(InjHyp $id)] + +| rewriteLR [ "Rewrite" "->" comarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))] +| rewriteRL [ "Rewrite" "<-" comarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))] +| rewrite [ "Rewrite" comarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))] + +| condrewriteLR [ "Conditional" tactic_com($tac) "Rewrite" "->" comarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))] +| condrewriteRL [ "Conditional" tactic_com($tac) "Rewrite" "<-" comarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))] +| condrewrite [ "Conditional" tactic_com($tac) "Rewrite" comarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))] + +| rewrite_in [ "Rewrite" comarg_binding_list($cl) "in" identarg($h) ] + -> [(RewriteLRin $h ($LIST $cl))] +| rewriteRL_in [ "Rewrite" "->" comarg_binding_list($cl) "in" identarg($h) ] + -> [(RewriteLRin $h ($LIST $cl))] +| rewriteLR_in [ "Rewrite" "<-" comarg_binding_list($cl) "in" identarg($h) ] + -> [(RewriteRLin $h ($LIST $cl))] + +| condrewriteLRin + [ "Conditional" tactic_com($tac) "Rewrite" "->" comarg_binding_list($cl) + "in" identarg($h) ] -> + [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))] +| condrewriteRLin + [ "Conditional" tactic_com($tac) "Rewrite" "<-" comarg_binding_list($cl) + "in" identarg($h)] -> + [(CondRewriteRLin (TACTIC $tac) $h ($LIST $cl))] +| condrewritein + [ "Conditional" tactic_com($tac) "Rewrite" comarg_binding_list($cl) "in" identarg($h) ] + -> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))] + +| DRewriteLR [ "Dependent" "Rewrite" "->" identarg($id) ] + -> [(SubstHypInConcl_LR $id)] +| DRewriteRL [ "Dependent" "Rewrite" "<-" identarg($id) ] + -> [(SubstHypInConcl_RL $id)] + +| cutrewriteLR [ "CutRewrite" "->" comarg($eqn) ] -> [(SubstConcl_LR $eqn)] +| cutrewriteLRin [ "CutRewrite" "->" comarg($eqn) "in" identarg($id) ] + -> [(SubstHyp_LR $eqn $id)] +| cutrewriteRL [ "CutRewrite" "<-" comarg($eqn) ] -> [(SubstConcl_RL $eqn)] +| cutrewriteRLin [ "CutRewrite" "<-" comarg($eqn) "in" identarg($id) ] + -> [(SubstHyp_RL $eqn $id)]. + +Syntax tactic level 0: + replace [(Replace $c1 $c2)] -> ["Replace " $c1 [1 1] "with " $c2] + +| deqhyp [(DEqHyp $id)] -> ["Simplify_eq " $id] +| deqconcl [(DEqConcl)] -> ["Simplify_eq"] + +| discr_id [(DiscrHyp $id)] -> ["Discriminate " $id] +| discr [(Discr)] -> ["Discriminate"] + +| inj [(Inj)] -> ["Injection"] +| inj_id [(InjHyp $id)] -> ["Injection " $id] + +| rewritelr [(RewriteLR $C ($LIST $bl))] -> ["Rewrite " $C (WITHBINDING ($LIST $bl))] +| rewriterl [(RewriteRL $C ($LIST $bl))] -> ["Rewrite <- " $C (WITHBINDING ($LIST $bl))] + +| condrewritelr [(CondRewriteLR (TACTIC $tac) $C ($LIST $bl))] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl))] +| condrewriterl [(CondRewriteRL (TACTIC $tac) $C ($LIST $bl))] -> ["Conditional " $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl))] + +| rewriteLR_in [(RewriteLRin $h $c ($LIST $bl))] -> ["Rewrite " $c (WITHBINDING ($LIST $bl)) [1 1] "in " $h] +| rewriteRL_in [(RewriteRLin $h $c ($LIST $bl))] -> ["Rewrite <- " $c (WITHBINDING ($LIST $bl)) [1 1]"in " $h] + +| condrewritelrin [(CondRewriteLRin (TACTIC $tac) $h $C ($LIST $bl))] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h] +| condrewriterlin [(CondRewriteRLin (TACTIC $tac) $h $C ($LIST $bl))] -> ["Conditional " $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h] + + +| DRewriteLR [(SubstHypInConcl_LR $id)] -> ["Dependent Rewrite -> " $id] +| DRewriteRL [(SubstHypInConcl_RL $id)] -> ["Dependent Rewrite <- " $id] + +| cutrewriteLR [(SubstConcl_LR $eqn)] -> ["CutRewrite -> " $eqn] +| cutrewriteLRin [(SubstHyp_LR $eqn $id)] + -> ["CutRewrite -> " $eqn:E [1 1]"in " $id] + +| cutrewriteRL [(SubstConcl_RL $eqn)] -> ["CutRewrite <- " $eqn:E] +| cutrewriteRLin [(SubstHyp_RL $eqn $id)] + -> ["CutRewrite <- " $eqn:E [1 1]"in " $id] +|nil_consbase [(CONSBASE)] -> [] +|single_consbase [(CONSBASE $tac)] -> [[1 0] $tac] +|nil_ortactic [(ORTACTIC)] -> [] +|single_ortactic [(ORTACTIC $tac)] -> ["|" $tac] +|AutoRewrite [(AutoRewrite $id)] -> ["AutoRewrite " $id] +|AutoRewriteBaseList [(REDEXP (BaseList $ft ($LIST $tl)))] -> + ["[" $ft (CONSBASE ($LIST $tl)) "]"] +|AutoRewriteStep [(REDEXP (Step $ft ($LIST $tl)))] -> + [[0 1] "Step=" "[" $ft (ORTACTIC ($LIST $tl)) "]"] +|AutoRewriteRest [(REDEXP (Rest $ft ($LIST $tl)))] -> + [[0 1] "Rest=" "[" $ft (ORTACTIC ($LIST $tl)) "]"] +|AutoRewriteSolveStep [(REDEXP (SolveStep))] -> ["with Solve"] +|AutoRewriteSolveRest [(REDEXP (SolveRest))] -> ["with Solve"] +|AutoRewriteUse [(REDEXP (Use))] -> ["with Use"] +|AutoRewriteAll [(REDEXP (All))] -> ["with All"] +|AutoRewriteCond [(REDEXP (Cond))] -> ["with Cond"] +|AutoRewriteDepth [(REDEXP (Depth $dth))] -> [[0 1] "Depth=" $dth] +|AutoRewriteByName [(REDEXP (ByName $id))] -> [ $id ] +|AutoRewriteExplicit [(REDEXP (Explicit $l))] -> ["[" $l "]"] +|AutoRewriteLR [(REDEXP (LR $c))] -> [ $c "LR" ] +|AutoRewriteRL [(REDEXP (RL $c))] -> [ $c "RL" ] +. diff --git a/tactics/equality.ml b/tactics/equality.ml new file mode 100644 index 000000000..0052cdfa1 --- /dev/null +++ b/tactics/equality.ml @@ -0,0 +1,2011 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Univ +open Generic +open Term +open Inductive +open Environ +open Reduction +open Instantiate +open Typeops +open Typing +open Tacmach +open Proof_trees +open Logic +open Wcclausenv +open Pattern +open Tacticals +open Tactics +open Tacinterp +open Tacred +open Vernacinterp + +(* Rewriting tactics *) + +(* Warning : rewriting from left to right only works + if there exists in the context a theorem named <eqname>_<suffsort>_r + with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y). + If another equality myeq is introduced, then corresponding theorems + myeq_ind_r, myeq_rec_r and myeq_rect_r have to be proven. See below. + -- Eduardo (19/8/97 +*) + +let general_rewrite_bindings lft2rgt (c,l) gl = + let ctype = pf_type_of gl c in + let env = pf_env gl in + let sigma = project gl in + let sign,t = splay_prod env sigma ctype in + match match_with_equation t with + | None -> error "The term provided does not end with an equation" + | Some (hdcncl,_) -> + let hdcncls = string_head hdcncl in + let elim = + if lft2rgt then + pf_global gl (id_of_string + (hdcncls^(suff gl (pf_concl gl))^"_r")) + else + pf_global gl (id_of_string (hdcncls^(suff gl (pf_concl gl)))) + in + tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl + (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal + and did not fail for useless conditional rewritings generating an + extra condition *) + +let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,[]) + +let rewriteLR_bindings = general_rewrite_bindings true +let rewriteRL_bindings = general_rewrite_bindings false + +let rewriteLR = general_rewrite true +let rewriteRL = general_rewrite false + +let dyn_rewriteLR = function + | [Command com; Bindings binds] -> + tactic_com_bind_list rewriteLR_bindings (com,binds) + | [Constr c; Cbindings binds] -> + rewriteLR_bindings (c,binds) + | _ -> assert false + +let dyn_rewriteRL = function + | [Command com; Bindings binds] -> + tactic_com_bind_list rewriteRL_bindings (com,binds) + | [Constr c; Cbindings binds] -> + rewriteRL_bindings (c,binds) + | _ -> assert false + +(* Replacing tactics *) + +(* eq,symeq : equality on Set and its symmetry theorem + eqt,sym_eqt : equality on Type and its symmetry theorem + c2 c1 : c1 is to be replaced by c2 + unsafe : If true, do not check that c1 and c2 are convertible + gl : goal *) + +let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl = + let t1 = pf_type_of gl c1 + and t2 = pf_type_of gl c2 in + if unsafe or (pf_conv_x gl t1 t2) then + let (e,sym) = + match hnf_type_of gl t1 with + | DOP0(Sort(Prop(Pos))) -> (eq,sym_eq) + | DOP0(Sort(Type(_))) -> (eqt,sym_eqt) + | _ -> error "replace" + in + (tclTHENL (elim_type (applist (e, [t1;c1;c2]))) + (tclORELSE assumption + (tclTRY (tclTHEN (apply sym) assumption)))) gl + else + error "terms does not have convertible types" + +(* Only for internal use *) +let unsafe_replace c2 c1 gl = + let eq = (pf_parse_const gl "eq") in + let eqt = (pf_parse_const gl "eqT") in + let sym_eq = (pf_parse_const gl "sym_eq") in + let sym_eqt = (pf_parse_const gl "sym_eqT") in + abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 true gl + +let replace c2 c1 gl = + let eq = (pf_parse_const gl "eq") in + let eqt = (pf_parse_const gl "eqT") in + let sym_eq = (pf_parse_const gl "sym_eq") in + let sym_eqt = (pf_parse_const gl "sym_eqT") in + abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 false gl + +let dyn_replace args gl = + match args with + | [(Command c1);(Command c2)] -> + replace (pf_constr_of_com gl c1) (pf_constr_of_com gl c2) gl + | [(Constr c1);(Constr c2)] -> + replace c1 c2 gl + | _ -> assert false + +let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR +let h_rewriteLR_bindings (c,bl) = v_rewriteLR [(Constr c);(Cbindings bl)] +let h_rewriteLR c = h_rewriteLR_bindings (c,[]) + +let v_rewriteRL = hide_tactic "RewriteRL" dyn_rewriteRL +let h_rewriteRL_bindings (c,bl) = v_rewriteRL [(Constr c);(Cbindings bl)] +let h_rewriteRL c = h_rewriteRL_bindings (c,[]) + +let v_replace = hide_tactic "Replace" dyn_replace +let h_replace c1 c2 = v_replace [(Constr c1);(Constr c2)] + +(* Conditional rewriting, the success of a rewriting is related + to the resolution of the conditions by a given tactic *) + +let conditional_rewrite lft2rgt tac (c,bl) = + tclTHEN_i (general_rewrite_bindings lft2rgt (c,bl)) + (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) 1 + +let dyn_conditional_rewrite lft2rgt = function + | [(Tacexp tac); (Command com);(Bindings binds)] -> + tactic_com_bind_list + (conditional_rewrite lft2rgt (Tacinterp.interp tac)) + (com,binds) + | [(Tacexp tac); (Constr c);(Cbindings binds)] -> + conditional_rewrite lft2rgt (Tacinterp.interp tac) (c,binds) + | _ -> assert false + +let v_conditional_rewriteLR = + hide_tactic "CondRewriteLR" (dyn_conditional_rewrite true) + +let v_conditional_rewriteRL = + hide_tactic "CondRewriteRL" (dyn_conditional_rewrite false) + +(* End of Eduardo's code. The rest of this file could be improved + using the functions match_with_equation, etc that I defined + in Pattern.ml. + -- Eduardo (19/8/97) +*) + +(* Tactics for equality reasoning with the "eq" or "eqT" + relation This code will work with any equivalence relation which + is substitutive *) + +let find_constructor env sigma c = + match whd_betadeltaiota_stack env sigma c [] with + | DOPN(MutConstruct _,_) as hd,stack -> (hd,stack) + | _ -> error "find_constructor" + +type leibniz_eq = { + eq : marked_term; + ind : marked_term; + rrec : marked_term option; + rect : marked_term option; + congr: marked_term; + sym : marked_term } + +let mmk = make_module_marker + [ "#Prelude.obj"; "#Logic_Type.obj"; "#Specif.obj"; + "#Logic.obj"; "#Core.obj"] + +let eq_pattern = put_pat mmk "(eq ? ? ?)" +let not_pattern = put_pat mmk "(not ?)" +let imp_False_pattern = put_pat mmk "? -> False" + +let pat_True = put_pat mmk "True" +let pat_False = put_pat mmk "False" +let pat_I = put_pat mmk "I" + +let eq= { eq = put_pat mmk "eq"; + ind = put_pat mmk "eq_ind" ; + rrec = Some (put_pat mmk "eq_rec"); + rect = Some (put_pat mmk "eq_rect"); + congr = put_pat mmk "f_equal" ; + sym = put_pat mmk "sym_eq" } + +let eqT_pattern = put_pat mmk "(eqT ? ? ?)" + +let eqT= { eq = put_pat mmk "eqT"; + ind = put_pat mmk "eqT_ind" ; + rrec = None; + rect = None; + congr = put_pat mmk "congr_eqT" ; + sym = put_pat mmk "sym_eqT" } + +let idT_pattern = put_pat mmk "(identityT ? ? ?)" + +let idT = { eq = put_pat mmk "identityT"; + ind = put_pat mmk "identityT_ind" ; + rrec = Some (put_pat mmk "identityT_rec") ; + rect = Some (put_pat mmk "identityT_rect"); + congr = put_pat mmk "congr_idT" ; + sym = put_pat mmk "sym_idT" } + +let pat_EmptyT = put_pat mmk "EmptyT" +let pat_UnitT = put_pat mmk "UnitT" +let pat_IT = put_pat mmk "IT" +let notT_pattern = put_pat mmk "(notT ?)" + +let rec hd_of_prod prod = + match strip_outer_cast prod with + | (DOP2(Prod,c,DLAM(n,t'))) -> hd_of_prod t' + | t -> t + +type elimination_types = + | Set_Type + | Type_Type + | Set_SetorProp + | Type_SetorProp + +let necessary_elimination sort_arity sort = + if (is_Type sort) then + if is_Set sort_arity then + Set_Type + else + if is_Type sort_arity then + Type_Type + else + errorlabstrm "necessary_elimination" + [< 'sTR "no primitive equality on proofs" >] + else + if is_Set sort_arity then + Set_SetorProp + else + if is_Type sort_arity then + Type_SetorProp + else errorlabstrm "necessary_elimination" + [< 'sTR "no primitive equality on proofs" >] + +let find_eq_pattern arity sort = + let mt = + match necessary_elimination (hd_of_prod arity) sort with + | Set_Type -> eq.eq + | Type_Type -> idT.eq + | Set_SetorProp -> eq.eq + | Type_SetorProp -> eqT.eq + in + get_pat mt + +(* [find_positions t1 t2] + + will find the positions in the two terms which are suitable for + discrimination, or for injection. Obviously, if there is a + position which is suitable for discrimination, then we want to + exploit it, and not bother with injection. So when we find a + position which is suitable for discrimination, we will just raise + an exception with that position. + + So the algorithm goes like this: + + if [t1] and [t2] start with the same constructor, then we can + continue to try to find positions in the arguments of [t1] and + [t2]. + + if [t1] and [t2] do not start with the same constructor, then we + have found a discrimination position + + if one [t1] or [t2] do not start with a constructor and the two + terms are not already convertible, then we have found an injection + position. + + A discriminating position consists of a constructor-path and a pair + of operators. The constructor-path tells us how to get down to the + place where the two operators, which must differ, can be found. + + An injecting position has two terms instead of the two operators, + since these terms are different, but not manifestly so. + + A constructor-path is a list of pairs of (operator * int), where + the int (based at 0) tells us which argument of the operator we + descended into. + + *) + +exception DiscrFound of (sorts oper * int) list * sorts oper * sorts oper + +let find_positions env sigma t1 t2 = + let rec findrec posn t1 t2 = + match (whd_betadeltaiota_stack env sigma t1 [], + whd_betadeltaiota_stack env sigma t2 []) with + + | ((DOPN(MutConstruct _ as oper1,_) as hd1,args1), + (DOPN(MutConstruct _ as oper2,_) as hd2,args2)) -> + (* both sides are constructors, so either we descend, or we can + discriminate here. *) + if oper1 = oper2 then + List.flatten (list_map2_i (fun i arg1 arg2 -> + findrec ((oper1,i)::posn) arg1 arg2) + 0 args1 args2) + else + raise (DiscrFound(List.rev posn,oper1,oper2)) + + | (t1_0,t2_0) -> + let t1_0 = applist t1_0 + and t2_0 = applist t2_0 in + if is_conv env sigma t1_0 t2_0 then + [] + else + (match whd_castapp ((unsafe_machine env sigma t1_0).uj_kind) with + | DOP0(Sort(Prop Pos)) -> + [(List.rev posn,t1_0,t2_0)] (* Set *) + | DOP0(Sort(Type(_))) -> + [(List.rev posn,t1_0,t2_0)] (* Type *) + | _ -> []) + in + (try + Inr(findrec [] t1 t2) + with DiscrFound (x_0,x_1,x_2) -> + Inl (x_0,x_1,x_2)) + +let discriminable env sigma t1 t2 = + match find_positions env sigma t1 t2 with + | Inl _ -> true + | _ -> false + +(* Once we have found a position, we need to project down to it. If + we are discriminating, then we need to produce False on one of the + branches of the discriminator, and True on the other one. So the + result type of the case-expressions is always Prop. + + If we are injecting, then we need to discover the result-type. + This can be difficult, since the type of the two terms at the + injection-position can be different, and we need to find a + dependent sigma-type which generalizes them both. + + We can get an approximation to the right type to choose by: + + (0) Before beginning, we reserve a metavariable for the default + value of the match, to be used in all the bogus branches. + + (1) perform the case-splits, down to the site of the injection. At + each step, we have a term which is the "head" of the next + case-split. At the point when we actually reach the end of our + path, the "head" is the term to return. We compute its type, and + then, backwards, make a sigma-type with every free debruijn + reference in that type. We can be finer, and first do a S(TRONG)NF + on the type, so that we get the fewest number of references + possible. + + (2) This gives us a closed type for the head, which we use for the + types of all the case-splits. + + (3) Now, we can compute the type of one of T1, T2, and then unify + it with the type of the last component of the result-type, and this + will give us the bindings for the other arguments of the tuple. + + *) + +(* The algorithm, then is to perform successive case-splits. We have + the result-type of the case-split, and also the type of that + result-type. We have a "direction" we want to follow, i.e. a + constructor-number, and in all other "directions", we want to juse + use the default-value. + + After doing the case-split, we call the afterfun, with the updated + environment, to produce the term for the desired "direction". + + The assumption is made here that the result-type is not manifestly + functional, so we can just use the length of the branch-type to + know how many lambda's to stick in. + + *) + +(* [descend_then sigma env head dirn] + + returns the number of products introduced, and the environment + which is active, in the body of the case-branch given by [dirn], + along with a continuation, which expects to be fed: + + (1) the value of the body of the branch given by [dirn] + (2) the default-value + + (3) the type of the default-value, which must also be the type of + the body of the [dirn] branch + + the continuation then constructs the case-split. + *) + +let descend_then sigma env head dirn = + let headj = unsafe_machine env sigma head in + let (construct,largs,nparams,arityind,mind, + consnamev,case_fun,type_branch_fun) = + (match whd_betadeltaiota_stack env sigma headj.uj_type [] with + | (DOPN(MutInd (x_0,x_1),cl) as ity,largs) -> + let mispec = Global.lookup_mind_specif ((x_0,x_1),cl) in + let nparams = mis_nparams mispec + and consnamev = mis_consnames mispec + and arity = mis_arity mispec in + (DOPN(MutConstruct((x_0,x_1),dirn),cl),largs,nparams, + mis_arity mispec,ity,consnamev,mkMutCase, + type_case_branches env sigma) + | _ -> assert false) + in + let (globargs,largs) = list_chop nparams largs in + let dirn_cty = + strong (fun _ _ -> whd_castapp) env sigma + (type_of env sigma (applist(construct,globargs))) in + let dirn_nlams = nb_prod dirn_cty in + let (_,dirn_env) = add_prods_rel sigma (dirn_cty,env) in + (dirn_nlams, + dirn_env, + (fun dirnval (dfltval,resty) -> + let nconstructors = Array.length consnamev in + let arity = + hnf_prod_applist env sigma "discriminate" arityind globargs in + let p = lambda_ize (nb_prod arity) arity resty in + let nb_prodP = nb_prod p in + let (_,bty,_) = + type_branch_fun (DOP2(Cast,headj.uj_type,headj.uj_kind)) + (type_of env sigma p) p head in + let build_branch i = + let result = if i = dirn then dirnval else dfltval in + let nlams = nb_prod bty.(i-1) in + let typstack,_,_ = + push_and_liftl (nlams-nb_prodP) [] bty.(i-1) [] in + let _,branchval,_ = + lam_and_popl_named (nlams-nb_prodP) typstack result [] in + branchval + in + case_fun (ci_of_mind mind) p head + (List.map build_branch (interval 1 nconstructors)))) + +(* Now we need to construct the discriminator, given a discriminable + position. This boils down to: + + (1) If the position is directly beneath us, then we need to do a + case-split, with result-type Prop, and stick True and False into + the branches, as is convenient. + + (2) If the position is not directly beneath us, then we need to + call descend_then, to descend one step, and then recursively + construct the discriminator. + + *) + +let necessary_elimination arity sort = + let ty = hd_of_prod arity in + if is_Type sort then + if is_Set ty then + Set_Type + else + if is_Type ty then + Type_Type + else + errorlabstrm "necessary_elimination" + [< 'sTR "no primitive equality on proofs" >] + else + if is_Set ty then + Set_SetorProp + else + if is_Type ty then + Type_SetorProp + else + errorlabstrm "necessary_elimination" + [< 'sTR "no primitive equality on proofs" >] + +(* [construct_discriminator env dirn headval] + constructs a case-split on [headval], with the [dirn]-th branch + giving [True], and all the rest giving False. *) + +let construct_discriminator sigma env dirn c sort= + let t = type_of env sigma c in + let (largs,nparams,arityind,mind,consnamev,case_fun,type_branch_fun) = + (match whd_betadeltaiota_stack env sigma t [] with + | (DOPN(MutInd (x_0,x_1),cl) as ity,largs) -> + let mispec = Global.lookup_mind_specif ((x_0,x_1),cl) in + let nparams = mis_nparams mispec + and consnamev = mis_consnames mispec + and arity = mis_arity mispec in + (largs,nparams,mis_arity mispec,ity,consnamev,mkMutCase, + type_case_branches env sigma) + | _ -> (* one can find Rel(k) in case of dependent constructors + like T := c : (A:Set)A->T and a discrimination + on (c bool true) = (c bool false) + CP : changed assert false in a more informative error + *) + errorlabstrm "Equality.construct_discriminator" + [< 'sTR "Cannot discriminate on inductive constructors with + dependent types" >]) + in + let nconstructors = Array.length consnamev in + let (globargs,largs) = list_chop nparams largs in + let arity = + hnf_prod_applist env sigma "construct_discriminator" arityind globargs in + let (true_0,false_0,sort_0) = + match necessary_elimination (hd_of_prod arity) sort with + | Type_Type -> + get_pat pat_UnitT, get_pat pat_EmptyT, + (DOP0(Sort (Type(dummy_univ)))) + | _ -> + get_pat pat_True, get_pat pat_False, (DOP0(Sort (Prop Null))) + in + let eq = find_eq_pattern arity sort in + let p = lambda_ize (nb_prod arity) arity sort_0 in + let (_,bty,_) = type_branch_fun (DOP2(Cast,t,type_of env sigma t)) + (type_of env sigma p) p c in + let build_branch i = + let nlams = nb_prod bty.(i-1) in + let endpt = if i = dirn then true_0 else false_0 in + lambda_ize nlams bty.(i-1) endpt + in + let build_match () = + case_fun (ci_of_mind mind) p c + (List.map build_branch (interval 1 nconstructors)) + in + build_match() + +let rec build_discriminator sigma env dirn c sort = function + | [] -> construct_discriminator sigma env dirn c sort + | (MutConstruct(sp,cnum),argnum)::l -> + let cty = type_of env sigma c in + let (ity,_) = find_mrectype env sigma cty in + let arity = Global.mind_arity ity in + let nparams = Global.mind_nparams ity in + let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in + let newc = Rel(cnum_nlams-(argnum-nparams)) in + let subval = build_discriminator sigma cnum_env dirn newc sort l in + (match necessary_elimination (hd_of_prod arity) sort with + | Type_Type -> + kont subval (get_pat pat_EmptyT,DOP0(Sort(Type(dummy_univ)))) + | _ -> kont subval (get_pat pat_False,DOP0(Sort(Prop Null)))) + | _ -> assert false + +let dest_somatch_eq eqn eq_pat = + match dest_somatch eqn eq_pat with + | [t;x;y] -> (t,x,y) + | _ -> anomaly "dest_somatch_eq: an eq pattern should match 3 terms" + +let find_eq_data_decompose eqn = + if (somatches eqn eq_pattern) then + (eq, dest_somatch_eq eqn eq_pattern) + else if (somatches eqn eqT_pattern) then + (eqT, dest_somatch_eq eqn eqT_pattern) + else if (somatches eqn idT_pattern) then + (idT, dest_somatch_eq eqn idT_pattern) + else + errorlabstrm "find_eq_data_decompose" [< >] + +let gen_absurdity id gl = + if (matches gl (clause_type (Some id) gl) pat_False) + or (matches gl (clause_type (Some id) gl) pat_EmptyT) + then + simplest_elim (VAR id) gl + else + errorlabstrm "Equality.gen_absurdity" + [< 'sTR "Not the negation of an equality" >] + +(* Precondition: eq is leibniz equality + + returns ((eq_elim t t1 P i t2), absurd_term) + where P=[e:t][h:(t1=e)]discrimator + absurd_term=EmptyT if the necessary elimination is Type_Tyoe + + and P=[e:t][h[e:t]discriminator + absurd_term=Fale if the necessary eliination is Type_ProporSet + or Set_ProporSet +*) + +let discrimination_pf e (t,t1,t2) discriminator lbeq gls = + let env = pf_env gls in + let (indt,_) = find_mrectype env (project gls) t in + let arity = Global.mind_arity indt in + let sort = pf_type_of gls (pf_concl gls) in + match necessary_elimination (hd_of_prod arity) sort with + | Type_Type -> + let rect = match lbeq.rect with Some x -> x | _ -> assert false in + let eq_elim = get_pat rect in + let eq_term = get_pat lbeq.eq in + let i = get_pat pat_IT in + let absurd_term = get_pat pat_EmptyT in + let h = pf_get_new_id (id_of_string "HH")gls in + let pred= mkNamedLambda e t + (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) + discriminator) + in (applist(eq_elim, [t;t1;pred;i;t2]), absurd_term) + + | _ -> + let i = get_pat pat_I in + let absurd_term = get_pat pat_False in + let eq_elim = get_pat lbeq.ind in + (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), + absurd_term) + +let discr id gls = + let eqn = (pf_whd_betadeltaiota gls (clause_type (Some id) gls)) in + let sort = pf_type_of gls (pf_concl gls) in + let (lbeq,(t,t1,t2)) = + try + find_eq_data_decompose eqn + with e when catchable_exception e -> + errorlabstrm "Discriminate" + [<'sTR (string_of_id id); 'sTR" Not a discriminable equality">] + in + let tj = pf_execute gls t in + let sigma = project gls in + let env = pf_env gls in + (match find_positions env sigma t1 t2 with + | Inr _ -> + errorlabstrm "Discr" + [< 'sTR (string_of_id id); 'sTR" Not a discriminable equality" >] + + | Inl(cpath,MutConstruct(_,dirn),_) -> + let e = pf_get_new_id (id_of_string "ee") gls in + let e_env = + push_var (e,assumption_of_judgment env sigma tj) env + in + let discriminator = + build_discriminator sigma e_env dirn (VAR e) sort cpath in + let (indt,_) = find_mrectype env sigma t in + let arity = Global.mind_arity indt in + let (pf, absurd_term) = + discrimination_pf e (t,t1,t2) discriminator lbeq gls + in + tclCOMPLETE((tclTHENS (cut_intro absurd_term) + ([onLastHyp (compose gen_absurdity out_some); + refine (mkAppL [| pf; VAR id |])]))) gls + | _ -> assert false) + +let not_found_message id = + [<'sTR "the variable"; 'sPC ; 'sTR (string_of_id id) ; 'sPC; + 'sTR" was not found in the current environment" >] + +let insatisfied_prec_message cls = + match cls with + | None -> [< 'sTR"goal does not satify the expected preconditions">] + | Some id -> [< 'sTR(string_of_id id); 'sPC; + 'sTR"does not satify the expected preconditions" >] + +let discrClause cls gls = + match cls with + | None -> + if somatches (pf_concl gls) not_pattern then + (tclTHEN (tclTHEN hnf_in_concl intro) + (onLastHyp (compose discr out_some))) gls + else if somatches (pf_concl gls) imp_False_pattern then + (tclTHEN intro (onLastHyp (compose discr out_some))) gls + else + errorlabstrm "DiscrClause" (insatisfied_prec_message cls) + | Some id -> + try (discr id gls) + with Not_found -> errorlabstrm "DiscrClause" (not_found_message id) + +let discrEverywhere = Tacticals.tryAllClauses discrClause +let discrConcl gls = discrClause None gls +let discrHyp id gls = discrClause (Some id) gls + +(**) +let h_discr = hide_atomic_tactic "Discr" discrEverywhere +let h_discrConcl = hide_atomic_tactic "DiscrConcl" discrConcl +let h_discrHyp = hide_ident_tactic "DiscrHyp" discrHyp +(**) + +(* [bind_ith na i T] + * will verify that T has no binders below [Rel i], and produce the + * term [na]T, binding [Rel i] in T. The resulting term should be + * valid in the same environment as T, which means that we have to + * re-lift it. *) + +let bind_ith na i t = lift i (DLAM(na,lift (-(i-1)) t)) + +let existS_term = put_pat mmk "existS" +let existS_pattern = put_pat mmk "(existS ? ? ? ?)" +let sigS_term = put_pat mmk "sigS" +let projS1_term = put_pat mmk "projS1" +let projS2_term = put_pat mmk "projS2" +let sigS_rec_term = put_pat mmk "sigS_rec" + +let existT_term = put_pat mmk "existT" +let existT_pattern = put_pat mmk "(existT ? ? ? ?)" +let sigT_term = put_pat mmk "sigT" +let projT1_term = put_pat mmk "projT1" +let projT2_term = put_pat mmk "projT2" +let sigT_rect_term = put_pat mmk "sigT_rect" + +(* returns the sigma type (sigS, sigT) with the respective + constructor depending on the sort *) + +let find_sigma_data s = + match strip_outer_cast s with + | DOP0(Sort(Prop Pos)) -> (* Set *) + (projS1_term,projS2_term,sigS_rec_term,existS_term, sigS_term) + | DOP0(Sort(Type(_))) -> (* Type *) + (projT1_term, projT2_term, sigT_rect_term, existT_term, sigT_term) + | _ -> error "find_sigma_data" + +(* [make_tuple env na lind rterm rty] + + If [rty] depends on lind, then we will fabricate the term + + (existS A==[type_of(Rel lind)] P==(Lambda(type_of(Rel lind), + [bind_ith na lind rty])) + [(Rel lind)] [rterm]) + + [The term (Lambda(type_of(Rel lind),[bind_ith na lind rty])) is + valid in [env] because [bind_ith] produces a term which does not + "change" environments.] + + which should have type (sigS A P) - we can verify it by + typechecking at the end. + *) + +let make_tuple sigma env na lind rterm rty = + if dependent (Rel lind) rty then + let (_,_,_,exist_term,sig_term) = + find_sigma_data (type_of env sigma rty) in + let a = type_of env sigma (Rel lind) in + let p = DOP2(Lambda,a, + bind_ith (fst(lookup_rel lind env)) lind rty) in + (applist(get_pat exist_term,[a;p;(Rel lind);rterm]), + applist(get_pat sig_term,[a;p])) + else + (rterm,rty) + +(* check that the free-references of the type of [c] are contained in + the free-references of the normal-form of that type. If the normal + form of the type contains fewer references, we want to return that + instead. *) + +let minimal_free_rels env sigma (c,cty) = + let cty_rels = free_rels cty in + let nf_cty = nf_betadeltaiota env sigma cty in + let nf_rels = free_rels nf_cty in + if Intset.subset cty_rels nf_rels then + (cty,cty_rels) + else + (nf_cty,nf_rels) + +(* [sig_clausale_forme siglen ty] + + Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the + type of ty), and return: + + (1) a pattern, with meta-variables in it for various arguments, + which, when the metavariables are replaced with appropriate + terms, will have type [ty] + + (2) an integer, which is the last argument - the one which we just + returned. + + (3) a pattern, for the type of that last meta + + (4) a typing for each metavariable + + WARNING: No checking is done to make sure that the + sigS(or sigT)'s are actually there. + - Only homogenious pairs are built i.e. pairs where all the + dependencies are of the same sort + *) + +let sig_clausale_forme env sigma sort_of_ty siglen ty = + let (_,_,_,exist_term,_) = find_sigma_data sort_of_ty in + let rec sigrec_clausale_forme siglen ty = + if siglen = 0 then + let mv = new_meta() in + (DOP0(Meta mv),(mv,ty),[(mv,ty)]) + else + let (a,p) = match whd_stack env sigma (whd_beta env sigma ty) [] with + | (_,[a;p]) -> (a,p) + | _ -> anomaly "sig_clausale_forme: should be a sigma type" in + let mv = new_meta() in + let rty = applist(p,[DOP0(Meta mv)]) in + let (rpat,headinfo,mvenv) = sigrec_clausale_forme (siglen-1) rty in + (applist(get_pat exist_term,[a;p;DOP0(Meta mv);rpat]), + headinfo, + (mv,a)::mvenv) + in + sigrec_clausale_forme siglen ty + +(* [make_iterated_tuple sigma env DFLT c] + + Will find the free (DB) references of the S(TRONG)NF of [c]'s type, + gather them together in left-to-right order (i.e. highest-numbered + is farthest-left), and construct a big iterated pair out of it. + This only works when the references are all themselves to members + of [Set]s, because we use [sigS] to construct the tuple. + + Suppose now that our constructed tuple is of length [tuplen]. + + Then, we need to construct the default value for the other + branches. The default value is constructed by taking the + tuple-type, exploding the first [tuplen] [sigS]'s, and replacing at + each step the binder in the right-hand-type by a fresh + metavariable. + + In addition, on the way back out, we will construct the pattern for + the tuple which uses these meta-vars. + + This gives us a pattern, which we use to match against the type of + DFLT; if that fails, then against the S(TRONG)NF of that type. If + both fail, then we just cannot construct our tuple. If one of + those succeed, then we can construct our value easily - we just use + the tuple-pattern. + + *) + +let make_iterated_tuple sigma env (dFLT,dFLTty) (c,cty) = + let (cty,rels) = minimal_free_rels env sigma (c,cty) in + let sort_of_cty = type_of env sigma cty in + let sorted_rels = Sort.list (>=) (Intset.elements rels) in + let (tuple,tuplety) = + List.fold_left (fun (rterm,rty) lind -> + let na = fst(lookup_rel lind env) in + make_tuple sigma env na lind rterm rty) + (c,cty) + sorted_rels + in + if not(closed0 tuplety) then failwith "make_iterated_tuple"; + let (tuplepat,(headmv,headpat),mvenv) = + sig_clausale_forme env sigma sort_of_cty (List.length sorted_rels) + tuplety + in + let headpat = nf_betadeltaiota env sigma headpat in + let nf_ty = nf_betadeltaiota env sigma dFLTty in + let dfltval = + list_try_find + (fun ty -> + try + let binding = + if is_Type headpat & is_Type ty then + [] + else + somatch None headpat ty + in + instance ((headmv,dFLT)::binding) env sigma tuplepat + with e when catchable_exception e -> failwith "caught") + [dFLTty; nf_ty] + in + (tuple,tuplety,dfltval) + +let rec build_injrec sigma env (t1,t2) c = function + | [] -> + make_iterated_tuple sigma env (t1,type_of env sigma t1) + (c,type_of env sigma c) + | (MutConstruct(sp,cnum),argnum)::l -> + let cty = type_of env sigma c in + let (ity,_) = find_mrectype env sigma cty in + let nparams = Global.mind_nparams ity in + let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in + let newc = Rel(cnum_nlams-(argnum-nparams)) in + let (subval,tuplety,dfltval) = + build_injrec sigma cnum_env (t1,t2) newc l + in + (kont subval (dfltval,tuplety), + tuplety,dfltval) + | _ -> assert false + +let build_injector sigma env (t1,t2) c cpath = + let (injcode,resty,_) = build_injrec sigma env (t1,t2) c cpath in + (injcode,resty) + +let try_delta_expand env sigma t = + let whdt = whd_betadeltaiota env sigma t in + let rec hd_rec c = + match c with + | DOPN(MutConstruct _,_) -> whdt + | DOPN(AppL,cl) -> hd_rec (array_hd cl) + | DOP2(Cast,c,_) -> hd_rec c + | _ -> t + in + hd_rec whdt + +(* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it + expands then only when the whdnf has a constructor of an inductive type + in hd position, otherwise delta expansion is not done *) + +let inj id gls = + let eqn = (pf_whd_betadeltaiota gls (clause_type (Some id) gls)) in + let (eq,(t,t1,t2))= + try + find_eq_data_decompose eqn + with e when catchable_exception e -> + errorlabstrm "Inj" [<'sTR(string_of_id id); + 'sTR" Not a primitive equality here " >] + in + let tj = pf_execute gls t in + let sigma = project gls in + let env = pf_env gls in + match find_positions env sigma t1 t2 with + | Inl _ -> + errorlabstrm "Inj" [<'sTR (string_of_id id); + 'sTR" is not a projectable equality" >] + | Inr posns -> + let e = pf_get_new_id (id_of_string "e") gls in + let e_env = + push_var (e,assumption_of_judgment env sigma tj) env + in + let injectors = + map_succeed + (fun (cpath,t1_0,t2_0) -> + let (injbody,resty) = + build_injector sigma e_env (t1_0,t2_0) (VAR e) cpath in + let injfun = mkNamedLambda e t injbody in + try + let _ = type_of env sigma injfun in (injfun,resty) + with e when catchable_exception e -> failwith "caught") + posns + in + if injectors = [] then + errorlabstrm "Equality.inj" + [<'sTR "Failed to decompose the equality">]; + tclMAP + (fun (injfun,resty) -> + let pf = applist(get_pat eq.congr, + [t;resty;injfun; + try_delta_expand env sigma t1; + try_delta_expand env sigma t2; + VAR id]) + in + let ty = pf_type_of gls pf in + ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) + injectors + gls + +let injClause cls gls = + match cls with + | None -> + if somatches (pf_concl gls) not_pattern then + (tclTHEN (tclTHEN hnf_in_concl intro) + (onLastHyp (compose inj out_some))) gls + else + errorlabstrm "InjClause" (insatisfied_prec_message cls) + | Some id -> + try + inj id gls + with + | Not_found -> + errorlabstrm "InjClause" (not_found_message id) + | UserError("refiner__FAIL",_) -> + errorlabstrm "InjClause" + [< 'sTR (string_of_id id); 'sTR" Not a projectable equality" >] + +let injConcl gls = injClause None gls +let injHyp id gls = injClause (Some id) gls + +(**) +let h_injConcl = hide_atomic_tactic "Inj" injConcl +let h_injHyp = hide_ident_tactic "InjHyp" injHyp +(**) + +let decompEqThen ntac id gls = + let eqn = (pf_whd_betadeltaiota gls (clause_type (Some id) gls)) in + let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in + let sort = pf_type_of gls (pf_concl gls) in + let tj = pf_execute gls t in + let sigma = project gls in + let env = pf_env gls in + (match find_positions env sigma t1 t2 with + | Inl(cpath,MutConstruct(_,dirn),_) -> + let e = pf_get_new_id (id_of_string "e") gls in + let e_env = + push_var (e,assumption_of_judgment env sigma tj) env in + let discriminator = + build_discriminator sigma e_env dirn (VAR e) sort cpath in + let (pf, absurd_term) = + discrimination_pf e (t,t1,t2) discriminator lbeq gls in + tclCOMPLETE + ((tclTHENS (cut_intro absurd_term) + ([onLastHyp (compose gen_absurdity out_some); + refine (mkAppL [| pf; VAR id |])]))) gls + | Inr posns -> + (let e = pf_get_new_id (id_of_string "e") gls in + let e_env = + push_var (e,assumption_of_judgment env sigma tj) env in + let injectors = + map_succeed + (fun (cpath,t1_0,t2_0) -> + let (injbody,resty) = + build_injector sigma e_env (t1_0,t2_0) (VAR e) cpath in + let injfun = mkNamedLambda e t injbody in + try + let _ = type_of env sigma injfun in (injfun,resty) + with e when catchable_exception e -> failwith "caught") + posns + in + if injectors = [] then + errorlabstrm "Equality.decompEqThen" + [<'sTR "Discriminate failed to decompose the equality">]; + ((tclTHEN + (tclMAP (fun (injfun,resty) -> + let pf = applist(get_pat lbeq.congr, + [t;resty;injfun;t1;t2; + VAR id]) in + let ty = pf_type_of gls pf in + ((tclTHENS (cut ty) + ([tclIDTAC;refine pf])))) + (List.rev injectors)) + (ntac (List.length injectors)))) + gls) + | _ -> assert false) + +let decompEq = decompEqThen (fun x -> tclIDTAC) + +let dEqThen ntac cls gls = + match cls with + | None -> + if somatches (pf_concl gls) not_pattern then + (tclTHEN hnf_in_concl + (tclTHEN intro + (onLastHyp (compose (decompEqThen ntac) out_some)))) gls + else + errorlabstrm "DEqThen" (insatisfied_prec_message cls) + | Some id -> + try + decompEqThen ntac id gls + with + | Not_found -> + errorlabstrm "DEqThen" (not_found_message id) + | e when catchable_exception e -> + errorlabstrm "DEqThen" (insatisfied_prec_message cls) + +let dEq = dEqThen (fun x -> tclIDTAC) + +let dEqConcl gls = dEq None gls +let dEqHyp id gls = dEq (Some id) gls + +(**) +let dEqConcl_tac = hide_atomic_tactic "DEqConcl" dEqConcl +let dEqHyp_tac = hide_ident_tactic "DEqHyp" dEqHyp +(**) + +let rewrite_msg = function + | None -> + [<'sTR "passed term is not a primitive equality">] + | Some id -> + [<'sTR (string_of_id id); 'sTR "does not satisfy preconditions ">] + +let swap_equands gls eqn = + let (lbeq,(t,e1,e2)) = + try + find_eq_data_decompose eqn + with _ -> errorlabstrm "swap_equamds" (rewrite_msg None) + in + applist(get_pat lbeq.eq,[t;e2;e1]) + +let swapEquandsInConcl gls = + let (lbeq,(t,e1,e2)) = + try + find_eq_data_decompose (pf_concl gls) + with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) + in + let sym_equal = get_pat lbeq.sym in + refine (applist(sym_equal,[t;e2;e1;DOP0(Meta(new_meta()))])) gls + +let swapEquandsInHyp id gls = + ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls))) + ([tclIDTAC; + (tclTHEN (swapEquandsInConcl) (exact (VAR id)))]))) gls + +(* find_elim determines which elimination principle is necessary to + eliminate lbeq on sort_of_gl. It yields the boolean true wether + it is a dependent elimination principle (as idT.rect) and false + otherwise *) + +let find_elim sort_of_gl lbeq = + match sort_of_gl with + | DOP0(Sort(Prop Null)) (* Prop *) -> (get_pat lbeq.ind, false) + | DOP0(Sort(Prop Pos)) (* Set *) -> + (match lbeq.rrec with + | Some eq_rec -> (get_pat eq_rec, false) + | None -> errorlabstrm "find_elim" + [< 'sTR "this type of elimination is not allowed">]) + | _ (* Type *) -> + (match lbeq.rect with + | Some eq_rect -> (get_pat eq_rect, true) + | None -> errorlabstrm "find_elim" + [< 'sTR "this type of elimination is not allowed">]) + +(* builds a predicate [e:t][H:(lbeq t e t1)](body e) + to be used as an argument for equality dependent elimination principle: + Preconditon: dependent body (Rel 1) *) + +let build_dependent_rewrite_predicate (t,t1,t2) body lbeq gls = + let e = pf_get_new_id (id_of_string "e") gls in + let h = pf_get_new_id (id_of_string "HH") gls in + let eq_term = get_pat lbeq.eq in + (mkNamedLambda e t + (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) + (lift 1 body))) + +(* builds a predicate [e:t](body e) ??? + to be used as an argument for equality non-dependent elimination principle: + Preconditon: dependent body (Rel 1) *) + +let build_non_dependent_rewrite_predicate (t,t1,t2) body gls = + lambda_create (pf_env gls) (t,body) + +let bareRevSubstInConcl lbeq body (t,e1,e2) gls = + let (eq_elim,dep) = + try + find_elim (pf_type_of gls (pf_concl gls)) lbeq + with e when catchable_exception e -> + errorlabstrm "RevSubstIncConcl" + [< 'sTR "this type of substitution is not allowed">] + in + let p = + if dep then + (build_dependent_rewrite_predicate (t,e1,e2) body lbeq gls) + else + (build_non_dependent_rewrite_predicate (t,e1,e2) body gls) + in + refine (applist(eq_elim,[t;e1;p;DOP0(Meta(new_meta())); + e2;DOP0(Meta(new_meta()))])) gls + +(* [subst_tuple_term dep_pair B] + + Given that dep_pair looks like: + + (existS e1 (existS e2 ... (existS en en+1) ... )) + + and B might contain instances of the ei, we will return the term: + + ([x1:ty(e1)]...[xn:ty(en)]B + (projS1 (Rel 1)) + (projS1 (projS2 (Rel 1))) + ... etc ...) + + That is, we will abstract out the terms e1...en+1 as usual, but + will then produce a term in which the abstraction is on a single + term - the debruijn index [Rel 1], which will be of the same type + as dep_pair. + + ALGORITHM for abstraction: + + We have a list of terms, [e1]...[en+1], which we want to abstract + out of [B]. For each term [ei], going backwards from [n+1], we + just do a [subst_term], and then do a lambda-abstraction to the + type of the [ei]. + + *) + + +let comp_carS_pattern = put_pat mmk "<<x>>(projS1 ? ? (?)@[x])" +let comp_cdrS_pattern = put_pat mmk "<<x>>(projS2 ? ? (?)@[x])" + +let comp_carT_pattern = put_pat mmk "<<x>>(projT1 ? ? (?)@[x])" +let comp_cdrT_pattern = put_pat mmk "<<x>>(projT2 ? ? (?)@[x])" + +let dest_somatch_sigma ex ex_pat = + match dest_somatch ex ex_pat with + | [a;p;car;cdr] -> (a,p,car,cdr) + | _ -> anomaly "dest_somatch_sigma: a sigma pattern should match 4 terms" + +let find_sigma_data_decompose ex = + try + (comp_carS_pattern, comp_cdrS_pattern, + dest_somatch_sigma ex existS_pattern) + with _ -> + (try + (comp_carT_pattern,comp_cdrT_pattern, + dest_somatch_sigma ex existT_pattern) + with _ -> + errorlabstrm "find_sigma_data_decompose" [< >]) + +let decomp_tuple_term env = + let rec decomprec to_here_fun ex = + try + let (comp_car_pattern,comp_cdr_pattern,(a,p,car,cdr)) = + find_sigma_data_decompose ex in + let car_code = soinstance comp_car_pattern [a;p;to_here_fun] + and cdr_code = soinstance comp_cdr_pattern [a;p;to_here_fun] in + (car,named_hd env a Anonymous,car_code)::(decomprec cdr_code cdr) + with e when catchable_exception e -> + [(ex,named_hd env ex Anonymous,to_here_fun)] + in + decomprec (DLAM(Anonymous,Rel 1)) + +let subst_tuple_term env sigma dep_pair b = + let sort_of_dep_pair = + type_of env sigma (type_of env sigma dep_pair) in + let (proj1_term,proj2_term,sig_elim_term,_,_) = + find_sigma_data sort_of_dep_pair in + let e_list = decomp_tuple_term env dep_pair in + let abst_B = + List.fold_right (fun (e,na,_) b -> + let body = subst_term e b in + let pB = DLAM(na,body) in + DOP2(Lambda,type_of env sigma e,pB)) + e_list b + in + let app_B = + applist(abst_B,(List.map (fun (_,_,c) -> (sAPP c (Rel 1))) e_list)) in + let (proj1_sp,_) = destConst (get_pat proj1_term) + and (proj2_sp,_) = destConst (get_pat proj2_term) + and (sig_elim_sp,_) = destConst (get_pat sig_elim_term) in + strong (fun _ _ -> + compose (whd_betaiota env sigma) + (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) + env sigma app_B + +(* |- (P e2) + BY RevSubstInConcl (eq T e1 e2) + |- (P e1) + |- (eq T e1 e2) + *) +let revSubstInConcl eqn gls = + let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in + let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in + if not (dependent (Rel 1) body) then errorlabstrm "RevSubstInConcl" [<>]; + bareRevSubstInConcl lbeq body (t,e1,e2) gls + +(* |- (P e1) + BY SubstInConcl (eq T e1 e2) + |- (P e2) + |- (eq T e1 e2) + *) +let substInConcl eqn gls = + (tclTHENS (revSubstInConcl (swap_equands gls eqn)) + ([tclIDTAC; + swapEquandsInConcl])) gls + +let substInHyp eqn id gls = + let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in + let body = subst_term e1 (clause_type (Some id) gls) in + if not (dependent (Rel 1) body) then errorlabstrm "SubstInHyp" [<>]; + let pB = DLAM(Environ.named_hd (pf_env gls) t Anonymous,body) in + (tclTHENS (cut_replacing id (sAPP pB e2)) + ([tclIDTAC; + (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2)) + ([exact (VAR id);tclIDTAC]))])) gls + +let revSubstInHyp eqn id gls = + (tclTHENS (substInHyp (swap_equands gls eqn) id) + ([tclIDTAC; + swapEquandsInConcl])) gls + +let try_rewrite tac gls = + try + tac gls + with + | UserError ("find_eq_data_decompose",_) -> errorlabstrm + "try_rewrite" [< 'sTR "Not a primitive equality here">] + | UserError ("swap_equamds",_) -> errorlabstrm + "try_rewrite" [< 'sTR "Not a primitive equality here">] + | UserError("find_eq_elim",s) -> errorlabstrm "try_rew" + [<'sTR "This type of elimination is not allowed ">] + | e when catchable_exception e -> + errorlabstrm "try_rewrite" + [< 'sTR "Cannot find a well type generalisation of the goal that"; + 'sTR " makes progress the proof.">] + +(* list_int n 0 [] gives the list [1;2;...;n] *) +let rec list_int n cmr l = + if cmr = n then + l @ [n] + else + list_int n (cmr+1) (l @ [cmr]) + +(* Tells if two constrs are equal modulo unification *) + +let bind_eq = function + | (Anonymous,Anonymous) -> true + | (Name _,Name _) -> true + | _ -> false + +let rec eq_mod_rel l_meta = function + | (t,DOP0(Meta n)) -> + if not (List.mem n (fst (List.split l_meta))) then + Some ([(n,t)]@l_meta) + else if (List.assoc n l_meta) = t then + Some l_meta + else + None + | (DOP1(op0,c0),DOP1(op1,c1)) -> + if op0 = op1 then + eq_mod_rel l_meta (c0,c1) + else + None + | (DOP2(op0,t0,c0),DOP2(op1,t1,c1)) -> + if op0 = op1 then + match (eq_mod_rel l_meta (t0,t1)) with + | None -> None + | Some l -> eq_mod_rel l (c0,c1) + else + None + | (DOPN(op0,t0),DOPN(op1,t1)) -> + if (op0 = op1) & (Array.length t0 = Array.length t1) then + List.fold_left2 + (fun a c1 c2 -> + match a with + | None -> None + | Some l -> eq_mod_rel l (c1,c2)) (Some l_meta) + (Array.to_list t0) (Array.to_list t1) + else + None + | (DLAM(n0,t0),DLAM(n1,t1)) -> + if bind_eq (n0,n1) then + eq_mod_rel l_meta (t0,t1) + else + None + | (t,u) -> + if t = u then + Some l_meta + else + None + +(* Verifies if the constr has an head constant *) + +let is_hd_const = function + | DOPN(AppL,t) -> + (match t.(0) with + | DOPN(Const c,_) -> Some (Const c, array_tl t) + |_ -> None) + | _ -> None + +(* Gives the occurences number of t in u *) +let rec nb_occ_term t u = + let one_step t = function + | DOP1(_,c) -> nb_occ_term t c + | DOP2(_,c0,c1) -> (nb_occ_term t c0) + (nb_occ_term t c1) + | DOPN(_,a) -> Array.fold_left (fun a x -> a + (nb_occ_term t x)) 0 a + | DOPL(_,l) -> List.fold_left (fun a x -> a + (nb_occ_term t x)) 0 l + | DLAM(_,c) -> nb_occ_term t c + | DLAMV(_,a) -> Array.fold_left (fun a x -> a + (nb_occ_term t x)) 0 a + | _ -> 0 + in + if t = u then + 1 + else + one_step t u + +(* Gives Some(first instance of ceq in cref,occurence number for this + instance) or None if no instance of ceq can be found in cref *) + +let sub_term_with_unif cref ceq = + let rec find_match l_meta nb_occ op_ceq t_eq = function + | DOPN(AppL,t) as u -> + (match (t.(0)) with + | DOPN(op,t_op) -> + let t_args=Array.of_list (List.tl (Array.to_list t)) in + if op = op_ceq then + match + (List.fold_left2 + (fun a c0 c1 -> + match a with + | None -> None + | Some l -> eq_mod_rel l (c0,c1)) (Some l_meta) + (Array.to_list t_args) (Array.to_list t_eq)) + with + | None -> + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ + op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list + t_args) + | Some l -> (l,nb_occ+1) + else + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta + nb_occ op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list t) + | VAR _ -> + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta + nb_occ op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list t) + |_ -> (l_meta,nb_occ)) + | DOP2(_,t,DLAM(_,c)) -> + let (lt,nbt)=find_match l_meta nb_occ op_ceq t_eq t in + find_match lt nbt op_ceq t_eq c + | DOPN(_,t) -> + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ op_ceq + t_eq x) (l_meta,nb_occ) (Array.to_list t) + |_ -> (l_meta,nb_occ) + in + match (is_hd_const ceq) with + | None -> + if (occur_meta ceq) then + None + else + let nb_occ = nb_occ_term ceq cref in + if nb_occ = 0 then + None + else + Some (ceq,nb_occ) + |Some (head,t_args) -> + let (l,nb)=find_match [] 0 head t_args cref in + if nb = 0 then + None + else + Some ((plain_instance l ceq),nb) + +(*The Rewrite in tactic*) +let general_rewrite_in lft2rgt id (c,lb) gls = + let typ_id = + (try + let (_,ty) = lookup_var id (pf_env gls) in ty.body + with Not_found -> + errorlabstrm "general_rewrite_in" + [< 'sTR"No such hypothesis : "; print_id id >]) + in + let (wc,_) = startWalk gls + and (_,_,t) = reduce_to_ind (pf_env gls) (project gls) (pf_type_of gls c) in + let ctype = type_clenv_binding wc (c,t) lb in + match (match_with_equation ctype) with + | None -> error "The term provided does not end with an equation" + | Some (hdcncl,l) -> + let mbr_eq = + if lft2rgt then + List.hd (List.tl (List.rev l)) + else + List.hd (List.rev l) + in + (match (sub_term_with_unif + (collapse_appl (strip_outer_cast typ_id)) + (collapse_appl mbr_eq)) with + | None -> + errorlabstrm "general_rewrite_in" + [<'sTR "Nothing to rewrite in: "; print_id id>] + |Some (l2,nb_occ) -> + (tclTHENSI + (tclTHEN + (tclTHEN (generalize [(pf_global gls id)]) + (reduce (Pattern [(list_int nb_occ 1 [],l2, + pf_type_of gls l2)]) [])) + (general_rewrite_bindings lft2rgt (c,lb))) + [(tclTHEN (clear_one id) (introduction id))]) gls) + +let dyn_rewrite_in lft2rgt = function + | [Identifier id;(Command com);(Bindings binds)] -> + tactic_com_bind_list (general_rewrite_in lft2rgt id) (com,binds) + | [Identifier id;(Constr c);(Cbindings binds)] -> + general_rewrite_in lft2rgt id (c,binds) + | _ -> assert false + +let rewriteLR_in_tac = hide_tactic "RewriteLRin" (dyn_rewrite_in true) +let rewriteRL_in_tac = hide_tactic "RewriteRLin" (dyn_rewrite_in false) + +let conditional_rewrite_in lft2rgt id tac (c,bl) = + tclTHEN_i (general_rewrite_in lft2rgt id (c,bl)) + (fun i -> if i=1 then tclIDTAC else tclCOMPLETE tac) 1 + +let dyn_conditional_rewrite_in lft2rgt = function + | [(Tacexp tac); Identifier id; (Command com);(Bindings binds)] -> + tactic_com_bind_list + (conditional_rewrite_in lft2rgt id (Tacinterp.interp tac)) + (com,binds) + | [(Tacexp tac); Identifier id; (Constr c);(Cbindings binds)] -> + conditional_rewrite_in lft2rgt id (Tacinterp.interp tac) (c,binds) + | _ -> assert false + +let v_conditional_rewriteLR_in = + hide_tactic "CondRewriteLRin" (dyn_conditional_rewrite_in true) + +let v_conditional_rewriteRL_in = + hide_tactic "CondRewriteRLin" (dyn_conditional_rewrite_in false) + +(* Rewrite c in id. Rewrite -> c in id. Rewrite <- c in id. + Does not work when c is a conditional equation *) + +let rewrite_in lR com id gls = + (try + let _ = lookup_var id (pf_env gls) in () + with Not_found -> + errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;print_id id >]); + let c = pf_constr_of_com gls com in + let eqn = pf_type_of gls c in + try + let _ = find_eq_data_decompose eqn in + (try + (tclTHENS + ((if lR then substInHyp else revSubstInHyp) eqn id) + ([tclIDTAC ; exact c])) gls + with UserError("SubstInHyp",_) -> tclIDTAC gls) + with UserError ("find_eq_data_decompose",_)-> + errorlabstrm "rewrite_in" [< 'sTR"No equality here" >] + +let subst eqn cls gls = + match cls with + | None -> substInConcl eqn gls + | Some id -> substInHyp eqn id gls + +(* |- (P a) + * Subst_Concl a=b + * |- (P b) + * |- a=b + *) + +let substConcl_LR eqn gls = try_rewrite (subst eqn None) gls +let substConcl_LR_tac = + let gentac = + hide_tactic "SubstConcl_LR" + (function + | [Command eqn] -> + (fun gls -> substConcl_LR (pf_constr_of_com gls eqn) gls) + | _ -> assert false) + in + fun eqn -> gentac [Command eqn] + +(* id:(P a) |- G + * SubstHyp a=b id + * id:(P b) |- G + * id:(P a) |-a=b +*) + +let hypSubst id cls gls = + match cls with + | None -> + (tclTHENS (substInConcl (clause_type (Some id) gls)) + ([tclIDTAC; exact (VAR id)])) gls + | Some hypid -> + (tclTHENS (substInHyp (clause_type (Some id) gls) hypid) + ([tclIDTAC;exact (VAR id)])) gls + +(* id:a=b |- (P a) + * HypSubst id. + * id:a=b |- (P b) + *) +let substHypInConcl_LR id gls = try_rewrite (hypSubst id None) gls +let substHypInConcl_LR_tac = + let gentac = + hide_tactic "SubstHypInConcl_LR" + (function + | [Identifier id] -> substHypInConcl_LR id + | _ -> assert false) + in + fun id -> gentac [Identifier id] + +(* id:a=b H:(P a) |- G + SubstHypInHyp id H. + id:a=b H:(P b) |- G +*) +let revSubst eqn cls gls = + match cls with + | None -> revSubstInConcl eqn gls + | Some id -> revSubstInHyp eqn id gls + +(* |- (P b) + SubstConcl_RL a=b + |- (P a) + |- a=b +*) +let substConcl_RL eqn gls = try_rewrite (revSubst eqn None) gls +let substConcl_RL_tac = + let gentac = + hide_tactic "SubstConcl_RL" + (function + | [Command eqn] -> + (fun gls -> substConcl_RL (pf_constr_of_com gls eqn) gls) + | _ -> assert false) + in + fun eqn -> gentac [Command eqn] + +(* id:(P b) |-G + SubstHyp_RL a=b id + id:(P a) |- G + |- a=b +*) +let substHyp_RL eqn id gls = try_rewrite (revSubst eqn (Some id)) gls + +let revHypSubst id cls gls = + match cls with + | None -> + (tclTHENS (revSubstInConcl (clause_type (Some id) gls)) + ([tclIDTAC; exact (VAR id)])) gls + | Some hypid -> + (tclTHENS (revSubstInHyp (clause_type (Some id) gls) hypid) + ([tclIDTAC;exact (VAR id)])) gls + +(* id:a=b |- (P b) + * HypSubst id. + * id:a=b |- (P a) + *) +let substHypInConcl_RL id gls = try_rewrite (revHypSubst id None) gls +let substHypInConcl_RL_tac = + let gentac = + hide_tactic "SubstHypInConcl_RL" + (function + | [Identifier id] -> substHypInConcl_RL id + | _ -> assert false) + in + fun id -> gentac [Identifier id] + +(* id:a=b H:(P b) |- G + SubstHypInHyp id H. + id:a=b H:(P a) |- G +*) + +(***************) +(* AutoRewrite *) +(***************) + +(****Dealing with the rewriting rules****) + +(* A rewriting is typically an equational constr with an orientation (true=LR + and false=RL) *) +type rewriting_rule = constr * bool + +(* The table of rewriting rules. The key is the name of the rule base. + the value is a list of [rewriting_rule] *) +let rew_tab = ref Gmapl.empty + +(*Functions necessary to the summary*) +let init () = rew_tab := Gmapl.empty +let freeze () = !rew_tab +let unfreeze ft = rew_tab := ft + +(*Declaration of the summary*) +let _ = + Summary.declare_summary "autorewrite" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + +(*Adds a list of rules to the rule table*) +let add_list_rules rbase lrl = + List.iter (fun r -> rew_tab := Gmapl.add rbase r !rew_tab) lrl + +(*Gives the list of rules for the base named rbase*) +let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab) + +(*Functions necessary to the library object declaration*) +let load_autorewrite_rule _ = () +let open_autorewrite_rule _ = () +let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl +let specification_autorewrite_rule x = x + +(*Declaration of the AUTOREWRITE_RULE library object*) +let (in_autorewrite_rule,out_autorewrite_rule)= + Libobject.declare_object + ("AUTOREWRITE_RULE", + { Libobject.load_function = load_autorewrite_rule; + Libobject.open_function = open_autorewrite_rule; + Libobject.cache_function = cache_autorewrite_rule; + Libobject.specification_function = specification_autorewrite_rule }) + +(* Semantic of the HintRewrite vernacular command *) +let _ = + vinterp_add "HintRewrite" + (let rec lrules_arg lrl = function + | [] -> lrl + | (VARG_VARGLIST [VARG_CONSTR rule; VARG_STRING ort])::a + when ort="LR" or ort="RL" -> + lrules_arg (lrl@[(Astterm.constr_of_com Evd.empty + (Global.env()) rule,ort="LR")]) a + | _ -> bad_vernac_args "HintRewrite" + and lbases_arg lbs = function + | [] -> lbs + | (VARG_VARGLIST ((VARG_IDENTIFIER rbase)::b))::a -> + lbases_arg (lbs@[(rbase,lrules_arg [] b)]) a + | _ -> bad_vernac_args "HintRewrite" + in + fun largs () -> + List.iter (fun c -> Lib.add_anonymous_leaf + (in_autorewrite_rule c)) (lbases_arg [] largs)) + +(****The tactic****) + +(*To build the validation function. Length=number of unproven goals, Valid=a + validation which solves*) +type valid_elem = + | Length of int + | Valid of validation + +(* Ce truc devrait aller dans Std -- papageno *) +(*Gives the sub_list characterized by the indexes i_s and i_e with respect to + lref*) +let sub_list lref i_s i_e = + let rec sub_list_rec l i = + if i = i_e then + l @ [List.nth lref i] + else if (i>=i_s) & (i<i_e) then + sub_list_rec (l@[List.nth lref i]) (i+1) + else + anomalylabstrm "Equality.sub_list" [<'sTR "Out of range">] + in + sub_list_rec [] i_s + +(*Cuts the list l2becut in lists which lengths are given by llth*) +let cut_list l2becut lval = + let rec cut4_1goal cmr l1g = function + | [] -> (cmr,l1g) + | a::b -> + (match a with + | Length lth -> + if lth = 0 then + cut4_1goal cmr l1g b + else + cut4_1goal (cmr+lth) + (l1g@(sub_list l2becut cmr (cmr+lth-1))) b + | Valid p -> + cut4_1goal cmr (l1g@[p []]) b) + and cut_list_rec cmr l2b=function + | [] -> l2b + | a::b -> + let (cmr,l1g)=cut4_1goal cmr [] a in + cut_list_rec cmr (l2b@[l1g]) b + in + cut_list_rec 0 [] lval + +(*Builds the validation function with lvalid and with respect to l*) +let validation_gen lvalid l = + let (lval,larg_velem) = List.split lvalid in + let larg=cut_list l larg_velem in + List.fold_left2 (fun a p l -> p ([a]@l)) (List.hd lval (List.hd larg)) + (List.tl lval) (List.tl larg) + +(*Adds the main argument for the last validation function*) +let mod_hdlist l = + match (List.hd l) with + | (p,[Length 0]) -> l + | (p,larg) -> (p,[Length 1]@larg)::(List.tl l) + +(*For the Step options*) +type option_step= + | Solve + | Use + | All + +(* the user can give a base either by a name of by its full definition + The definition is an Ast that will find its meaning only in the context + of a given goal *) +type hint_base = + | By_name of identifier + | Explicit of (Coqast.t * bool) list + +let explicit_hint_base gl = function + | By_name id -> + begin match rules_of_base id with + | [] -> errorlabstrm "autorewrite" [<'sTR ("Base "^(string_of_id id)^ + " does not exist")>] + | lbs -> lbs + end + | Explicit lbs -> + List.map (fun (ast,b) -> (pf_constr_of_com gl ast, b)) lbs + +(*AutoRewrite cannot be expressed with a combination of tacticals (due to the + options). So, we make it in a primitive way*) +let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = + let lst = List.flatten (List.map (explicit_hint_base gls) lbases) + and unproven_goals = ref [] + and fails = ref 0 + and (sigr,g) = unpackage gls in + let put_rewrite lrw = List.map (fun (x,y) -> general_rewrite y x) lrw + and nbr_rules = List.length lst in + let lst_rew = put_rewrite lst in + let rec try2solve_main_goal mgl = function + | [] -> None + | a::b -> + try + let (gl_solve,p_solve)=apply_sig_tac sigr a mgl in + if gl_solve=[] then + Some (gl_solve,p_solve) + else + try2solve_main_goal mgl b + with e when catchable_exception e -> + try2solve_main_goal mgl b + and try_tacs4main_goal mgl = function + | [] -> None + | a::b -> + try + Some (apply_sig_tac sigr a mgl) + with e when catchable_exception e -> + try_tacs4main_goal mgl b + and try2solve1gen_goal gl = function + | [] -> ([gl],Length 1) + | a::b -> + try + let (gl_solve,p_solve)=apply_sig_tac sigr a gl in + if gl_solve=[] then + ([],Valid p_solve) + else + try2solve1gen_goal gl b + with e when catchable_exception e -> + try2solve1gen_goal gl b + and try2solve_gen_goals (lgls,valg) ltac = function + | [] -> (lgls,valg) + | a::b -> + let (g,elem)=try2solve1gen_goal a ltac in + try2solve_gen_goals (lgls@g,valg@[elem]) ltac b + and iterative_rew cmr fails (cglob,cmod,warn) unp_goals lvalid = + let cmd = ref cmod + and wrn = ref warn in + if !cmd=depth_step then begin + wARNING [<'sTR ((string_of_int cglob)^" rewriting(s) carried out") >]; + cmd := 0; + wrn := true + end; + if fails = nbr_rules then + (unp_goals,lvalid,!wrn) + else if cmr = nbr_rules then + iterative_rew 0 0 (cglob,!cmd,!wrn) unp_goals lvalid + else + try + let (gl,p) = + apply_sig_tac sigr (List.nth lst_rew cmr) (List.hd unp_goals) + in + let (lgl_gen,lval_gen) = + match ltacrest with + | None -> + if (List.length gl)=1 then + ([],[]) + else + (List.tl gl,[Length ((List.length gl)-1)]) + | Some ltac -> + try2solve_gen_goals ([],[]) ltac (List.tl gl) + in + if opt_rest & (not(lgl_gen=[])) then + iterative_rew (cmr+1) (fails+1) (cglob,!cmd,!wrn) unp_goals lvalid + else + (match ltacstp with + | None -> + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + ((List.hd gl)::(lgl_gen@(List.tl unp_goals))) + ((p,lval_gen)::lvalid) + | Some ltac -> + (match opt_step with + | Solve -> + (match (try2solve_main_goal (List.hd gl) ltac) with + | None -> + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + ((List.hd gl)::(lgl_gen@(List.tl unp_goals))) + ((p,lval_gen)::lvalid) + | Some (gl_solve,p_solve) -> + (lgl_gen@(List.tl unp_goals), + (p_solve,[Length 0])::(p,lval_gen) + ::lvalid,!wrn)) + | Use -> + (match (try_tacs4main_goal (List.hd gl) ltac) with + | None -> + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + ((List.hd gl)::(lgl_gen@(List.tl unp_goals))) + ((p,lval_gen)::lvalid) + | Some(gl_trans,p_trans) -> + let lth=List.length gl_trans in + if lth=0 then + (lgl_gen@(List.tl unp_goals), + (p_trans,[Length 0])::(p,lval_gen)::lvalid, + !wrn) + else if lth=1 then + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + (gl_trans@(lgl_gen@(List.tl + unp_goals))) + ((p_trans,[])::(p,lval_gen):: + lvalid) + else + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + (gl_trans@(lgl_gen@(List.tl unp_goals))) + ((p_trans, + [Length ((List.length gl_trans)-1)]):: + (p,lval_gen):: lvalid)) + | All -> + (match (try2solve_main_goal (List.hd gl) ltac) with + | None -> + (match (try_tacs4main_goal + (List.hd gl) ltac) with + | None -> + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + ((List.hd + gl)::(lgl_gen@(List.tl + unp_goals))) + ((p,lval_gen)::lvalid) + | Some(gl_trans,p_trans) -> + let lth = List.length gl_trans in + if lth = 0 then + (lgl_gen@(List.tl unp_goals), + (p_trans,[Length 0]):: + (p,lval_gen)::lvalid, !wrn) + else if lth = 1 then + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + (gl_trans@ + (lgl_gen@ + (List.tl unp_goals))) + ((p_trans,[]):: + (p,lval_gen)::lvalid) + else + iterative_rew (cmr+1) fails + (cglob+1,!cmd+1,!wrn) + (gl_trans@ + (lgl_gen@ + (List.tl unp_goals))) + ((p_trans, + [Length + ((List.length gl_trans)-1)]):: + (p, lval_gen)::lvalid)) + | Some (gl_solve,p_solve) -> + (lgl_gen@(List.tl unp_goals), + (p_solve,[Length 0]):: + (p,lval_gen)::lvalid,!wrn)))) + with e when catchable_exception e -> + iterative_rew (cmr+1) (fails+1) (cglob,!cmd,!wrn) unp_goals lvalid + in + let (gl,lvalid)= + let (gl_res,lvalid_res,warn)=iterative_rew 0 0 (0,0,false) [g] [] in + if warn then mSGNL [<>]; + (gl_res,lvalid_res) + in + let validation_fun= + if lvalid = [] then + (fun l -> List.hd l) + else + let nlvalid=mod_hdlist lvalid in + (fun l -> validation_gen nlvalid l) + in + (repackage sigr gl,validation_fun) + +(*Collects the arguments of AutoRewrite ast node*) +let dyn_autorewrite largs= + let rec explicit_base largs = + let tacargs = List.map cvt_arg largs in + List.map + (function + | Redexp ("LR", [Coqast.Node(_,"Command", [ast])]) -> ast, true + | Redexp ("RL", [Coqast.Node(_,"Command", [ast])]) -> ast, false + | _ -> anomaly "Equality.explicit_base") + tacargs + and list_bases largs = + let tacargs = List.map cvt_arg largs in + List.map + (function + | Redexp ("ByName", [Coqast.Nvar(_,s)]) -> + By_name (id_of_string s) + | Redexp ("Explicit", l) -> + Explicit (explicit_base l) + | _ -> anomaly "Equality.list_bases") + tacargs + and int_arg=function + | [(Integer n)] -> n + | _ -> anomalylabstrm "dyn_autorewrite" + [<'sTR "Bad call of int_arg (not an INTEGER)">] + and list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest) + (orest,evorest) (depth,evdepth) = function + | [] -> (lstep,ostep,lrest,orest,depth) + | (Redexp (s,l))::tail -> + if s="Step" & not evstep then + list_args_rest ((List.map Tacinterp.interp l),true) (ostep,evostep) + (lrest,evrest) (orest,evorest) (depth,evdepth) tail + else if s="SolveStep" & not evostep then + list_args_rest (lstep,evstep) (Solve,true) (lrest,evrest) + (orest,evorest) (depth,evdepth) tail + else if s="Use" & not evostep then + list_args_rest (lstep,evstep) (Use,true) (lrest,evrest) + (orest,evorest) (depth,evdepth) tail + else if s="All" & not evostep then + list_args_rest (lstep,evstep) (All,true) (lrest,evrest) + (orest,evorest) (depth,evdepth) tail + else if s="Rest" & not evrest then + list_args_rest (lstep,evstep) (ostep,evostep) + ((List.map Tacinterp.interp l),true) (orest,evorest) + (depth,evdepth) tail + else if s="SolveRest" & not evorest then + list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest) + (false,true) (depth,evdepth) tail + else if s="Cond" & not evorest then + list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest) + (true,true) (depth,evdepth) tail + else if s="Depth" & not evdepth then + (let dth = int_arg (List.map cvt_arg l) in + if dth > 0 then + list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest) + (orest,evorest) (dth,true) tail + else + errorlabstrm "dyn_autorewrite" + [<'sTR "Depth value lower or equal to 0">]) + else + anomalylabstrm "dyn_autorewrite" + [<'sTR "Bad call of list_args_rest">] + | _ -> + anomalylabstrm "dyn_autorewrite" + [<'sTR "Bad call of list_args_rest">] + and list_args = function + | (Redexp (s,lbases))::tail -> + if s = "BaseList" then + (let (lstep,ostep,lrest,orest,depth) = + list_args_rest ([],false) (Solve,false) ([],false) (false,false) + (100,false) tail + in + autorewrite (list_bases lbases) + (if lstep = [] then None else Some lstep) + ostep (if lrest=[] then None else Some lrest) orest depth) + else + anomalylabstrm "dyn_autorewrite" + [<'sTR "Bad call of list_args (not a BaseList tagged REDEXP)">] + | _ -> + anomalylabstrm "dyn_autorewrite" + [<'sTR "Bad call of list_args (not a REDEXP)">] + in + list_args largs + +(*Adds and hides the AutoRewrite tactic*) +let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite + diff --git a/tactics/equality.mli b/tactics/equality.mli new file mode 100644 index 000000000..8cb4cfe18 --- /dev/null +++ b/tactics/equality.mli @@ -0,0 +1,147 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Sign +open Evd +open Environ +open Proof_trees +open Tacmach +open Pattern +open Wcclausenv +open Tacticals +open Tactics +(*i*) + +type leibniz_eq = { + eq : marked_term; + ind : marked_term; + rrec : marked_term option; + rect : marked_term option; + congr: marked_term; + sym : marked_term } + +val eq : leibniz_eq +val eqT : leibniz_eq +val idT : leibniz_eq + +val eq_pattern : marked_term +val eqT_pattern : marked_term +val idT_pattern : marked_term + +val find_eq_pattern : constr -> constr -> constr + + +val general_rewrite_bindings : bool -> (constr * constr substitution) -> tactic +val general_rewrite : bool -> constr -> tactic +val rewriteLR_bindings : (constr * constr substitution) -> tactic +val h_rewriteLR_bindings : (constr * constr substitution) -> tactic +val rewriteRL_bindings : (constr * constr substitution) -> tactic +val h_rewriteRL_bindings : (constr * constr substitution) -> tactic + +val rewriteLR : constr -> tactic +val h_rewriteLR : constr -> tactic +val rewriteRL : constr -> tactic +val h_rewriteRL : constr -> tactic + +val conditional_rewrite : + bool -> tactic -> (constr * constr substitution) -> tactic +val general_rewrite_in : + bool -> identifier -> (constr * constr substitution) -> tactic +val conditional_rewrite_in : + bool -> identifier -> tactic -> (constr * constr substitution) -> tactic + + +(* usage : abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl + + eq,symeq : equality on Set and its symmetry theorem + eqt,sym_eqt : equality on Type and its symmetry theorem + c2 c1 : c1 is to be replaced by c2 + unsafe : If true, do not check that c1 and c2 are convertible + gl : goal +*) + +val abstract_replace : + constr * constr -> constr * constr -> constr -> constr -> bool -> tactic + +(* Only for internal use *) +val unsafe_replace : constr -> constr -> tactic + +val replace : constr -> constr -> tactic +val h_replace : constr -> constr -> tactic + +type elimination_types = + | Set_Type + | Type_Type + | Set_SetorProp + | Type_SetorProp + + +(* necessary_elimination [sort_of_arity] [sort_of_goal] *) +val necessary_elimination : constr -> constr -> elimination_types + +val discr : identifier -> tactic +val discrClause : clause -> tactic +val discrConcl : tactic +val discrHyp : identifier -> tactic +val discrEverywhere : tactic +val h_discrConcl : tactic +val h_discrHyp : identifier -> tactic +val h_discrConcl : tactic +val h_discr : tactic +val inj : identifier -> tactic +val h_injHyp : identifier -> tactic +val h_injConcl : tactic + +val dEq : clause -> tactic +val dEqThen : (int -> tactic) -> clause -> tactic + +val make_iterated_tuple : + 'a evar_map -> env -> (constr * constr) -> (constr * constr) + -> constr * constr * constr + +val subst : constr -> clause -> tactic +val hypSubst : identifier -> clause -> tactic +val revSubst : constr -> clause -> tactic +val revHypSubst : identifier -> clause -> tactic + +val discriminable : env -> 'a evar_map -> constr -> constr -> bool + +(***************) +(* AutoRewrite *) +(***************) + +(****Dealing with the rewriting rules****) + +(*A rewriting is typically an equational constr with an orientation (true=LR + and false=RL)*) +type rewriting_rule = constr * bool + +(*Adds a list of rules to the rule table*) +val add_list_rules : identifier -> rewriting_rule list -> unit + +(****The tactic****) + +(*For the Step options*) +type option_step = + | Solve + | Use + | All + +(* the user can give a base either by a name of by its full definition + The definition is an Ast that will find its meaning only in the context + of a given goal *) +type hint_base = + | By_name of identifier + | Explicit of (Coqast.t * bool) list + +val explicit_hint_base : goal sigma -> hint_base -> rewriting_rule list + +(*AutoRewrite cannot be expressed with a combination of tacticals (due to the + options). So, we make it in a primitive way*) +val autorewrite : + hint_base list -> tactic list option -> option_step + -> tactic list option -> bool -> int -> tactic + diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 3038933e9..239b5e84f 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -42,7 +42,7 @@ let parse_pattern s = raw_sopattern_of_compattern (Global.env()) com let (pattern_stock : constr Stock.stock) = - Stock.make_stock {name="PATTERN";proc=parse_pattern} + Stock.make_stock { name = "PATTERN"; proc = parse_pattern } let make_module_marker = Stock.make_module_marker pattern_stock let put_pat = Stock.stock pattern_stock @@ -306,8 +306,8 @@ let match_with_equation t = | IsMutInd ind -> let constr_types = Global.mind_lc_without_abstractions ind in - let refl_rel_term1 = put_pat mmk "(A:?)(x:A)(? A x x)" in - let refl_rel_term2 = put_pat mmk "(x:?)(? x x)" in + let refl_rel_term1 = put_pat mmk "(A : ?)(x:A)(? A x x)" in + let refl_rel_term2 = put_pat mmk "(x : ?)(? x x)" in let nconstr = Global.mind_nconstr ind in if nconstr = 1 && (somatches constr_types.(0) refl_rel_term1 || diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 50425b002..b7fdd67a7 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -90,19 +90,19 @@ let clenv_constrain_with_bindings bl clause = in matchrec clause bl -(***TODO: SUPPRIMMER ?? let add_prod_rel sigma (t,env) = match t with | DOP2(Prod,c1,(DLAM(na,b))) -> - (b,add_rel (na,Typing_ev.execute_type sigma env c1) env) + (b,push_rel (na,Typing.execute_type env sigma c1) env) | _ -> failwith "add_prod_rel" let rec add_prods_rel sigma (t,env) = try - add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota sigma t,env)) + add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota env sigma t,env)) with Failure "add_prod_rel" -> (t,env) +(***TODO: SUPPRIMMER ?? let add_prod_sign sigma (t,sign) = match t with | DOP2(Prod,c1,(DLAM(na,_) as b)) -> diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli index b1bf17e01..deae4091f 100644 --- a/tactics/wcclausenv.mli +++ b/tactics/wcclausenv.mli @@ -5,6 +5,7 @@ open Names open Term open Sign +open Environ open Evd open Proof_trees open Tacmach @@ -27,11 +28,10 @@ type wc = walking_constraints val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv -(*i** -val add_prod_rel : 'a evar_map -> constr * context -> constr * context - -val add_prods_rel : 'a evar_map -> constr * context -> constr * context +val add_prod_rel : 'a evar_map -> constr * env -> constr * env +val add_prods_rel : 'a evar_map -> constr * env -> constr * env +(*i** val add_prod_sign : 'a evar_map -> constr * typed_type signature -> constr * typed_type signature diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 7ae7ffa90..6760bcafa 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -15,15 +15,15 @@ Grammar command command1 := with command10 := allTexplicit [ "ALLT" ident($v) ":" command($t) "|" command($c1) ] - -> [<<(allT $t [$v:$t]$c1)>>] + -> [<<(allT $t [$v : $t]$c1)>>] | allTimplicit [ "ALLT" ident($v) "|" command($c1) ] -> [<<(allT ? [$v]$c1)>>] | exTexplicit [ "EXT" ident($v) ":" command($t) "|" command($c1) ] - -> [<<(exT $t [$v:$t]$c1)>>] + -> [<<(exT $t [$v : $t]$c1)>>] | exTimplicit [ "EXT" ident($v) "|" command($c1) ] -> [<<(exT ? [$v]$c1)>>] | exT2explicit [ "EXT" ident($v) ":" command($t) "|" command($c1) "&" - command($c2) ] -> [<<(exT2 $t [$v:$t]$c1 [$v:$t]$c2)>>] + command($c2) ] -> [<<(exT2 $t [$v : $t]$c1 [$v : $t]$c2)>>] | exT2implicit [ "EXT" ident($v) "|" command($c1) "&" command($c2) ] -> [<<(exT2 ? [$v]$c1 [$v]$c2)>>]. @@ -32,16 +32,16 @@ with command10 := Syntax constr level 10: allT_pred [<<(allT $_ $p)>>] -> [ [<hov 0> "AllT " $p:L ] ] - | allT [<<(allT $T [$x:$T]$p)>>] + | allT [<<(allT $T [$x : $T]$p)>>] -> [ [<hov 3> "ALLT " $x ":" $T:L " |" [1 0] $p:L ] ] | exT_pred [<<(exT $_ $p)>>] -> [ [<hov 4> "ExT " $p:L ] ] - | exT [<<(exT $t1 [$x:$T]$p)>>] + | exT [<<(exT $t1 [$x : $T]$p)>>] -> [ [<hov 4> "EXT " $x ":" $T:L " |" [1 0] $p:L ] ] | exT2_pred [<<(exT2 $_ $p1 $p2)>>] -> [ [<hov 4> "ExT2 " $p1:L [1 0] $p2:L ] ] - | exT2 [<<(exT2 $T [$x:$T]$P1 [$x:$T]$P2)>>] + | exT2 [<<(exT2 $T [$x : $T]$P1 [$x : $T]$P2)>>] -> [ [<hov 2> "EXT " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ] ; diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v new file mode 100755 index 000000000..e4406a65f --- /dev/null +++ b/theories/Logic/Classical.v @@ -0,0 +1,7 @@ + +(* $Id$ *) + +(* Classical Logic *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Set. diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v new file mode 100755 index 000000000..3b4e17041 --- /dev/null +++ b/theories/Logic/Classical_Pred_Set.v @@ -0,0 +1,57 @@ + +(* $Id$ *) + +(* Classical Predicate Logic on Set*) + +Require Classical_Prop. + +Section Generic. +Variable U: Set. + +(* de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EX n:U | ~(P n)). +Proof. +Unfold not; Intros P notall. +Apply NNPP; Unfold not. +Intro abs. +Cut ((n:U)(P n)); Auto. +Intro n; Apply NNPP. +Unfold not; Intros. +Apply abs; Exists n; Trivial. +Qed. + +Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EX n:U |(P n)). +Proof. +Intros P H. +Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n. +Apply NNPP; Trivial. +Qed. + +Lemma not_ex_all_not : (P:U->Prop) (~(EX n:U |(P n))) -> (n:U)~(P n). +Proof. +Unfold not; Intros P notex n abs. +Apply notex. +Exists n; Trivial. +Qed. + +Lemma not_ex_not_all : (P:U->Prop)(~(EX n:U | ~(P n))) -> (n:U)(P n). +Proof. +Intros P H n. +Apply NNPP. +Red; Intro K; Apply H; Exists n; Trivial. +Qed. + +Lemma ex_not_not_all : (P:U->Prop) (EX n:U | ~(P n)) -> ~(n:U)(P n). +Proof. +Unfold not; Intros P exnot allP. +Elim exnot; Auto. +Qed. + +Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EX n:U |(P n)). +Proof. +Unfold not; Intros P allnot exP; Elim exP; Intros n p. +Apply allnot with n; Auto. +Qed. + +End Generic. diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v new file mode 100755 index 000000000..2f3b331cb --- /dev/null +++ b/theories/Logic/Classical_Pred_Type.v @@ -0,0 +1,57 @@ + +(* $Id$ *) + +(* Classical Predicate Logic on Type *) + +Require Classical_Prop. + +Section Generic. +Variable U: Type. + +(* de Morgan laws for quantifiers *) + +Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EXT n:U | ~(P n)). +Proof. +Unfold not; Intros P notall. +Apply NNPP; Unfold not. +Intro abs. +Cut ((n:U)(P n)); Auto. +Intro n; Apply NNPP. +Unfold not; Intros. +Apply abs; Exists n; Trivial. +Qed. + +Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EXT n:U | (P n)). +Proof. +Intros P H. +Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n. +Apply NNPP; Trivial. +Qed. + +Lemma not_ex_all_not : (P:U->Prop)(~(EXT n:U | (P n))) -> (n:U)~(P n). +Proof. +Unfold not; Intros P notex n abs. +Apply notex. +Exists n; Trivial. +Qed. + +Lemma not_ex_not_all : (P:U->Prop)(~(EXT n:U | ~(P n))) -> (n:U)(P n). +Proof. +Intros P H n. +Apply NNPP. +Red; Intro K; Apply H; Exists n; Trivial. +Qed. + +Lemma ex_not_not_all : (P:U->Prop) (EXT n:U | ~(P n)) -> ~(n:U)(P n). +Proof. +Unfold not; Intros P exnot allP. +Elim exnot; Auto. +Qed. + +Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EXT n:U | (P n)). +Proof. +Unfold not; Intros P allnot exP; Elim exP; Intros n p. +Apply allnot with n; Auto. +Qed. + +End Generic. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v new file mode 100755 index 000000000..f9afd26b0 --- /dev/null +++ b/theories/Logic/Classical_Prop.v @@ -0,0 +1,73 @@ + +(* $Id$ *) + +(* Classical Propositional Logic *) + +Hints Unfold not : core. + +Axiom classic: (P:Prop)(P \/ ~(P)). + +Lemma NNPP : (p:Prop)~(~(p))->p. +Proof. +Unfold not; Intros; Elim (classic p); Auto. +Intro NP; Elim (H NP). +Qed. + +Lemma not_imply_elim : (P,Q:Prop)~(P->Q)->P. +Proof. +Intros; Apply NNPP; Red. +Intro; Apply H; Intro; Absurd P; Trivial. +Qed. + +Lemma not_imply_elim2 : (P,Q:Prop)~(P->Q) -> ~Q. +Proof. +Intros; Elim (classic Q); Auto. +Qed. + +Lemma imply_to_or : (P,Q:Prop)(P->Q) -> ~P \/ Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma imply_to_and : (P,Q:Prop)~(P->Q) -> P /\ ~Q. +Proof. +Intros; Split. +Apply not_imply_elim with Q; Trivial. +Apply not_imply_elim2 with P; Trivial. +Qed. + +Lemma or_to_imply : (P,Q:Prop)(~P \/ Q) -> P->Q. +Proof. +Induction 1; Auto. +Intros H1 H2; Elim (H1 H2). +Qed. + +Lemma not_and_or : (P,Q:Prop)~(P/\Q)-> ~P \/ ~Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma or_not_and : (P,Q:Prop)(~P \/ ~Q) -> ~(P/\Q). +Proof. +Induction 1; Red; Induction 2; Auto. +Qed. + +Lemma not_or_and : (P,Q:Prop)~(P\/Q)-> ~P /\ ~Q. +Proof. +Intros; Elim (classic P); Auto. +Qed. + +Lemma and_not_or : (P,Q:Prop)(~P /\ ~Q) -> ~(P\/Q). +Proof. +Induction 1; Red; Induction 3; Trivial. +Qed. + +Lemma imply_and_or: (P,Q:Prop)(P->Q) -> P \/ Q -> Q. +Proof. +Induction 2; Trivial. +Qed. + +Lemma imply_and_or2: (P,Q,R:Prop)(P->Q) -> P \/ R -> Q \/ R. +Proof. +Induction 2; Auto. +Qed. diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v new file mode 100755 index 000000000..c679f549c --- /dev/null +++ b/theories/Logic/Classical_Type.v @@ -0,0 +1,7 @@ + +(* $Id$ *) + +(* Classical Logic for Type *) + +Require Export Classical_Prop. +Require Export Classical_Pred_Type. diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v new file mode 100755 index 000000000..d1f45be08 --- /dev/null +++ b/theories/Logic/Eqdep.v @@ -0,0 +1,97 @@ + +(* $Id$ *) + +Section Dependent_Equality. + +Variable U : Set. +Variable P : U->Set. + +Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop := + eq_dep_intro : (eq_dep p x p x). +Hint constr_eq_dep : core v62 := Constructors eq_dep. + +Lemma eq_dep_sym : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep q y p x). +Proof. +Induction 1; Auto. +Qed. +Hints Immediate eq_dep_sym : core v62. + +Lemma eq_dep_trans : (p,q,r:U)(x:(P p))(y:(P q))(z:(P r)) + (eq_dep p x q y)->(eq_dep q y r z)->(eq_dep p x r z). +Proof. +Induction 1; Auto. +Qed. + +Inductive eq_dep1 [p:U;x:(P p);q:U;y:(P q)] : Prop := + eq_dep1_intro : (h:q=p) + (x=(eq_rec U q P y p h))->(eq_dep1 p x q y). + +Axiom eq_rec_eq : (p:U)(Q:U->Set)(x:(Q p))(h:p=p) + x=(eq_rec U p Q x p h). + + +Lemma eq_dep1_dep : + (p:U)(x:(P p))(q:U)(y:(P q))(eq_dep1 p x q y)->(eq_dep p x q y). +Proof. +Induction 1; Intros eq_qp. +Cut (h:q=p)(y0:(P q)) + (x=(eq_rec U q P y0 p h))->(eq_dep p x q y0). +Intros; Apply H0 with eq_qp; Auto. +Rewrite eq_qp; Intros h y0. +Elim eq_rec_eq. +Induction 1; Auto. +Qed. + +Lemma eq_dep_dep1 : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y). +Proof. +Induction 1; Intros. +Apply eq_dep1_intro with (refl_equal U p). +Elim eq_rec_eq; Trivial. +Qed. + +Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y. +Proof. +Induction 1; Intro. +Elim eq_rec_eq; Auto. +Qed. + +Lemma eq_dep_eq : (p:U)(x,y:(P p))(eq_dep p x p y)->x=y. +Proof. +Intros; Apply eq_dep1_eq; Apply eq_dep_dep1; Trivial. +Qed. + +Lemma equiv_eqex_eqdep : (p,q:U)(x:(P p))(y:(P q)) + (existS U P p x)=(existS U P q y) <-> (eq_dep p x q y). +Proof. +Split. +Intros. +Generalize (eq_ind (sigS U P) (existS U P q y) + [pr:(sigS U P)] (eq_dep (projS1 U P pr) (projS2 U P pr) q y)) . +Proof. +Simpl. +Intro. +Generalize (H0 (eq_dep_intro q y)) . +Intro. +Apply (H1 (existS U P p x)). +Auto. +Intros. +Elim H. +Auto. +Qed. + + +Lemma inj_pair2: (p:U)(x,y:(P p)) + (existS U P p x)=(existS U P p y)-> x=y. +Proof. +Intros. +Apply eq_dep_eq. +Generalize (equiv_eqex_eqdep p p x y) . +Induction 1. +Intros. +Auto. +Qed. + +End Dependent_Equality. + +Hints Resolve eq_dep_intro : core v62. +Hints Immediate eq_dep_sym eq_dep_eq : core v62. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v new file mode 100644 index 000000000..ecf73f99c --- /dev/null +++ b/theories/Logic/Eqdep_dec.v @@ -0,0 +1,148 @@ + +(* $Id$ *) + +(* We prove that there is only one proof of x=x, i.e (refl_equal ? x). + This holds if the equality upon the set of x is decidable. + A corollary of this theorem is the equality of the right projections + of two equal dependent pairs. + + Author: Thomas Kleymann <tms@dcs.ed.ac.uk> in Lego + adapted to Coq by B. Barras + Credit: Proofs up to K_dec follows an outline by Michael Hedberg +*) + + +(* We need some dependent elimination schemes *) +Scheme eq_indd := Induction for eq Sort Prop. +Scheme eqT_indd := Induction for eqT Sort Prop. +Scheme or_indd := Induction for or Sort Prop. + +Implicit Arguments On. + + (* Bijection between eq and eqT *) + Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y := + [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end. + + Definition eqT2eq: (A:Set)(x,y:A)x==y->x=y := + [A,x,_,eqTxy]<[y:A]x=y>Cases eqTxy of refl_eqT => (refl_equal ? x) end. + + Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)). +Intros. +Elim p using eq_indd. +Reflexivity. +Save. + + Lemma eqT_eq_bij: (A:Set)(x,y:A)(p:x==y)p==(eq2eqT (eqT2eq p)). +Intros. +Elim p using eqT_indd. +Reflexivity. +Save. + + +Section DecidableEqDep. + + Variable A: Type. + + Local comp: (x,y,y':A)x==y->x==y'->y==y' := + [x,y,y',eq1,eq2](eqT_ind ? ? [a]a==y' eq2 ? eq1). + + Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y). +Intros. +Elim u using eqT_indd. +Trivial. +Save. + + + + Variable eq_dec: (x,y:A) x==y \/ ~x==y. + + Variable x: A. + + + Local nu: (y:A)x==y->x==y := + [y,u]Case (eq_dec x y) of + [H:x==y]H + [H:~x==y](False_ind ? (H u)) + end. + + Remark nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v). +Intros. +Unfold nu. +Elim (eq_dec x y) using or_indd; Intros. +Reflexivity. + +Case y0; Trivial. +Save. + + + Local nu_inv: (y:A)x==y->x==y := [y,v](comp (nu (refl_eqT ? x)) v). + + + Remark nu_left_inv : (y:A)(u:x==y) (nu_inv (nu u))==u. +Intros. +Elim u using eqT_indd. +Unfold nu_inv. +Apply trans_sym_eqT. +Save. + + + Theorem eq_proofs_unicity: (y:A)(p1,p2:x==y) p1==p2. +Intros. +Elim nu_left_inv with u:=p1. +Elim nu_left_inv with u:=p2. +Elim nu_constant with y p1 p2. +Reflexivity. +Save. + + Theorem K_dec: (P:x==x->Prop)(P (refl_eqT ? x)) -> (p:x==x)(P p). +Intros. +Elim eq_proofs_unicity with x (refl_eqT ? x) p. +Trivial. +Save. + + + (* The corollary *) + + Local proj: (P:A->Prop)(ExT P)->(P x)->(P x) := + [P,exP,def]Cases exP of + (exT_intro x' prf) => + Cases (eq_dec x' x) of + (or_introl eqprf) => (eqT_ind ? x' P prf x eqprf) + | _ => def + end + end. + + + Theorem inj_right_pair: (P:A->Prop)(y,y':(P x)) + (exT_intro ? P x y)==(exT_intro ? P x y') -> y==y'. +Intros. +Cut (proj (exT_intro A P x y) y)==(proj (exT_intro A P x y') y). +Simpl. +Elim (eq_dec x x) using or_indd. +Intro e. +Elim e using K_dec; Trivial. + +Intros. +Case y0; Trivial. + +Case H. +Reflexivity. +Save. + +End DecidableEqDep. + + (* We deduce the K axiom for (decidable) Set *) + Theorem K_dec_set: (A:Set)((x,y:A){x=y}+{~x=y}) + ->(x:A)(P: x=x->Prop)(P (refl_equal ? x)) + ->(p:x=x)(P p). +Intros. +Rewrite eq_eqT_bij. +Elim (eq2eqT p) using K_dec. +Intros. +Case (H x0 y); Intros. +Elim e; Left ; Reflexivity. + +Right ; Red; Intro neq; Apply n; Elim neq; Reflexivity. + +Trivial. +Save. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8f64b1fac..564acaee6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -17,7 +17,7 @@ let set_batch_mode () = batch_mode := true let remove_top_ml () = Mltop.remove () -let inputstate = ref "barestate.coq" +let inputstate = ref "initial.coq" let set_inputstate s = inputstate:= s let inputstate () = if !inputstate <> "" then begin diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index f57ddb378..09b10538d 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -172,8 +172,9 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb = let body = expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in let typ = expmod_type oldenv modlist cb.const_type in + let hyps = map_sign_typ (expmod_type oldenv modlist) cb.const_hyps in let (body',typ',modl) = - abstract_constant ids_to_discard cb.const_hyps (body,typ) + abstract_constant ids_to_discard hyps (body,typ) in let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in (body', typ'.body, mods) @@ -305,10 +306,10 @@ let process_operation = function let close_section _ s = let oldenv = Global.env() in - let (sec_sp,decls,frozen) = close_section s in - let (ops,_,_) = + let (sec_sp,decls) = close_section s in + let (ops,ids,_) = List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in - Summary.unfreeze_summaries frozen; + Global.pop_vars ids; List.iter process_operation (List.rev ops) |