(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 First-Order Logic} *)

type being
(** a type name *)

constant socrates : being
(** inhabitant of `being` *)

predicate is_human being
predicate is_mortal being
(** two predicates on `being` *)

goal socrates_is_mortal:
   is_human socrates ->
   (forall x:being. is_human x -> is_mortal x) ->
   is_mortal socrates

predicate is_a_cat being

goal sophism:
   is_mortal socrates ->
   (forall x:being. is_a_cat x -> is_mortal x) ->
   is_a_cat socrates

(** {3 Drinker's paradox} *)

type customer
predicate drinks customer

goal drinkers_paradox: 
   exists x:customer. drinks x -> 
     (forall y:customer. drinks y)
(** valid because the logic is classical, 
    and all types are assumed inhabited *)