Le 06/07/2016 07:45, Johannes Kanig a écrit : > * goal : will generate a proof obligation, does not appear in context > of other proof obligations; > * lemma: will generate a proof obligation, will appear in the context; > * axiom: does not generate a proof obligation, will appear in the context.
Correct. Home work: * if you replace the 'lemma' by 'goal', both of them are unproved. Explain Why. * if you replace the 'goal' by 'lemma' instead, the first is unproved but the second is proved. Explain Why. By the way, this property cannot be proved by solvers directly because it requires reasoning by induction on the list. Home work: * prove the goal using the 'induction_ty_lex' transformation * prove the goal using a lemma function * prove the goal using an interactive prover of your choice (Coq, Isabelle/HOL, PVS) Have a nice day ! - 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 http://lists.gforge.inria.fr/mailman/listinfo/why3-club
