From 4c47727977f13d6e4946fb78bad8d25e8a22a10c Mon Sep 17 00:00:00 2001 From: =?utf8?q?Michele=20Galat=C3=A0?= Date: Fri, 13 Dec 2002 09:27:05 +0000 Subject: [PATCH] Rearranged tactics in VariousTactics into new modules EliminationTactics, EqualityTactics, IntroductionTactics and NegationTactics. --- helm/gTopLevel/eliminationTactics.cmi | Bin 0 -> 468 bytes helm/gTopLevel/eliminationTactics.cmx | Bin 0 -> 726 bytes helm/gTopLevel/eliminationTactics.ml | 190 ++++++++++++++++++++ helm/gTopLevel/eliminationTactics.mli | 28 +++ helm/gTopLevel/eliminationTactics.o | Bin 0 -> 3636 bytes helm/gTopLevel/equalityTactics.cmi | Bin 0 -> 1067 bytes helm/gTopLevel/equalityTactics.cmx | Bin 0 -> 1563 bytes helm/gTopLevel/equalityTactics.ml | 236 +++++++++++++++++++++++++ helm/gTopLevel/equalityTactics.mli | 35 ++++ helm/gTopLevel/equalityTactics.o | Bin 0 -> 17152 bytes helm/gTopLevel/introductionTactics.cmi | Bin 0 -> 573 bytes helm/gTopLevel/introductionTactics.cmx | Bin 0 -> 809 bytes helm/gTopLevel/introductionTactics.ml | 59 +++++++ helm/gTopLevel/introductionTactics.mli | 31 ++++ helm/gTopLevel/introductionTactics.o | Bin 0 -> 2940 bytes helm/gTopLevel/negationTactics.cmi | Bin 0 -> 397 bytes helm/gTopLevel/negationTactics.cmx | Bin 0 -> 802 bytes helm/gTopLevel/negationTactics.ml | 67 +++++++ helm/gTopLevel/negationTactics.mli | 28 +++ helm/gTopLevel/negationTactics.o | Bin 0 -> 3424 bytes helm/gTopLevel/variousTactics.ml | 5 +- 21 files changed, 678 insertions(+), 1 deletion(-) create mode 100644 helm/gTopLevel/eliminationTactics.cmi create mode 100644 helm/gTopLevel/eliminationTactics.cmx create mode 100644 helm/gTopLevel/eliminationTactics.ml create mode 100644 helm/gTopLevel/eliminationTactics.mli create mode 100644 helm/gTopLevel/eliminationTactics.o create mode 100644 helm/gTopLevel/equalityTactics.cmi create mode 100644 helm/gTopLevel/equalityTactics.cmx create mode 100644 helm/gTopLevel/equalityTactics.ml create mode 100644 helm/gTopLevel/equalityTactics.mli create mode 100644 helm/gTopLevel/equalityTactics.o create mode 100644 helm/gTopLevel/introductionTactics.cmi create mode 100644 helm/gTopLevel/introductionTactics.cmx create mode 100644 helm/gTopLevel/introductionTactics.ml create mode 100644 helm/gTopLevel/introductionTactics.mli create mode 100644 helm/gTopLevel/introductionTactics.o create mode 100644 helm/gTopLevel/negationTactics.cmi create mode 100644 helm/gTopLevel/negationTactics.cmx create mode 100644 helm/gTopLevel/negationTactics.ml create mode 100644 helm/gTopLevel/negationTactics.mli create mode 100644 helm/gTopLevel/negationTactics.o diff --git a/helm/gTopLevel/eliminationTactics.cmi b/helm/gTopLevel/eliminationTactics.cmi new file mode 100644 index 0000000000000000000000000000000000000000..6283bd6b3b0e692da50581f7085a14266b0bc4cc GIT binary patch literal 468 zcmZ=x%*`>hw6ydzFtBWyx@;c<10xdy1A`?H9|z)X3yfTIGIKNY5=%1k^Fk7nOEQy- z7cAINrJD*AjxVV!NR2N^OmYEkZnO&cd{a8P#6Om+nG8U8y=aA0En`jCO) z4@Ax&peR2-%{4DQGcPp+sJ+-x4QK$+SR|!?p<4bq0IjOlO-W78&n?I=hFhhYoRe8x zvSHJN4W23>7SMX!_Wppo;3x4e_yu*rZwCiRs4&a}hK2|b2LZ9u0&KxzutkjuowHzpR%lVCZ(?3zdTNmYhjPZ9xmRZ?#?KI2TqY+Q29ym*Ehhw6u&gFtBKux@;c<1Jg1F28KWe2F64nmgHbyP+%}}&B@Ho%u6iE%+Cu+ zOfJbxE?&UGA9k*>trq1@PVii?Kog=WF{jwz2~Wt^^>sZV zuT|>PZ!Qe;U$DR+pa^JMNoH9p)GUMl;*-1FH@tJ%cJWcs;iH*%7A&v|D9X=IbInW7 z%u5X}DJo4aDJ@FO2`bG=EjDms+17GY=E}#-pJeV{{@v}iV1bTvW^zz!3Q!f$fd=-X z7cNekxTWk~my2SXoVPvLM!0Dql?6aEyu6Cm2Nh1c?ym9i+rIMo-xe%T2AW~;zSeQB zvFjpMMTx?qKBmab1q-wSQj5wGi-C?UHn4wu(580N&obw@+MXx5{O^IXp+%X#iFt|X zsYM1H${Ba&UY(^FKSOMBnVf9cf(2ND&0yDU>%tU~)uCMHQ`g7LS~>?9h`{hbbDf_0 z8GWyRQNbThtRElh&XZ?bfA-(hAJe)w zv7m?3syEe>_g8Z`-Qx0Ny0coe2PN7H--Q|rOym6dX#JDk3!Dae*rIK6pZ=8h3qzI8 zuKBRuKqdMUG!UC3e)de_tZ4KxH1vEj@urN!#03iuaH?RYq4@YzV7iJg0mevtNn&!m yshN|bg99$LDXGc%xdr*f5VdATV6_Z?7dSaMIQ(xm@AXsO;$QaWYvohx(h2|`B{RGL literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/eliminationTactics.ml b/helm/gTopLevel/eliminationTactics.ml new file mode 100644 index 000000000..d2ed74810 --- /dev/null +++ b/helm/gTopLevel/eliminationTactics.ml @@ -0,0 +1,190 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* +let induction_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let termty = T.type_of_aux' metasenv context term in + let uri,exp_named_subst,typeno,args = + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args) + | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate") + in + let eliminator_uri = + let base = U.buri_of_uri uri in + let name = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tys,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + | _ -> assert false + in + let ext = + match T.type_of_aux' metasenv context ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.Type -> "_rect" + | _ -> assert false + in + U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con") + in + apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst)) (* come mi devo comportare con gli args??? *) +;; +*) + +let elim_type_tac ~term ~status = + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.thens + ~start: (P.cut_tac ~term) + ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] + ~status +;; + +(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-) +let elim_type_tac ~term ~status = + warn "in Ring.elim_type_tac"; + Tacticals.thens ~start:(cut_tac ~term) + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status +*) + + +(* PROVE DI DECOMPOSE + +(* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *) +let decompose_tac ~what ~where ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + + let rec decomposing ty what = + match (what) with + [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *) + | hd::tl as what -> + match ty with + (C.Appl (hd::_)) -> hd + | _ -> decomposing ty tl + in + + let (_,metasenv,_,_) = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + T.repeat_tactic + ~tactic:(T.then_ + ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what)) + ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *) + ) + ~status +;; + + +let decompose_tac ~clist ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *) + try + let (proof, goallist) = + T.then_ + ~start:(P.elim_simpl_intros_tac ~term) + ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *) + ~status + in + let rec step proof goallist = + match goallist with + [] -> (proof, []) + | hd::tl -> + let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in + let (proof'', goallist'') = step proof' tl in + proof'', goallist'@goallist'' + in + step proof goallist + with + (Fail _) -> T.id_tac + + in + let rec decomposing ty clist = (* term -> (term list) -> bool *) + match (clist) with + [] -> false + | hd::tl as clist -> + match ty with + (C.Appl (hd::_)) -> true + | _ -> decomposing ty tl + + in + let term = decomposing (R.whd context ty) clist in + if (term == C.Implicit) + then (Fail "Decompose: nothing to decompose or no application") + else repeat_elim ~term ~status +;; +*) + +let decompose_tac ~clist ~status = + let module C = Cic in + let module R = CicReduction in + let module P = PrimitiveTactics in + let module T = Tacticals in + let module S = ProofEngineStructuralRules in + + let rec choose ty = + function + [] -> C.Implicit (* a cosa serve? *) + | hd::tl -> + match ty with + (C.Appl (hd::_)) -> hd + | _ -> choose ty tl + in + + let decompose_one_tac ~clist ~status:((proof,goal) as status) = + let (_,metasenv,_,_) = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let term = choose (R.whd context ty) clist in + if (term == C.Implicit) + then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application") + else T.then_ + ~start:(P.elim_intros_simpl_tac ~term) + ~continuation:(S.clear ~hyp:(List.hd context)) +(* (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)*) + ~status + in + T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status +;; + + diff --git a/helm/gTopLevel/eliminationTactics.mli b/helm/gTopLevel/eliminationTactics.mli new file mode 100644 index 000000000..00ccedd64 --- /dev/null +++ b/helm/gTopLevel/eliminationTactics.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic + +val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/eliminationTactics.o b/helm/gTopLevel/eliminationTactics.o new file mode 100644 index 0000000000000000000000000000000000000000..ad369ef75fe65a923c9dfa4c027ab3cac18120c5 GIT binary patch literal 3636 zcma)8Uu;uV82`EzDOuuUwV38QWEFK~&ZV8v> zBGi=$=-^LE@gN}V@X?aegi7_3UzN5sIaVWo1`2C*xUeT&ZpaBGa9p}iIgcV3h0-EE z52&n0%f}a!F?qNTmEut+rhqwd5lR?RvvS`0$b>g>tRPyF95{<;sR$(c>;f~wPw;9%368zkyysE2UD4Wm~F-S zTy4zCK_5$Gv*}baVW+H&NDZSk;P*bH2xt(=e4%6}MOG&>Wd{DU^)d(gC~U&8Y*sR} zq)h}CBH!Z$h%zCqTdHh=6^jjO9!l7EX*mdawUSu{nTV;l$OXtzR2NbaMZQ$r@y8rS z6?b!>M&v!c#>q;=Qoh_A5ThkOJY*-f1MQrHgRYb_(=E2S+m;qeeF-}uE!*>Xc>I53 z0n8Ata=OL2jAiM;{5a;~H%m#*<66DQOISD)l`{11a$Wrkr{5^_=W(F?&zN@SL@*!oc!^;4QE<0L&Tj;F_k?_Kn!Sh(9@hnO z{mbAnZA1HaA@9}6bN*ZKR?qw|kYg1dkPvL+6<#az!FxQsUHhVn{`h}+sxlvt;c4?Y zw|)G8k00^zV?KVy$G`URt3LjRk1zCWKKt0=<7<3;osU1^;|U)x`1n2_KjP!3z%ObY z`}YmxzdZbR$a^aNtd%;vLVG=2y3?tlR7M?*n-fVpmCPFkj{#%5IgrX!olaVP<}IhI zu2?3?#8BEu7IL}awyGAD6Wg#8Nn=HIqv~1{6&Ut#)>KP7R#f%Bys9=iXyNKGR<>51 zZLg~BsH*KRWQ=94)#s*avocPSD?4P^Dr5$Xtew*mx50MWWEXH-^$#zX-c;T;jQ&)n z&uD9Fm#$QDquE!$CRrK7*frQ^bhgTdoMrWQXRuf1X7nKMxG;Ao&8)J^TB(d}=Cm)Y zL2ozY7%a8Ztn9ezAq;a?-pHqhvT4=J_V!kBOcH6l7WSZtxSef!GZX2wF_2_d|8h9B zYD#j}=hINu**R2K$R*Mn3u%<%iJddEX2NDxctwp>)wk0`0mD_dN4>IUrmyOx zdfjg|*`G@cnYc95reyKI3EUyFTjR6DIUKBRgMP4B; z5P6k|cyDTan}~Ry6K9L??4!R6dj68e%S6~U;p||XB^rByjPn?Ap~&Mz#M??lyguUn zA}J!i=`uvb->GpA5q@7F;yye~#Krp=kZ~@Nqfb8*aj%XOaiQ}JBj1L+YVaYk0K6t9 z@+t8F=RTu9v`hlHcrm5?Hxu!l!TX8xokaM5o(NwDH6GP?T;n;7=QUo@cugaYS+zc* RF{-gyW2Z*$7vnH*;y=0iyTSkf literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/equalityTactics.cmi b/helm/gTopLevel/equalityTactics.cmi new file mode 100644 index 0000000000000000000000000000000000000000..645ab0f51a0f51f4e6ecb1b0328ce4801f285153 GIT binary patch literal 1067 zcmZ=x%*`>hw6ydzFtBWyx@;c<19J=m1H*O(2Bvl(4p^Y?T3DKxlUY(3l9*hQnOwYJ z!3G8g?V{B3qRf)i_>#nAhXorBsFb7@wbW(b2dYh^#1l~Wo_H61fV$`-l>P*EnX7(LYFbWeMP?Z=y+H#XoT!LN zIB&s5xakyE=H{lB6p^g|4OqXsK}k_!UU6m#vKt7d@0Y~;{1w#4uN@p9`Hf*VFu#ca zaUc*oF2Kle24z*toU@L8Q#fzYu%&s5=Z^&ov_gwAeG~H%(^HEKIFvK)%)L5GF@A>F z;xakeFraKeYEfBYab{U+v4Q>LgEqCBewI1M)%HBe<$u3m0VswI-q$+LHFjOZswh!d h)W;N=xnKcC2pf2L6|D~{oOaz^hw6u&gFtBKux@;c<1M6!B28JyR49o%y3{3eP3=9ek`mTkgi8+}il_81A zC7H>^3s{&O7A!CbN=+#R^7Hec!UhU64eRQ-7QZ$;qqP6p+!ehG7MKJS<>#ll=A~!m zrNWgPyj)i%bYYIk^1tG&Pea)FE-qN0;*(iiV(@FLaadjJhn;I|t3|n!6Fe6zF!szV zDauE)Mt)h=PsKwG`Kx7a-SN8f(q+K{edo;N;L@bxlFX7)kb?}ObXz*3XD#9g_WsFe z=EiY;!2(sFl7Iq(wQYLQTRwZ7sr|t0Su&$dX2AkYi0cz`iVdFdgnV6J*Awzur9S=U z!Z7~@3yhH5?~$5QkXlr1pmp@iikTLzy63Fy|3s%B{I6RKjVJa_JDb@z_1D^%FN9y$t+8Sh1GxY$zARn-nneM_^9ac(abvw7FZ$K z6*h4U5-TbieM{#dX;Do!2)HV#|+-rI?gqAUBs#=QCQT+6qyOs6k3$&o0ylF4)iOBa>kvxS7#~4 z&k$Q&CMO%VV1W)$6C$qdMK4^OG;vGWy)GBUHaTy5V8TIFurLsrN@aeOR8sgZ)L38|=g&v$pY&efG|&UazhiN6YEemi z8pJ^?0@xyaa-aT`_X|Un&aU~e-asY#6ZXWlSH=0s3$?v1yMo!W!evi&z!UDIx!W^L zH&;cxne@Q!1W%VTYSg{ELigOB#}ucVw>BeCIuLsoD(0F^3@g#Z8m literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/equalityTactics.ml b/helm/gTopLevel/equalityTactics.ml new file mode 100644 index 000000000..afa210119 --- /dev/null +++ b/helm/gTopLevel/equalityTactics.ml @@ -0,0 +1,236 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[]) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) +;; + + +let rewrite_simpl_tac ~term ~status = + Tacticals.then_ + ~start:(rewrite_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; + + +let rewrite_back_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[]) + in + eq_ind_r,ty,t2,t1 + | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[]) + in + eqT_ind_r,ty,t2,t1 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.alpha_equivalence + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) + +;; + + +let rewrite_back_simpl_tac ~term ~status = + Tacticals.then_ + ~start:(rewrite_back_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status +;; + + +let replace_tac ~what ~with_what ~status:((proof, goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let wty = CicTypeChecker.type_of_aux' metasenv context what in + try + if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) + then T.thens + ~start:( + P.cut_tac + ~term:( + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; (* quale uguaglianza usare, eq o eqT ? *) + wty ; + what ; + with_what])) + ~continuations:[ + T.then_ + ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *) + ~continuation:( + ProofEngineStructuralRules.clear + ~hyp:(List.hd context)) ; +(* (Some(C.Name "dummy_for_replace" , C.Def (CicTypeChecker.type_of_aux' metasenv context (C.Rel 1)) (* NOOOO!!!!! tipo di dummy *) )))) ; *) + T.id_tac] + ~status + else raise (ProofEngineTypes.Fail "Replace: terms not replaceable") + with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context") +;; + + +let reflexivity_tac = + IntroductionTactics.constructor_tac ~n:1 +;; + + +let symmetry_tac ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", [])) + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", [])) + + | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") +;; + + +let transitivity_tac ~term ~status:((proof, goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let module T = Tacticals in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + T.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", []))) + ~continuations: + [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac] + ~status + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + T.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", []))) + ~continuations: + [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term] + ~status + + | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") +;; + + diff --git a/helm/gTopLevel/equalityTactics.mli b/helm/gTopLevel/equalityTactics.mli new file mode 100644 index 000000000..7d57a0c11 --- /dev/null +++ b/helm/gTopLevel/equalityTactics.mli @@ -0,0 +1,35 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic + +val reflexivity_tac: ProofEngineTypes.tactic +val symmetry_tac: ProofEngineTypes.tactic +val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic + diff --git a/helm/gTopLevel/equalityTactics.o b/helm/gTopLevel/equalityTactics.o new file mode 100644 index 0000000000000000000000000000000000000000..7686b7d23d0616a64d8c5a920a3c8b86d57adce7 GIT binary patch literal 17152 zcmeHOdvH`$nm?U1&_b693S*S0tu`7Rggkf!aY+bZ6m$XvCPeVkBn|1c^Ptn=wdeu? zwQYI^$4AZXP&=TO<<2@gII9*aqcEVsSyzXZowa6lR~*;n;e*--gPMW;{m%XF?b|mu zfwHD*_YZHS`*(il@tyB{=R42a`SY1`X8C+RWj#KXud+<3@nJJ%yoM5Wff{UO)tGJ! zR=!*C$lih%_GbJuS#p2o1*T;7Tt_&M^z@znJ|b5AvC4OUQkt3(9+95yPt6Gzrbnd~ zhl9JRnEpc5hzRUtMEB7VPY`b!#P5PljlfKmzo)AA_k~LJFjDnY`M)}Q_H0j8fGkxT zJlYG23RJp*lKknBv{!mYIFOzb9-&kJnno$u@^^rO7aDrIzX}v=c?u*Q=>Ec2u=z&} z`Xtl$>`X%owrpfdgTMPLU%{3x9S-PljNz63?lUO8gyDt$?k^FZ%kXV}EtNfyUSyW7 zWcX5O7fxS>?@;;*d>5w`)GpFi&}ya^hl?ur=k#RvX6#$y z97@*&Xzp~49}wP+^2&4_Hc+Lj0_kCA4K;t!SoHO5;Q2?7)Uh)Fw3MGf|*5iRvEfm zp)Rx7s=q!wB2{QP=iC<7%g&33i&8hB&P;U@IrCUyDU>Nrb@(&SZa`CeW|?XXPA&9j z9@@$nvuJ8cDuFyd%;rI*p_Ig*x-xgS$+p!-1Z80Y41=Kn4B{2$WufB2jE zf1oAloB1CD>6`igoB1D8a(40le?9+WyX zO}vs-HupI2xw)~zntrb1fcq$*upSlZ^$xWZA6*A+Q?I{_ZyJ|gF`hranTL-;$8DQUOulK2wx%<(x6IfeH?@=9x6`YEoWwF+>4ii90oi>Z+ zrb-2yS7I;Xsn%X3Wc2xGgzUc{p%4d*{GJ-U3*3p#9*-N`_M1}+mT7Ct8%STy4%GE= zO-E8;dUlXGOru%Hj#9^-rC?JvE3M*o8k;(EhgO6#Be*BT86tfrj~~HIUC`R-;mnh| ztY^BpEv+rGcB?oLr7lg)^=BHw+;n6c5KiT%X8W^du#Z3C96f#p-Oc^eP;6sUm&(Ss zr#b)yRc2A4wI$^S#oWdgLt(wuqrySE&2z#fy1^%AXOh=i`ymg5Cnjfid;^|6D8@X8 zbRWRJEiC)CXLK#c#@hR~?Psk0*yVO;y}g6`4BM!TeIDojY#&CFJ~wOQWWPk$+;P)o z`)t4CrXh%^vID`S=ys)ILN%3nGVTeV(=s(SKoQ!XbJqGsz)(gASXA z=p@7D0eN!^!*}Y#^5(^ka9uXMWd_6aVbf8yw&*?Oab#Y<6CICZvU8VSu&D_G%t4~E zKIYfwVtR##pXHXnl;!nxM9wjrI#_#M_BVXkp`kuME06Q@8c!Ynh90X2^4HNZ5j_w6 zJnBtcdw%|G4vtq$?_FhV0-U6JJbR{mJ5bgb+>#{$ccz^L)LM#A*A_5#auV8 z&9}@ykQa}Cg| zbO1LR`#k)hVAI<^%m4h&SyN$r=={0E&z_KT2MR}dKaMC$bpNdu|I_YY(hWyK(htl2Z- z&R8d{1zA`Y6z?xNhd+#qthe!D|3+7KMdIk&`bbkU*3>z+H4b@*zXnfe zehk_qW9!yMlI>HV2;}TSd8RjawYIJ`mbWL2M09l`mW(QuXVud?o;vH;DWPObG!#j! z=xU9&B||Y&`$(uG(cZp1guh5z$Wmcozk=-z_=@cZVNd&?cRxi}+S1N#KiF*-40zqQ zP$xcL$8JYa{{PZ$M&ge%9!YoF=SwPL9c7P0STV{3aoU zBPU8(@^Q8fl&aJ}UCesTI#}~-;LdtWHK)#I{%c(6m$=d^MK?2lzUsJ0@eP7ntr3F` zZ9Fxcaa=B7Pl;##ztZt$JGdI99cAV@$~@{Q!+Ek$&kB^F)C$dMr+{j7rQP93`>~ec z*ZJ~crJollRf_WS1!rl@gX|LZq7Dzz79gjF$1h}lvz3h7uk#Fn?TTQ}kP1t_Wjf#B zocMVNgOEC+%h2N4INEU=oT^Zdhk&|Q!pzg@2!A;Y z@41m@3`+YDKOPu!#5L%!Pp1#l>G-m3?XYX&=*n^VKGF?|A$I zp>LW}cj+{@UCoje1IRo9_v%mP8#>Kf=G8ilK4^_O%u+fo%Wu~84u-dxv#9n*6tVqL z!rC7l;V&^s+Wv@m?T?PQ1|1fE)aj_mp+|P?!5=X>4Cs$K-Q7mhU*8!Z?X3aQemOwe zNUd)_{;13KPlUKMo-C1eT%x zWWJ%(yk%ak(;(R42fXSW@8CD@qwvj9Z9Ti;@O5Y=hLbMOT?c3O>xHA+^z#8^ zg=h|W^gamT(fBy!1*R!=8igp2Wi5H*5T;y99u~=*$C8JoKAVR*kdI^1de}xjMD8f8 zXFC+x0h_Z9%HoG@rfznf2u~fO)LLee$C77pFUtR_{S4ugSeN-Q{~=(lW@i46 zBut?Ellbi5RECH7hrR{Hax)BYhwE z1CI2=EN^q4`fup@2{*MUnaPW^2KIq_IBK(1aUuX?7 zR7m?@4bJy0R{awZu5$3(5RNTMzwzh>Kt3;>9jr;^Grse5Q-nyZCAsf7HdFa`9id_-|bNgo|^nw;r}{ zl#7?R_*55fbn$gA{<4ezi;I8m;%8iZ7#9S2s9&**m$>*;7r))bzw6?Li?_RYmy2(7 z@$D}Dw2SX?aqd^Ghwb@S7e51DCF?Ke*O37$H~kmuE4Z~jGrb1V@d znS04)7~CTm%c3h{ZGF?4+MA=^X?^pSsisJ4+-T}bB-WPqP1bjza(QYbBTYux#PNM| zm77A6T^;e*axXF1`RMyhQ^bU_z9K3ddQ|jHmfJ$Je8t4R89cO-YdvFGr0H&>GuGM> zm*O7sC-jw=Q=Cn&^r+S&$|{$wvC^Z$N&Q#Ix+ZuCp4_)cW#6c>Qja(fgO_>qcA1Bw zWgeC-^DtMLhsI?dtt|6sMwv%D%01dq?$M5Nk9L%Mw4>ak9pxVFDEDYbxko$7J=#(3 z(T)m_c2sz@qr#&d6&~%V@MuScM?1U*Nrgu{Dm>az;n9xq9_?7()n=4?O$a(+l85#> zVX{Y4%>)nI>x9a3RTFDc3lg#0BW;lt(S%yt-qp6k=tx?jc&s&+%$bHN)SOsn(lD0e z&fO?S_d^2T@6@zJo9>2$Txu9eq#5nYjY!v;aQP&oY;viiKEvor#F&Z`TMQLfpu6h$ z24H3zrr;>$cAB+E*EB^tlCkzSqobWKA9O|YyOwn(W63TZZ(x#48WVE_%!@X6;q?XH zH#wx*kp^B-=$9*jf&D79crWTj%WfU+oG!tOxFPkf7^Sa{bb<@jQn%SeS`a6wDrR*SE=Nw`ft5FJW=GM?KbaS+c z$}2s_JItS0t8T@2yUQ4T_6d3~fDZ4wDCix8XUg(KguTc&b9kP|$M+{ny+p+M{&ixN zQf~O=BLO8tlM&&aEk zIwjaktX66P&O5$|N;LvmZY}u)rFfPj=MOztE+hCb5#^2uKPJeZ7czcOKJXT$E+pcT zVFa;Osmla!0_NeMzEE%l<128EA>O7`7vpCuwVoXHZWery2>DME%W z1APmXS|-@e`0v6#WEuZKSo=}$oI zPvj-=Cvy4|k^V%aKN0CqK*~KWc!mhM^>~G%{fS6_0y5uf!F!0v_kAM$iFh6SiHP<+ zF8C}F1GPU1wlkjoL=NBBMT9>+PlP|c zL|lX)q!1hNo|6c@-WU8G5qf<=gntbg3cLwF5(DPd;A~2c`RaP|nMzfX->K9L;x)Ke zVmvPF7Lh}4L~sQWa_=GDqSSrFt8vdngq?mM_@v-Z1b;5LTksVk>VF%^`hQElM5%ux zzYBMFdr<$zh+{h}Yu14dY?AC^^cv3U(4v{s?ijQXd03 z9zK=y{}KF(hSQFf@gs2=X@NXeamp)L_~k{-ka_1or@G z*L_6T^>rfb`u9YPpTk7x^`78|MCf;#2>TAc7 z7qoLksh_faz!HV>0rNK(KCD653MwDg2AER+CIBW;KFl?BM2vZe)cKbZA-hF*2N6EA zM)(FI>Uco-HsU47p9jQ;_vyqP`6hl~pbf6)~@DahZiF+PZW5RrGn#4&=C1#1QQ zu9)e~f=R*6f{zI95ZooWSMb+@9|)clRIo4Q777*#h6PInd8f;Ka|9a%n*}=rHwbPO zWdE_;(}KGN_X-{q)cZ2zJ1Si7%cvK8f#t)3yt^f@7mN#T7UW$k)1MRM-75KE!J~qF znaB8`V3A;0uvBoe;0(b!!4AP~g3kyZ6#Ph#F9}&svEXFEdch9Ct%6Sr?h<@c@Tj1l z>oMfaJ}F*!R>-i3qB{fSMZ?VVZjds`4bpjpWswM{+5RENx^M`&j=nA o{74W#ozVG<1t$wu3F>_qhw6ydzFtBWyx@;c<17j8g1A`Bc<^s~+78rZxl@#TtlqQ#C=I4bZ0;%NU z1q(LR>L=&t6_*qN#q*2eOA?bE7Hl}6n73imgbj|$nRz7+4ig-hSie4GVED6P)5ZxK z91H@A^7GSN^U^c(QbQ^WQi~ncfVzODG5m)s{R`Fd&jDydomOf^W^qX|)NrB=`3=%s zuUTA>lUYKl-d`ZS3=SGOsc9tZ{R!6Vs9BVmo=)PsKwG`Kx7a-SN8f(q+K{te+;1L;fv literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/introductionTactics.cmx b/helm/gTopLevel/introductionTactics.cmx new file mode 100644 index 0000000000000000000000000000000000000000..bf2bb17cf5030b772de1b942750736bd922665ec GIT binary patch literal 809 zcmZ=x%*`>hw6u&gFtBKux@;c<1Jh3i28JpI2F8m(+{MAbpuk}4nO9PjpHiA!l9`_u zk_e=dix;pkIV@P9;*(iiV(@FLaadjJhn;I|t3|n!6Fe6zz^21Mep%K}#X}AGt7UH8 z@w)TUWx)c2fTH~TG}pZJ%)Hc)%7WBl123Fp%SfCYA_ETPj5~9$&Qgq@A-1?oPBv`8 z0v({Hpj4=z4eUiPT%0s^j*b%+EZD%{rB+;$SW;T-;IN2=Yr(_`6C4*zVBrKCqKMUy z;)0ya5{Mb5P&0gx%#cJiLjkK9IjLz-Bg~;j_#qjgfocSHXB1_oXF$!cgqjh6WQIA& g3@4~poE9+rb#QQyW-H~)zY>zByiq-Pk#{UR0K-{G*#H0l literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/introductionTactics.ml b/helm/gTopLevel/introductionTactics.ml new file mode 100644 index 000000000..bd29f4f5a --- /dev/null +++ b/helm/gTopLevel/introductionTactics.ml @@ -0,0 +1,59 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let constructor_tac ~n ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.MutInd (uri, typeno, exp_named_subst)) + | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> + PrimitiveTactics.apply_tac ~status:(proof, goal) + ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) + | _ -> raise (ProofEngineTypes.Fail "Constructor failed") +;; + + +let exists_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let split_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let left_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let right_tac ~status = + constructor_tac ~n:2 ~status +;; + diff --git a/helm/gTopLevel/introductionTactics.mli b/helm/gTopLevel/introductionTactics.mli new file mode 100644 index 000000000..c3a12720b --- /dev/null +++ b/helm/gTopLevel/introductionTactics.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val constructor_tac: n:int -> ProofEngineTypes.tactic + +val exists_tac: ProofEngineTypes.tactic +val split_tac: ProofEngineTypes.tactic +val left_tac: ProofEngineTypes.tactic +val right_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/introductionTactics.o b/helm/gTopLevel/introductionTactics.o new file mode 100644 index 0000000000000000000000000000000000000000..0f67a41747080f5ec87a4a950aaa35120fdbfedc GIT binary patch literal 2940 zcma)8UuauZ82^&ou4x-grgd&^&I+~Gmzs91v-)6MtyZm2rNTA~*EG3lFQiF!b2A$e z)|olI+(io;s7#TeJ_tVeFiIb$6f;(RQ+z4H&<7tnrl26U(qR34=bmJ@;TC(~-rx5- z-=Fh+=bU@aJvBV~l+Wj*TJuqWZZV?Q1CFL&KsU9}u9~Sp`*>(@C46Biys%VOhS{@H zUSLi6$^#6g-y+tNogw=<#TxAl+WW1EPGyl5;&n-wthRr`_*fIa!*6hua!gr{Ro5a! z%iKxJF=blvg{=K-&_1r%e(Rd`)6JH7dn9O& zDRxw5-mxX~({L;wRhEaUgglXqVg>LHT0=^CD1?IAP>>b15MaDBWQ_$;NapgmP(-C$%y!>!WrskG3WjmazMXb|mv4Xrgpr z6>*2MnY?Kf5@y!uNX7NEmUOl<@7Q@{!9%|%a2F|<%@Dksv7+BY`iRa6&XqYm za}D}SB1V(c2Amvv^2Hf5K1n@D!NKX8WN7IgQ=2uZhoxlPj8o5KK98t7Yxly8C$aYB z#UMxhc*(}I%xyoO79lyWzd*X-*bK`4ToF(6gOc-HbIT#tiX)1**jkWybGhRkXd`+B zeH@Q{Yw;d}%yDb+Mrs23xYgqAhU`|copY`Tv--Kixw^`uUlD-oInMvJt*0Hwb4O&}RL_fJMbLAfD`*7TC%|hpvi>FT1JZ_h8uBkP8Mc21yxXP! z4D$Cb{Wb8~ys-au@Fkai6Fi288|(K#_oYie2zk^|3;meXIrc;o;2m|nkIsNk)Omm| zZn5_{UvOPdbY+X4=(`5~V*~%Wf&bpXs||d&YYlmwdmH$X27au8r@;S^F?qgEgLg|C z<{v}O)$0k+SKy|L(=!><$R=@+=-JG89FWMXDu1`?q&B5zy!DA}Qrlkd?bGYsZRk_e zrfS9$>fu3ei$3q}w3d>7hrJCBd3Wb?Xu_zFwx(PxCA#CTR91bH!hw6ydzFtBWyx@;c<0|N-F193MH*DcWZOHEHK$;{6SNlY%uOfFuqU_+Hw zVp4HwQA&JCVzR@64F^<8Qj2moY}z_1nP# z>Z92}pNIf)AP_q)!0?hm(9gZyGuTs>MlF+lRGYnN!-54`p+%X#iFt|XsYM1H${Ba& zUY(^FKSOMBnVf7GP&Od7s4THKvn;jP!2a<;o7zo3%beqCd!FR-zhAHb6b1(GYaQnr nyDnl?lqf9fV~WgNumHo!23}r8>w^lXU3b^`_-$YL{BI5bLo}al literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/negationTactics.cmx b/helm/gTopLevel/negationTactics.cmx new file mode 100644 index 0000000000000000000000000000000000000000..bb903429438578abe4e37b17dfce875350d215ef GIT binary patch literal 802 zcmZ=x%*`>hw6u&gFtBKux@;c<1Jfr428K8W2F5-hw&P%6P+-vaOHEHK$;{6SNlY%u zOfFu)!sM`Efr?LNaf!jNt;S(>tsi!-v8@*6PEPP#us{={DlwrbezuDOu>d(HL>3l^YTW)SpqZ}$xLl%-M2 zWFOULZ`!b6fk8k~W^QIlW?3rCnE&FFyWBUtbJ=$BQPJU}nRkE|IcFw^R2HNS(G676T3nGo6URul(+boz4==C)Vj0+B{mA* zg&GS?fKYJ!|Ry6t;8hSpNcvHq<;(`SS?9h^Ae0*Y3acNOXd`V(*ys4R! zql3eO1DvWDs*>~bN{SLwGJ)whKM$ m=goal) metasenv in + if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) + then P.apply_tac + ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status + else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") +;; + + +let contradiction_tac ~status = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.then_ + ~start: P.intros_tac + ~continuation:( + T.then_ + ~start: (EliminationTactics.elim_type_tac + ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) + ~continuation: VariousTactics.assumption_tac) + ~status +;; + +(* Questa era in fourierR.ml +(* !!!!! fix !!!!!!!!!! *) +let contradiction_tac ~status:(proof,goal)= + Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) + ~continuation:(Tacticals.then_ + ~start:(VariousTactics.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) +;; +*) + + diff --git a/helm/gTopLevel/negationTactics.mli b/helm/gTopLevel/negationTactics.mli new file mode 100644 index 000000000..bfa3e8d5d --- /dev/null +++ b/helm/gTopLevel/negationTactics.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic +val contradiction_tac: ProofEngineTypes.tactic + diff --git a/helm/gTopLevel/negationTactics.o b/helm/gTopLevel/negationTactics.o new file mode 100644 index 0000000000000000000000000000000000000000..2c872a7df82832e39b93165e1adebc602bc25490 GIT binary patch literal 3424 zcma)9QD_`h6urCI)FfS+R8yO3wW)5kf+Tj6*0g?@kVI0NmMB$fEew;%BpJKe-R#cB ztbVjKMOc?b3l&5~TSP%EDhRdEDwR|g=}*O<`XQ(vl2Sj5Z7~|pdGj`z%tr9R?78RO z`|i8QDRoE6 z-San_M9Nf3xjXXL!ootiyN;}IAX>OQHxC6Ch!oewper7T6#HUQ9E{Z|%Qzi})S8OV zT&kP76>2fSk1Hxy^&H+3rem-(+e#{^lau*(=}D%pSqtqe$*E~ z^N`mlmGOO83Ukpa3dJq_eO>i*R(0U|Hwv!pN8dc@#y=G)3(4EB;9hYHRh4YDN&$km zmnz6&-A(?yc6)g>M0G}NAvTYI+N8L8;Rj%(xF=dvY3opEMIE}1O*Ggrf z7V#vOd5#fhOWagp6Ds4TmTRE6i6l5wD}eK@B9>$AYVS==w(m|lZu?+r%(2>^G80+5 z%}I`kgy%Pk^bBWnnUP(s`%-SJ**cU-rBhkQby7*%|09N}=CoOG3e_M%rpLh)o(_vN zOBiWJjE3!s$ID>zyZI!s6LAw!N zQE5_h-ve(3uh@@k&gL=4%W6LJAg@*Nr7fGEaLr+$oAGeGB4zAEn`=+I(ne{-bWLd+ z&So+H|BX#>!;*_9OE=^SNU5nqb`txl$wTyOp2k zKz<0~6`c(IkAdUUQG@n3wM<}Lr}4Dn;h_IT;G-lM^#2h!q?pHlhn)8D+mKKCc+}Sj z#)~cE*oOe`2=KlD-xuHq1AIKdUkdP71N`Fv|2)9Y2l!6`emlS$eD47JxjDew0=z50 z_XPOC03QwTm%-Co$Nrvx{F;w{3i&PHetZZ1u8+$;d(7mSx!<&0$I2Q8&j@4K9&?h_ zHY+t^uWYOK-Bzu_sq1FU5eF-!l7?$q#*VIPueey|M8dFgnM^)jZT3!ZHGBJxYI8@m zs`@v1Bh!%U|WdDXZ0&Q91|{elgec)T~QO&n(?K1C~e$M8b;R&8*Ag` z$XD-+dgp9h`YXSwD_TY~=7f!#Fk$mm=lK=F1+a~Hr^pWCT_Sx%T-bvepCPUj87JN? zGDXBkd=wa7kMD}SMdWSr4I=N8H;Q~nyhr2{>TwaCCr8{_jo%Xyw-#qbXpKk%FpNWZ zEjj!)Xxv1E-=yYwjYqWp1o3{XPi*k+*AOn~kH~>%fZh(7#A zL?5mbH;ddLJ|OZp5%+BvX9e@D2QtsK8rKt%=K%3Rk-flhOk|9R^(U#v1vy2;za*~^ zad98j+(P^?F0x_pFfMwYlOf!nyq8!PLP>~!KM>)2M&kvIS2X^jaZckcjr@Or^O`mC M&LQvA$UBAnUw2J!TL1t6 literal 0 HcmV?d00001 diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 615cf43b4..604307cd3 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -65,6 +65,9 @@ let assumption_tac ~status:(proof,goal)= (* ANCORA DA DEBUGGARE *) +(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda +e li aggiunga nel context, poi si conta la lunghezza di questo nuovo +contesto e si lifta *) let generalize_tac ~term ~status:((proof,goal) as status) = let module C = Cic in let module P = PrimitiveTactics in @@ -82,7 +85,7 @@ let generalize_tac ~term ~status:((proof,goal) as status) = ~what:term ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) ~where:ty) - ))) + ))) ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] ~status ;; -- 2.39.2