agatha.why_Agatha_Enigma_1.v 1.47 KB
 MARCHE Claude committed Jan 06, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 ``````(* Beware! Only edit allowed sections below *) (* This file is generated by Why3's Coq driver *) Require Import ZArith. Require Import Rbase. Inductive person := | agatha : person | butler : person | charles : person . Parameter hates: person -> person -> Prop. Parameter richer: person -> person -> Prop. Parameter lives: person -> Prop. Parameter killed: person -> person -> Prop. Axiom Lives1 : (lives (agatha )). Axiom Lives2 : (lives (charles )). Axiom Lives3 : (lives (butler )). Axiom NoOneLivesForever : forall (x:person), (lives x) -> ((x = (agatha )) \/ ((x = (charles )) \/ (x = (butler )))). Axiom MURDER : exists x:person, (lives x) /\ (killed x (agatha )). Axiom Hate_and_killed : forall (p1:person) (p2:person), (killed p1 p2) -> (hates p1 p2). Axiom Killed_and_wealth : forall (p1:person) (p2:person), (killed p1 p2) -> ~ (richer p1 p2). Axiom Diff1 : ~ ((agatha ) = (butler )). Axiom Diff2 : ~ ((agatha ) = (charles )). Axiom Diff3 : ~ ((charles ) = (butler )). Axiom H1 : forall (x:person), (hates (agatha ) x) -> ~ (hates (charles ) x). Axiom H2 : forall (x:person), (~ (x = (butler ))) -> (hates (agatha ) x). Axiom H3 : forall (x:person), (~ (richer x (agatha ))) -> (hates (butler ) x). Axiom H4 : forall (x:person), (hates (agatha ) x) -> (hates (butler ) x). Axiom H5 : forall (x:person), exists y:person, ~ (hates x y). Theorem Enigma : (killed (agatha ) (agatha )). (* YOU MAY EDIT THE PROOF BELOW *) Qed. (* DO NOT EDIT BELOW *) ``````