Re: [mizar] Weak types

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Andrzej,

>>reserve x for SomePossibleEmptyType;

>  (for x holds P(x)) implies ex x st P(x)
>    proof
>      assume
>Z:      for x holds P(x);
>
>      take a;
>      thus P(a) by Z;
>     end;

Here is the exactly equivalent thing in Coq (which of course
_does_ allow its types to be empty):

  Parameter SomePossibleEmptyType : Type.
  Parameter P : SomePossibleEmptyType -> Prop.

  Goal (forall x, P x) -> (exists x, P x).
  Proof.
    intro Z.

    exists a.
    exact (Z a).
   Qed.

And again there is no way to get a term "a" to be used in the
"exists".  But I don't see why Mizar should have a problem
with this when Coq doesn't have any problems at all with this
kind of situation in general.

>But it is much more: we cannot allow for a ground term, even
>in a relaxed meaning - with local constants in it - with the
>type 'SomePossibleEmptyType'. Am I wrong?

Given what you have been given for SomePossibleEmptyType: of
course not.  But in general you probably will have something
to work with.  Consider the following pseudo-Mizar ("pseudo"
because of the "weak mode" in the fourth line):

  reserve n for Nat;

  definition let n;
   weak mode NonTrivialDivisor of n -> Nat means
  :Def1: it divides n & it <> 1 & it <> n;
  end;

  reserve m for non zero Nat;
  reserve d for NonTrivialDivisor of m;

  definition let m,d;
   redefine func m/d -> NonTrivialDivisor of m;
  ::  m has to be non-zero as 2 is NonTrivialDivisor of 0,
  ::  but 0/2 is not NonTrivialDivisor of 0
   coherence
   proof
  A1: d divides m & d <> 1 & d <> m by Def1;
    then consider d' being Nat such that
  A2: d*d' = m by NAT_1:def 3;
    d <> 0 by A2;
    then
  A3: d' = m/d by A2,XCMPLX_1:90;
    d' divides m & d' <> 1 & d' <> m by A1,A2,NAT_1:def 3,XCMPLX_1:7;
    hence thesis by A3,Def1;
   end;
  end;

  2*2 = 4;
  then 2 divides 4 by NAT_1:def 3;
  then reconsider two = 2 as NonTrivialDivisor of 4 by Def1;
  4/two is NonTrivialDivisor of 4;

  now
   let m,d;
   thus m/d is NonTrivialDivisor of m;
  end;

So the "NonTrivialDivisor" type will not always be non-empty
(there are no NonTrivialDivisors of a prime number), but I can
easily make terms ("two", "4/two", "m/d") that have it for a
type.

Or did I misunderstand the question?

Freek