test_argument.whyitp 1015 Bytes
 Sylvain Dailler committed Oct 11, 2016 1 2 ``````b introduce_premises (* print goal with premisses introduced *) `````` Sylvain Dailler committed Oct 20, 2016 3 ``````b cut "exists x: int. x = x" `````` Sylvain Dailler committed Oct 11, 2016 4 5 6 ``````(* print goal with h in context *) b exists "5" (* print new goal G1 with (x = (2 * 5)) *) `````` Sylvain Dailler committed Oct 20, 2016 7 ``````b case "exists x. exists y. x + y = y - x" "h10" `````` Sylvain Dailler committed Oct 11, 2016 8 9 10 ``````(* print the goal with the hypothesis in context *) pg (* return to context with positive exists *) `````` Sylvain Dailler committed Oct 20, 2016 11 ``````b cut "exists x. exists y. x + y = 0" "he" `````` Sylvain Dailler committed Oct 11, 2016 12 13 14 15 ``````ng (* Have to prove h1 with 2 exists *) b exists "4" (* Instantiate x1 *) `````` Sylvain Dailler committed Oct 20, 2016 16 ``````b cut "forall x. forall y. x + y = 0" "hf" `````` Sylvain Dailler committed Oct 11, 2016 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 ``````(* print with h2 in context *) b instantiate "h2" "4" (* create h21 which is correct *) b exists "3" (* instantiate y in the goal *) b cut "forall y. true -> 4 + y = 0" (* generate h3 *) b apply h2 (* apply h2 to the goal and generate the new goal*) gu (* go back to the 4 + 3 = 0 goal *) b cut "forall y. y = 5 -> 4 + y = 0" (* new hypothesis to apply *) b apply h3 (* apply hypothesis and generate the goal 3 = 5 which is correct. *) b remove h2 (* remove correct hypothesis h2 *) b remove CompatOrderMult (* Success *)``````