[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: proofs involving epsilon

Murali Rangarajan posed the question" how to prove "choice" in the following:

choice: THEORY
  t: TYPE
  sets: TYPE = setof[t]
  sets_of_sets: TYPE = setof[sets]
  u, z: VAR t
  w, y: VAR sets
  x: VAR sets_of_sets

% forall nonempty sets x whose members are nonempty sets, there exists
% a set y such that every member of y is a member of some member of x,
% and every member of x has a member in y 

  choice: THEOREM
    (FORALL x:
       (nonempty?(x) AND (FORALL y: member(y, x) => nonempty?(y)))
         => ((EXISTS y:
               (FORALL z:
                  member(z, y)
                    IMPLIES (EXISTS w: member(w, x) AND member(z, w)))
               (FORALL w:
                  member(w, x)
                    IMPLIES (EXISTS z: member(z, w) AND member(z,
  END choice


The following proof does it.  Generally, it's preferable to use
"choose" rather than epsilon, because then the essential property is
encoded in the type.

There's some discussion of this in the paper

It's important to exclude "choose" from any grinds ('cos you do not
want the definition opened up).  The initial instantiation needs some
thought; the rest of the proof is then pretty routine: grind and its
friends will get the wrong instantiations, so you have to step
somewhat slowly and make the instantiations by hand until you get to
the point on each branch where you can let rip with reduce (the guts
of grind).

 (INST + "{a:t| exists (b: sets): member(b,x!1) and a=choose(b)}")
   (GRIND :IF-MATCH NIL :EXCLUDE ("choose"))
     (INST + "choose(w!1)")
     (("1" (ASSERT) (INST + "w!1") (ASSERT)) ("2" (REDUCE))))
    ("2" (INST + "b!1") (ASSERT))))
  ("2" (REDUCE))))