Le 10/02/2018 à 15:03, Ziqing Luo a écrit : > > Thanks for telling me that provers have problems with "existential" goals. >
have "problems" is not really well said. Never forget that provers are trying to solve queries that are indeed undecidable. Existential quantifiers are just one of the multiple sources of undecidability. Regarding your initial question: when you add "k=2" in hypothesis might add "2" as a potential trigger for the prover, in other words it gives it a "hint" that trying the witness "2" might solves the goal. Depending on your initial problem, you should consider translating "0 <= k <= 3 " into "k=0 \/ k=1 \/ k=2 \/ k=3" - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
