agatha.why_Agatha_Enigma_1.v 1.47 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
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 *)