Re: [Hol-info] 0 / 0 = 0 ???

[Norrish, Michael (Data61, Acton)]

My comment is about how this is done in HOL, where the existing axiomatization 
is sufficient to give the behaviour as I have explained it.

Michael

From: Saburou Saitoh 
Date: Saturday, 10 August 2019 at 10:28
To: "Norrish, Michael (Data61, Acton)" 
Cc: "Chun Tian (binghe)" , hol-info 

Subject: Re: [Hol-info] 0 / 0 = 0 ???


Dear  Michael

For  x/0, the essential problem is on its definition.
I think the division by zero is trivial and clear all.
However, we will need a new axiom.
So, I would like to ask for your kind help for the axiom problem; Foundation of 
Mathematics.

Please look the draft:


viXra:1908.0100<http://vixra.org/abs/1908.0100> submitted on 2019-08-06 
20:03:01,

Fundamental of Mathematics; Division by Zero Calculus and a New Axiom


With best regards,
Sincerely yours,

Saburou Saitoh
2019.8.10.9:25



2019年8月10日(土) 9:07 Norrish, Michael (Data61, Acton) 
mailto:michael.norr...@data61.csiro.au>>:
It’s still defined inasmuch as it is perfectly legitimate to write x/0 and use 
that term to define other things in turn.   For example, I can define foo = x/0 
+ 1 and then quite successfully prove that x/0 < foo.

I would avoid the use of the word undefined in this context; rather x/0 has an 
unspecified value.  All functions are total so all applications of functions to 
all possible arguments have values.

Michael

> On 9 Aug 2019, at 21:46, Chun Tian (binghe) 
> mailto:binghe.l...@gmail.com>> wrote:
>
> A follow-up of this old topic:
>
> Finally I found the following definitions of `extreal_inv` and `extreal_div` 
> based on new_specification():
>
> local
>  val lemma = Q.prove (
> `?i. (i NegInf = Normal 0) /\
>  (i PosInf = Normal 0) /\
>  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
>   (* proof *)
>  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
>else if x = Normal 0 then ARB
>else Normal (inv (real x))` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- extreal_inv NegInf = Normal 0 /\
>extreal_inv PosInf = Normal 0 /\
>!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
>   *)
>  val extreal_inv_def = new_specification
>("extreal_inv_def", ["extreal_inv"], lemma);
> end;
>
> local
>  val lemma = Q.prove (
> `?d. (!r. d (Normal r) PosInf = Normal 0) /\
>  (!r. d (Normal r) NegInf = Normal 0) /\
>  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv 
> (Normal r`,
>   (* proof *)
>  Q.EXISTS_TAC `\x y.
>if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
>else if y = Normal 0 then ARB
>else extreal_mul x (extreal_inv y)` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
>(!r. extreal_div (Normal r) NegInf = Normal 0) /\
>!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
>   *)
>  val extreal_div_def = new_specification
>("extreal_div_def", ["extreal_div"], lemma);
> end;
>
> In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* 
> undefined.
>
> --Chun
>
> Il 20/02/19 06:48, 
> michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au> ha 
> scritto:
>> Your right hand side is no better than ARB really.  You say that your aim is 
>> to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a 
>> literal extreal, then I will define
>>
>>  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>>
>> and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
>> surely pni is too.
>>
>> (Recall that ARB's definition is `ARB = @x. T`.)
>>
>> Michael
>>
>>
>> On 20/2/19, 09:31, "Chun Tian (binghe)" 
>> mailto:binghe.l...@gmail.com>> wrote:
>>
>>Some further updates:
>>
>>With my last definition of `extreal_div`, I still have:
>>
>> |- !x. x / 0 = ARB
>>
>>and
>>
>> |- 0 / 0 = ARB
>>
>>trivially holds (by definition). This is still not satisfied to me.
>>
>>Now I tried the following new definition which looks more reasonable:
>>
>>val extreal_div_def = Define
>>   `extreal_div x y = if y = Normal 0 then
>>  (@x. (x = PosInf) \/ (x = NegInf))
>>  else extreal_mul x (extreal_inv y)`;
>>
>>literally, it says anything (well, let's ignore zero) divides zero is
>>equal to either +Inf or -In

Re: [Hol-info] 0 / 0 = 0 ???

[Saburou Saitoh]

Dear  Michael

For  x/0, the essential problem is on its definition.
I think the division by zero is trivial and clear all.
However, we will need a new axiom.
So, I would like to ask for your kind help for the axiom problem;
Foundation of Mathematics.

Please look the draft:

*viXra:1908.0100 * *submitted on 2019-08-06
20:03:01*,
Fundamental of Mathematics; Division by Zero Calculus and a New Axiom


With best regards,
Sincerely yours,

Saburou Saitoh
2019.8.10.9:25



2019年8月10日(土) 9:07 Norrish, Michael (Data61, Acton) <
michael.norr...@data61.csiro.au>:

> It’s still defined inasmuch as it is perfectly legitimate to write x/0 and
> use that term to define other things in turn.   For example, I can define
> foo = x/0 + 1 and then quite successfully prove that x/0 < foo.
>
> I would avoid the use of the word undefined in this context; rather x/0
> has an unspecified value.  All functions are total so all applications of
> functions to all possible arguments have values.
>
> Michael
>
> > On 9 Aug 2019, at 21:46, Chun Tian (binghe) 
> wrote:
> >
> > A follow-up of this old topic:
> >
> > Finally I found the following definitions of `extreal_inv` and
> `extreal_div` based on new_specification():
> >
> > local
> >  val lemma = Q.prove (
> > `?i. (i NegInf = Normal 0) /\
> >  (i PosInf = Normal 0) /\
> >  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
> >   (* proof *)
> >  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
> >else if x = Normal 0 then ARB
> >else Normal (inv (real x))` \\
> >  RW_TAC std_ss [extreal_not_infty, real_normal]);
> > in
> >  (* |- extreal_inv NegInf = Normal 0 /\
> >extreal_inv PosInf = Normal 0 /\
> >!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
> >   *)
> >  val extreal_inv_def = new_specification
> >("extreal_inv_def", ["extreal_inv"], lemma);
> > end;
> >
> > local
> >  val lemma = Q.prove (
> > `?d. (!r. d (Normal r) PosInf = Normal 0) /\
> >  (!r. d (Normal r) NegInf = Normal 0) /\
> >  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv
> (Normal r`,
> >   (* proof *)
> >  Q.EXISTS_TAC `\x y.
> >if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then
> Normal 0
> >else if y = Normal 0 then ARB
> >else extreal_mul x (extreal_inv y)` \\
> >  RW_TAC std_ss [extreal_not_infty, real_normal]);
> > in
> >  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
> >(!r. extreal_div (Normal r) NegInf = Normal 0) /\
> >!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv
> (Normal r)
> >   *)
> >  val extreal_div_def = new_specification
> >("extreal_div_def", ["extreal_div"], lemma);
> > end;
> >
> > In this way, things like `extreal_inv 0` and `extreal_div x 0` are
> *really* undefined.
> >
> > --Chun
> >
> > Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
> >> Your right hand side is no better than ARB really.  You say that your
> aim is to avoid x/0 = y, with y a literal extreal.  But if you believe ARB
> is a literal extreal, then I will define
> >>
> >>  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
> >>
> >> and then I can certainly prove that x/0 = pni.  If ARB is a literal
> extreal, surely pni is too.
> >>
> >> (Recall that ARB's definition is `ARB = @x. T`.)
> >>
> >> Michael
> >>
> >>
> >> On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
> >>
> >>Some further updates:
> >>
> >>With my last definition of `extreal_div`, I still have:
> >>
> >> |- !x. x / 0 = ARB
> >>
> >>and
> >>
> >> |- 0 / 0 = ARB
> >>
> >>trivially holds (by definition). This is still not satisfied to me.
> >>
> >>Now I tried the following new definition which looks more reasonable:
> >>
> >>val extreal_div_def = Define
> >>   `extreal_div x y = if y = Normal 0 then
> >>  (@x. (x = PosInf) \/ (x = NegInf))
> >>  else extreal_mul x (extreal_inv y)`;
> >>
> >>literally, it says anything (well, let's ignore zero) divides zero is
> >>equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf
> is
> >>irrelevant, as the sole purpose is to prevent any theorem like ``|-
> x /
> >>0 = y`` being proved, in which y is a literal extreal. For example,
> if I
> >>try to prove ``!x. x / 0 = ARB``:
> >>
> >>(* with the new definition, ``x / 0 = ARB`` (or any other extreal)
> can't
> >>be proved, e.g.
> >>val test_div = prove (
> >>   `!x. extreal_div x (Normal 0) = ARB`,
> >>RW_TAC std_ss [extreal_div_def]
>  Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
> >>> - RW_TAC std_ss []
>  MATCH_MP_TAC SELECT_ELIM_THM
>  RW_TAC std_ss [] (* 3 gubgoals *)
> >>   NegInf = ARB
> >>
> >>   PosInf = ARB
> >>
> >>   ∃x. (x = PosInf) ∨ (x = NegInf));
> >> *)
> >>
> >>at the end I got 3 subgoals 

Re: [Hol-info] 0 / 0 = 0 ???

[Norrish, Michael (Data61, Acton)]

It’s still defined inasmuch as it is perfectly legitimate to write x/0 and use 
that term to define other things in turn.   For example, I can define foo = x/0 
+ 1 and then quite successfully prove that x/0 < foo.

I would avoid the use of the word undefined in this context; rather x/0 has an 
unspecified value.  All functions are total so all applications of functions to 
all possible arguments have values.   

Michael

> On 9 Aug 2019, at 21:46, Chun Tian (binghe)  wrote:
> 
> A follow-up of this old topic:
> 
> Finally I found the following definitions of `extreal_inv` and `extreal_div` 
> based on new_specification():
> 
> local
>  val lemma = Q.prove (
> `?i. (i NegInf = Normal 0) /\
>  (i PosInf = Normal 0) /\
>  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
>   (* proof *)
>  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
>else if x = Normal 0 then ARB
>else Normal (inv (real x))` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- extreal_inv NegInf = Normal 0 /\
>extreal_inv PosInf = Normal 0 /\
>!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
>   *)
>  val extreal_inv_def = new_specification
>("extreal_inv_def", ["extreal_inv"], lemma);
> end;
> 
> local
>  val lemma = Q.prove (
> `?d. (!r. d (Normal r) PosInf = Normal 0) /\
>  (!r. d (Normal r) NegInf = Normal 0) /\
>  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv 
> (Normal r`,
>   (* proof *)
>  Q.EXISTS_TAC `\x y.
>if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
>else if y = Normal 0 then ARB
>else extreal_mul x (extreal_inv y)` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
>(!r. extreal_div (Normal r) NegInf = Normal 0) /\
>!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
>   *)
>  val extreal_div_def = new_specification
>("extreal_div_def", ["extreal_div"], lemma);
> end;
> 
> In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* 
> undefined.
> 
> --Chun
> 
> Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
>> Your right hand side is no better than ARB really.  You say that your aim is 
>> to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a 
>> literal extreal, then I will define
>> 
>>  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>> 
>> and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
>> surely pni is too.
>> 
>> (Recall that ARB's definition is `ARB = @x. T`.)
>> 
>> Michael
>> 
>> 
>> On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
>> 
>>Some further updates:
>> 
>>With my last definition of `extreal_div`, I still have:
>> 
>> |- !x. x / 0 = ARB
>> 
>>and
>> 
>> |- 0 / 0 = ARB
>> 
>>trivially holds (by definition). This is still not satisfied to me.
>> 
>>Now I tried the following new definition which looks more reasonable:
>> 
>>val extreal_div_def = Define
>>   `extreal_div x y = if y = Normal 0 then
>>  (@x. (x = PosInf) \/ (x = NegInf))
>>  else extreal_mul x (extreal_inv y)`;
>> 
>>literally, it says anything (well, let's ignore zero) divides zero is
>>equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
>>irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
>>0 = y`` being proved, in which y is a literal extreal. For example, if I
>>try to prove ``!x. x / 0 = ARB``:
>> 
>>(* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
>>be proved, e.g.
>>val test_div = prove (
>>   `!x. extreal_div x (Normal 0) = ARB`,
>>RW_TAC std_ss [extreal_div_def]
 Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>>> - RW_TAC std_ss []
 MATCH_MP_TAC SELECT_ELIM_THM
 RW_TAC std_ss [] (* 3 gubgoals *)
>>   NegInf = ARB
>> 
>>   PosInf = ARB
>> 
>>   ∃x. (x = PosInf) ∨ (x = NegInf));
>> *)
>> 
>>at the end I got 3 subgoals like above. I *believe*, no matter what
>>value I put instead of ARB, at least one of the subgoals must be false.
>>Thus the theorem should be unprovable. (am I right?)
>> 
>>Can I adopt this new definition of `extreal_div` in the future? Any
>>objection or suggestion?
>> 
>>--Chun
>> 
>>Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
>>> I'm going to use the following definition for `extreal_div`:
>>> 
>>> (* old definition of `extreal_div`, which allows `0 / 0 = 0`
>>> val extreal_div_def = Define
>>>   `extreal_div x y = extreal_mul x (extreal_inv y)`;
>>> 
>>>   new definition of `extreal_div`, excluding the case `0 / 0`: *)
>>> val extreal_div_def = Define
>>>   `extreal_div x y = if (y = Normal 0) then ARB
>>>  else extreal_mul x 

Re: [Hol-info] 0 / 0 = 0 ???

[Saburou Saitoh]

Dear Professor Chun Tian:


I am very interesting the problem.

Could you kindly give your kind comments and suggestions on the draft:

*viXra:1908.0100 * *submitted on 2019-08-06
20:03:01*,
Fundamental of Mathematics; Division by Zero Calculus and a New Axiom
?

It seems that the problem is very Fundamental for our Mathematics.

With best regards,
Sincerely yours,

Saburou Saitoh
2019.8.9.21:08



2019年8月9日(金) 20:47 Chun Tian (binghe) :

> A follow-up of this old topic:
>
> Finally I found the following definitions of `extreal_inv` and
> `extreal_div` based on new_specification():
>
> local
>   val lemma = Q.prove (
>  `?i. (i NegInf = Normal 0) /\
>   (i PosInf = Normal 0) /\
>   (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
>(* proof *)
>   Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
> else if x = Normal 0 then ARB
> else Normal (inv (real x))` \\
>   RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>   (* |- extreal_inv NegInf = Normal 0 /\
> extreal_inv PosInf = Normal 0 /\
> !r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
>*)
>   val extreal_inv_def = new_specification
> ("extreal_inv_def", ["extreal_inv"], lemma);
> end;
>
> local
>   val lemma = Q.prove (
>  `?d. (!r. d (Normal r) PosInf = Normal 0) /\
>   (!r. d (Normal r) NegInf = Normal 0) /\
>   (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv
> (Normal r`,
>(* proof *)
>   Q.EXISTS_TAC `\x y.
> if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then
> Normal 0
> else if y = Normal 0 then ARB
> else extreal_mul x (extreal_inv y)` \\
>   RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>   (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
> (!r. extreal_div (Normal r) NegInf = Normal 0) /\
> !x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv
> (Normal r)
>*)
>   val extreal_div_def = new_specification
> ("extreal_div_def", ["extreal_div"], lemma);
> end;
>
> In this way, things like `extreal_inv 0` and `extreal_div x 0` are
> *really* undefined.
>
> --Chun
>
> Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
> > Your right hand side is no better than ARB really.  You say that your
> aim is to avoid x/0 = y, with y a literal extreal.  But if you believe ARB
> is a literal extreal, then I will define
> >
> >   val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
> >
> > and then I can certainly prove that x/0 = pni.  If ARB is a literal
> extreal, surely pni is too.
> >
> > (Recall that ARB's definition is `ARB = @x. T`.)
> >
> > Michael
> >
> >
> > On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
> >
> > Some further updates:
> >
> > With my last definition of `extreal_div`, I still have:
> >
> >  |- !x. x / 0 = ARB
> >
> > and
> >
> >  |- 0 / 0 = ARB
> >
> > trivially holds (by definition). This is still not satisfied to me.
> >
> > Now I tried the following new definition which looks more reasonable:
> >
> > val extreal_div_def = Define
> >`extreal_div x y = if y = Normal 0 then
> > (@x. (x = PosInf) \/ (x = NegInf))
> > else extreal_mul x (extreal_inv y)`;
> >
> > literally, it says anything (well, let's ignore zero) divides zero is
> > equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf
> is
> > irrelevant, as the sole purpose is to prevent any theorem like ``|-
> x /
> > 0 = y`` being proved, in which y is a literal extreal. For example,
> if I
> > try to prove ``!x. x / 0 = ARB``:
> >
> > (* with the new definition, ``x / 0 = ARB`` (or any other extreal)
> can't
> > be proved, e.g.
> > val test_div = prove (
> >`!x. extreal_div x (Normal 0) = ARB`,
> > RW_TAC std_ss [extreal_div_def]
> >  >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
> >  >- RW_TAC std_ss []
> >  >> MATCH_MP_TAC SELECT_ELIM_THM
> >  >> RW_TAC std_ss [] (* 3 gubgoals *)
> >NegInf = ARB
> >
> >PosInf = ARB
> >
> >∃x. (x = PosInf) ∨ (x = NegInf));
> >  *)
> >
> > at the end I got 3 subgoals like above. I *believe*, no matter what
> > value I put instead of ARB, at least one of the subgoals must be
> false.
> > Thus the theorem should be unprovable. (am I right?)
> >
> > Can I adopt this new definition of `extreal_div` in the future? Any
> > objection or suggestion?
> >
> > --Chun
> >
> > Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> > > I'm going to use the following definition for `extreal_div`:
> > >
> > > (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> > > val extreal_div_def = Define
> > >`extreal_div x y = extreal_mul x (extreal_inv y)`;
> > >
> > >new definition of 

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

A follow-up of this old topic:

Finally I found the following definitions of `extreal_inv` and `extreal_div` 
based on new_specification():

local
  val lemma = Q.prove (
 `?i. (i NegInf = Normal 0) /\
  (i PosInf = Normal 0) /\
  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
   (* proof *)
  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
else if x = Normal 0 then ARB
else Normal (inv (real x))` \\
  RW_TAC std_ss [extreal_not_infty, real_normal]);
in
  (* |- extreal_inv NegInf = Normal 0 /\
extreal_inv PosInf = Normal 0 /\
!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
   *)
  val extreal_inv_def = new_specification
("extreal_inv_def", ["extreal_inv"], lemma);
end;

local
  val lemma = Q.prove (
 `?d. (!r. d (Normal r) PosInf = Normal 0) /\
  (!r. d (Normal r) NegInf = Normal 0) /\
  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv 
(Normal r`,
   (* proof *)
  Q.EXISTS_TAC `\x y.
if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
else if y = Normal 0 then ARB
else extreal_mul x (extreal_inv y)` \\
  RW_TAC std_ss [extreal_not_infty, real_normal]);
in
  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
(!r. extreal_div (Normal r) NegInf = Normal 0) /\
!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
   *)
  val extreal_div_def = new_specification
("extreal_div_def", ["extreal_div"], lemma);
end;

In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* 
undefined.

--Chun

Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
> Your right hand side is no better than ARB really.  You say that your aim is 
> to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a 
> literal extreal, then I will define
> 
>   val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
> 
> and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
> surely pni is too.
> 
> (Recall that ARB's definition is `ARB = @x. T`.)
> 
> Michael
> 
> 
> On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
> 
> Some further updates:
> 
> With my last definition of `extreal_div`, I still have:
> 
>  |- !x. x / 0 = ARB
> 
> and
> 
>  |- 0 / 0 = ARB
> 
> trivially holds (by definition). This is still not satisfied to me.
> 
> Now I tried the following new definition which looks more reasonable:
> 
> val extreal_div_def = Define
>`extreal_div x y = if y = Normal 0 then
> (@x. (x = PosInf) \/ (x = NegInf))
> else extreal_mul x (extreal_inv y)`;
> 
> literally, it says anything (well, let's ignore zero) divides zero is
> equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
> irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
> 0 = y`` being proved, in which y is a literal extreal. For example, if I
> try to prove ``!x. x / 0 = ARB``:
> 
> (* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
> be proved, e.g.
> val test_div = prove (
>`!x. extreal_div x (Normal 0) = ARB`,
> RW_TAC std_ss [extreal_div_def]
>  >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>  >- RW_TAC std_ss []
>  >> MATCH_MP_TAC SELECT_ELIM_THM
>  >> RW_TAC std_ss [] (* 3 gubgoals *)
>NegInf = ARB
> 
>PosInf = ARB
> 
>∃x. (x = PosInf) ∨ (x = NegInf));
>  *)
> 
> at the end I got 3 subgoals like above. I *believe*, no matter what
> value I put instead of ARB, at least one of the subgoals must be false.
> Thus the theorem should be unprovable. (am I right?)
> 
> Can I adopt this new definition of `extreal_div` in the future? Any
> objection or suggestion?
> 
> --Chun
> 
> Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> > I'm going to use the following definition for `extreal_div`:
> > 
> > (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> > val extreal_div_def = Define
> >`extreal_div x y = extreal_mul x (extreal_inv y)`;
> > 
> >new definition of `extreal_div`, excluding the case `0 / 0`: *)
> > val extreal_div_def = Define
> >`extreal_div x y = if (y = Normal 0) then ARB
> >   else extreal_mul x (extreal_inv y)`;
> > 
> > previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
> >  antecedent, which makes perfectly senses.
> > 
> > P.S. the division of extended reals in HOL4 are not used until the
> > statement and proof of Radon-Nikodým theorem, then the conditional
> > probability.
> > 
> > --Chun
> > 
> > Il 15/02/19 17:39, Mark Adams ha scritto:
> >> I think there is 

Re: [Hol-info] 0 / 0 = 0 ???

[Freek Wiedijk]

Dear all,

For what it's worth, a definition of division with 0/0 = 0
won't be possible constructively, because in constructive
mathematics all functions of type real->real are continuous,
and with this definition division is _not_ continuous.

Also, in IEEE 754 floating point of course division is a
total operation.  One can easily imagine an "extreal" type
that is in this spirit (with "infinity" and "-infinity"
and "nan" added to the mathematical reals), where division
is total.

Finally, my PhD advisor Jan Bergstra has a theory of
something called "meadows" (related to "fields", I guess),
in which division is total.  Google "bergstra meadows"
for some references :-)  So that gives some legimity
to formalizing a total division function ("this is just
about meadows").  I never really looked at this work though,
and don't know whether in "meadows" one always has 1/0 = 0.
(I guess one certainly will have 0/0 = 0.)

I'm sure all these observations won't satisfy traditional
mathematicians about the treatment of divisions in systems
that only allow for total functions.  Hell, it doesn't
statisfy _me_ :-)

Freek


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Lawrence Paulson]

I sympathise with you here, as some mathematicians freak out at any mention of 
division by zero. It’s not always easy for them to grasp what we are doing with 
formal logic. You also need to bear in mind that mathematics texts are not 
proved in any formal system, and in most cases, foundational matters are kept 
well in the background. Unless the material is specifically axiomatic set 
theory, it’s a mistake to imagine that mathematics is being done in ZFC.

One can at least mention that the usual paradoxes connected with division by 
zero do not occur, since we do not have (x*y)/x = y unconditionally.

Larry Paulson


> On 20 Feb 2019, at 20:40, hol-info-requ...@lists.sourceforge.net wrote:
> 
> Keeping ``0 / 0 = 0`` as before, could be another option, but I have concerns 
> to convince mathematicians to accept this fact since I aim at precisely 
> reproduce those pure math proofs under the ?same? formal system with math 
> books



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Ramana Kumar]

Very nice paper. Thanks Umair and Freek for the correction and link.

On Wed, 20 Feb 2019 21:08 Umair Siddique 
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101=rep1=pdf
>
> http://www.gilith.com/talks/tphols2001-subtypes.pdf
>
>
> - Umair
>
> On Wed, Feb 20, 2019 at 4:02 PM Freek Wiedijk  wrote:
>
>> Hi Ramana,
>>
>> >I think this is exactly what is impossible to do in HOL:
>> >it is a logic of total functions.
>>
>> I think that in PVS you _can_ do something like that, right?
>> Using the predicate subtypes.  Even though PVS _also_
>> only has total functions.
>>
>> And I _think_ there was a paper once about how to mimic
>> predicate subtypes in HOL.  Does anyone remember the
>> reference?
>>
>> Freek
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Ramana Kumar]

> So I think the key is to make sure that “undefined” thing really
undefined, such that whenever it appears, the proof cannot proceed any more

I think this is exactly what is impossible to do in HOL: it is a logic of
total functions.

On Wed, 20 Feb 2019 at 15:26, Chun Tian (binghe) 
wrote:

> Well, as the purpose of optionTheory is to augment any type with one more
> value, for (at least) extreals, it would be equivalent to have that
> “undefined” thing defined as part of the datatype definition:
>
> val extreal_def = Datatype
>`extreal = NegInf | PosInf | Normal real | Undefined`;
>
> However, once “Undefined” is actually defined, it’s then a disaster to
> affect almost all arithmetic laws. For a number which is either PosInf nor
> NegInf, now we can’t say it must be a (Normal x) any more, and many
> theorems will be broken.  To fix it, we have to treat this “Undefined” as
> something like those NaNs in IEEE 754 standard and define their orders and
> arithmetic laws, then all these work are unnecessary for formalization of
> pure math theorems.
>
> So I think the key is to make sure that “undefined” thing really
> undefined, such that whenever it appears, the proof cannot proceed any
> more, except for syntactic rewriting, which is inevitable in HOL.   Keeping
> ``0 / 0 = 0`` as before, could be another option, but I have concerns to
> convince mathematicians to accept this fact since I aim at precisely
> reproduce those pure math proofs under the “same” formal system with math
> books (except for the subtle differences between ZFC and HOL not affecting
> the math theories that I’m working with.)
>
> —Chun
>
> Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> I'd say one of the stronger ways to get "undefined" is to add an element
> to your type representing undefinedness, e.g., make it (/) : real option ->
> real option -> real option, where NONE represents "undefined". But then you
> will have a lot of bookkeeping to deal with...
> I don't suggest this seriously in the case of division -- I would rather
> suggest accepting the usual treatment of these partial functions as a small
> price for the benefits of working in a logic of (only) total functions.
>
> On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson  wrote:
>
>> None of these attempts make any sense. In HOL and similar systems
>> (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be
>> undefined in any strong sense. Fortunately, it’s consistent and harmless to
>> put x/0 = 0.
>>
>> Larry Paulson
>>
>>
>> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote:
>> >
>> > I run some experiments so to check if it is violating any fundamental
>> rule.
>> > So far it went good.
>>
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

Well, as the purpose of optionTheory is to augment any type with one more 
value, for (at least) extreals, it would be equivalent to have that “undefined” 
thing defined as part of the datatype definition:

val extreal_def = Datatype
   `extreal = NegInf | PosInf | Normal real | Undefined`;

However, once “Undefined” is actually defined, it’s then a disaster to affect 
almost all arithmetic laws. For a number which is either PosInf nor NegInf, now 
we can’t say it must be a (Normal x) any more, and many theorems will be 
broken.  To fix it, we have to treat this “Undefined” as something like those 
NaNs in IEEE 754 standard and define their orders and arithmetic laws, then all 
these work are unnecessary for formalization of pure math theorems.

So I think the key is to make sure that “undefined” thing really undefined, 
such that whenever it appears, the proof cannot proceed any more, except for 
syntactic rewriting, which is inevitable in HOL.   Keeping ``0 / 0 = 0`` as 
before, could be another option, but I have concerns to convince mathematicians 
to accept this fact since I aim at precisely reproduce those pure math proofs 
under the “same” formal system with math books (except for the subtle 
differences between ZFC and HOL not affecting the math theories that I’m 
working with.)

—Chun

> Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar 
>  ha scritto:
> 
> I'd say one of the stronger ways to get "undefined" is to add an element to 
> your type representing undefinedness, e.g., make it (/) : real option -> real 
> option -> real option, where NONE represents "undefined". But then you will 
> have a lot of bookkeeping to deal with...
> I don't suggest this seriously in the case of division -- I would rather 
> suggest accepting the usual treatment of these partial functions as a small 
> price for the benefits of working in a logic of (only) total functions.
> 
> On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson  > wrote:
> None of these attempts make any sense. In HOL and similar systems (including 
> Isabelle/HOL), it’s *impossible* to arrange for x/0 to be undefined in any 
> strong sense. Fortunately, it’s consistent and harmless to put x/0 = 0.
> 
> Larry Paulson
> 
> 
> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net 
> >  wrote:
> >
> > I run some experiments so to check if it is violating any fundamental rule.
> > So far it went good.
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Ramana Kumar]

I'd say one of the stronger ways to get "undefined" is to add an element to
your type representing undefinedness, e.g., make it (/) : real option ->
real option -> real option, where NONE represents "undefined". But then you
will have a lot of bookkeeping to deal with...
I don't suggest this seriously in the case of division -- I would rather
suggest accepting the usual treatment of these partial functions as a small
price for the benefits of working in a logic of (only) total functions.

On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson  wrote:

> None of these attempts make any sense. In HOL and similar systems
> (including Isabelle/HOL), it’s *impossible* to arrange for x/0 to be
> undefined in any strong sense. Fortunately, it’s consistent and harmless to
> put x/0 = 0.
>
> Larry Paulson
>
>
> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net wrote:
> >
> > I run some experiments so to check if it is violating any fundamental
> rule.
> > So far it went good.
>
>
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Michael.Norrish]

Ha - I stand corrected.  Thanks for that.

From: Konrad Slind 
Date: Wednesday, 20 February 2019 at 17:22
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] 0 / 0 = 0 ???

Just a minor note: ARB is declared as an uninterpreted constant of type 'a. It 
used to be defined to be @x.T.

Konrad.


On Tue, Feb 19, 2019 at 11:49 PM 
mailto:michael.norr...@data61.csiro.au>> wrote:
Your right hand side is no better than ARB really.  You say that your aim is to 
avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a literal 
extreal, then I will define

  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;

and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
surely pni is too.

(Recall that ARB's definition is `ARB = @x. T`.)

Michael


On 20/2/19, 09:31, "Chun Tian (binghe)" 
mailto:binghe.l...@gmail.com>> wrote:

Some further updates:

With my last definition of `extreal_div`, I still have:

 |- !x. x / 0 = ARB

and

 |- 0 / 0 = ARB

trivially holds (by definition). This is still not satisfied to me.

Now I tried the following new definition which looks more reasonable:

val extreal_div_def = Define
   `extreal_div x y = if y = Normal 0 then
  (@x. (x = PosInf) \/ (x = NegInf))
  else extreal_mul x (extreal_inv y)`;

literally, it says anything (well, let's ignore zero) divides zero is
equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
0 = y`` being proved, in which y is a literal extreal. For example, if I
try to prove ``!x. x / 0 = ARB``:

(* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
be proved, e.g.
val test_div = prove (
   `!x. extreal_div x (Normal 0) = ARB`,
RW_TAC std_ss [extreal_div_def]
 >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
 >- RW_TAC std_ss []
 >> MATCH_MP_TAC SELECT_ELIM_THM
 >> RW_TAC std_ss [] (* 3 gubgoals *)
   NegInf = ARB

   PosInf = ARB

   ∃x. (x = PosInf) ∨ (x = NegInf));
 *)

at the end I got 3 subgoals like above. I *believe*, no matter what
value I put instead of ARB, at least one of the subgoals must be false.
Thus the theorem should be unprovable. (am I right?)

Can I adopt this new definition of `extreal_div` in the future? Any
objection or suggestion?

--Chun

Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> I'm going to use the following definition for `extreal_div`:
>
> (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> val extreal_div_def = Define
>`extreal_div x y = extreal_mul x (extreal_inv y)`;
>
>new definition of `extreal_div`, excluding the case `0 / 0`: *)
> val extreal_div_def = Define
>`extreal_div x y = if (y = Normal 0) then ARB
>   else extreal_mul x (extreal_inv y)`;
>
> previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
>  antecedent, which makes perfectly senses.
>
> P.S. the division of extended reals in HOL4 are not used until the
> statement and proof of Radon-Nikodým theorem, then the conditional
> probability.
>
> --Chun
>
> Il 15/02/19 17:39, Mark Adams ha scritto:
>> I think there is definitely an advantage in keeping ``x/y`` undefined
>> (even granted that it will always be possible to prove ``?y. x/0 = y``),
>> namely that it means that your proofs are much more likely to directly
>> translate to other formalisms of real numbers where '/' is not total.
>>
>> Of course there is also a disadvantage, in that it makes proof harder.
>> But then, arguably, being forced to justify that we are staying within
>> the "normal" domain of the function is probably a good thing (in a
>> similar way as being forced to conform to a type system is a good
>> thing).  I understand that, historically, it is this disadvantage of
>> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
>> much easier for automated routines if they don't have to consider side
>> conditions.
>>
>> Mark.
>>
>> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
>>> Thanks to all kindly answers.
>>>
>>> Even I wanted ``0 / 0 = 0`` to be excluded from at least
>>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I
>>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
>>> going to happen, I do case analysis in

Re: [Hol-info] 0 / 0 = 0 ???

[Konrad Slind]

Just a minor note: ARB is declared as an uninterpreted constant of type 'a.
It used to be defined to be @x.T.

Konrad.


On Tue, Feb 19, 2019 at 11:49 PM  wrote:

> Your right hand side is no better than ARB really.  You say that your aim
> is to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a
> literal extreal, then I will define
>
>   val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>
> and then I can certainly prove that x/0 = pni.  If ARB is a literal
> extreal, surely pni is too.
>
> (Recall that ARB's definition is `ARB = @x. T`.)
>
> Michael
>
>
> On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
>
> Some further updates:
>
> With my last definition of `extreal_div`, I still have:
>
>  |- !x. x / 0 = ARB
>
> and
>
>  |- 0 / 0 = ARB
>
> trivially holds (by definition). This is still not satisfied to me.
>
> Now I tried the following new definition which looks more reasonable:
>
> val extreal_div_def = Define
>`extreal_div x y = if y = Normal 0 then
>   (@x. (x = PosInf) \/ (x = NegInf))
>   else extreal_mul x (extreal_inv y)`;
>
> literally, it says anything (well, let's ignore zero) divides zero is
> equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
> irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
> 0 = y`` being proved, in which y is a literal extreal. For example, if
> I
> try to prove ``!x. x / 0 = ARB``:
>
> (* with the new definition, ``x / 0 = ARB`` (or any other extreal)
> can't
> be proved, e.g.
> val test_div = prove (
>`!x. extreal_div x (Normal 0) = ARB`,
> RW_TAC std_ss [extreal_div_def]
>  >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>  >- RW_TAC std_ss []
>  >> MATCH_MP_TAC SELECT_ELIM_THM
>  >> RW_TAC std_ss [] (* 3 gubgoals *)
>NegInf = ARB
>
>PosInf = ARB
>
>∃x. (x = PosInf) ∨ (x = NegInf));
>  *)
>
> at the end I got 3 subgoals like above. I *believe*, no matter what
> value I put instead of ARB, at least one of the subgoals must be false.
> Thus the theorem should be unprovable. (am I right?)
>
> Can I adopt this new definition of `extreal_div` in the future? Any
> objection or suggestion?
>
> --Chun
>
> Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> > I'm going to use the following definition for `extreal_div`:
> >
> > (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> > val extreal_div_def = Define
> >`extreal_div x y = extreal_mul x (extreal_inv y)`;
> >
> >new definition of `extreal_div`, excluding the case `0 / 0`: *)
> > val extreal_div_def = Define
> >`extreal_div x y = if (y = Normal 0) then ARB
> >   else extreal_mul x (extreal_inv y)`;
> >
> > previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <>
> 0` as
> >  antecedent, which makes perfectly senses.
> >
> > P.S. the division of extended reals in HOL4 are not used until the
> > statement and proof of Radon-Nikodým theorem, then the conditional
> > probability.
> >
> > --Chun
> >
> > Il 15/02/19 17:39, Mark Adams ha scritto:
> >> I think there is definitely an advantage in keeping ``x/y``
> undefined
> >> (even granted that it will always be possible to prove ``?y. x/0 =
> y``),
> >> namely that it means that your proofs are much more likely to
> directly
> >> translate to other formalisms of real numbers where '/' is not
> total.
> >>
> >> Of course there is also a disadvantage, in that it makes proof
> harder.
> >> But then, arguably, being forced to justify that we are staying
> within
> >> the "normal" domain of the function is probably a good thing (in a
> >> similar way as being forced to conform to a type system is a good
> >> thing).  I understand that, historically, it is this disadvantage of
> >> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
> >> much easier for automated routines if they don't have to consider
> side
> >> conditions.
> >>
> >> Mark.
> >>
> >> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
> >>> Thanks to all kindly answers.
> >>>
> >>> Even I wanted ``0 / 0 = 0`` to be excluded from at least
> >>> "extreal_div_def" (in extrealTheory), I found no way to do that.
> All I
> >>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever
> it's
> >>> going to happen, I do case analysis instead.
> >>>
> >>> --Chun
> >>>
> >>> Il 14/02/19 18:12, Konrad Slind ha scritto:
>  It's a deliberate choice. See the discussion in Section 1.2 of
> 
> 
> http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf
> 
> 
> 
> 
>

Re: [Hol-info] 0 / 0 = 0 ???

[Michael.Norrish]

Your right hand side is no better than ARB really.  You say that your aim is to 
avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a literal 
extreal, then I will define

  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;

and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
surely pni is too.

(Recall that ARB's definition is `ARB = @x. T`.)

Michael


On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:

Some further updates:

With my last definition of `extreal_div`, I still have:

 |- !x. x / 0 = ARB

and

 |- 0 / 0 = ARB

trivially holds (by definition). This is still not satisfied to me.

Now I tried the following new definition which looks more reasonable:

val extreal_div_def = Define
   `extreal_div x y = if y = Normal 0 then
  (@x. (x = PosInf) \/ (x = NegInf))
  else extreal_mul x (extreal_inv y)`;

literally, it says anything (well, let's ignore zero) divides zero is
equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
0 = y`` being proved, in which y is a literal extreal. For example, if I
try to prove ``!x. x / 0 = ARB``:

(* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
be proved, e.g.
val test_div = prove (
   `!x. extreal_div x (Normal 0) = ARB`,
RW_TAC std_ss [extreal_div_def]
 >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
 >- RW_TAC std_ss []
 >> MATCH_MP_TAC SELECT_ELIM_THM
 >> RW_TAC std_ss [] (* 3 gubgoals *)
   NegInf = ARB

   PosInf = ARB

   ∃x. (x = PosInf) ∨ (x = NegInf));
 *)

at the end I got 3 subgoals like above. I *believe*, no matter what
value I put instead of ARB, at least one of the subgoals must be false.
Thus the theorem should be unprovable. (am I right?)

Can I adopt this new definition of `extreal_div` in the future? Any
objection or suggestion?

--Chun

Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> I'm going to use the following definition for `extreal_div`:
> 
> (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> val extreal_div_def = Define
>`extreal_div x y = extreal_mul x (extreal_inv y)`;
> 
>new definition of `extreal_div`, excluding the case `0 / 0`: *)
> val extreal_div_def = Define
>`extreal_div x y = if (y = Normal 0) then ARB
>   else extreal_mul x (extreal_inv y)`;
> 
> previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
>  antecedent, which makes perfectly senses.
> 
> P.S. the division of extended reals in HOL4 are not used until the
> statement and proof of Radon-Nikodým theorem, then the conditional
> probability.
> 
> --Chun
> 
> Il 15/02/19 17:39, Mark Adams ha scritto:
>> I think there is definitely an advantage in keeping ``x/y`` undefined
>> (even granted that it will always be possible to prove ``?y. x/0 = y``),
>> namely that it means that your proofs are much more likely to directly
>> translate to other formalisms of real numbers where '/' is not total.
>>
>> Of course there is also a disadvantage, in that it makes proof harder. 
>> But then, arguably, being forced to justify that we are staying within
>> the "normal" domain of the function is probably a good thing (in a
>> similar way as being forced to conform to a type system is a good
>> thing).  I understand that, historically, it is this disadvantage of
>> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
>> much easier for automated routines if they don't have to consider side
>> conditions.
>>
>> Mark.
>>
>> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
>>> Thanks to all kindly answers.
>>>
>>> Even I wanted ``0 / 0 = 0`` to be excluded from at least
>>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I
>>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
>>> going to happen, I do case analysis instead.
>>>
>>> --Chun
>>>
>>> Il 14/02/19 18:12, Konrad Slind ha scritto:
 It's a deliberate choice. See the discussion in Section 1.2 of

 
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf




 On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
 mailto:binghe.l...@gmail.com>> wrote:

 Hi,

 in HOL's realTheory, division is defined by multiplication:

 [real_div]  Definition

   ⊢ ∀x y. x / y = x * y⁻¹

 and zero 

Re: [Hol-info] 0 / 0 = 0 ???

[Waqar Ahmad via hol-info]

Hi Chun,

I run some experiments so to check if it is violating any fundamental rule.
So far it went good.



On Tue, Feb 19, 2019 at 5:31 PM Chun Tian (binghe) 
wrote:

> Some further updates:
>
> With my last definition of `extreal_div`, I still have:
>
>  |- !x. x / 0 = ARB
>
> and
>
>  |- 0 / 0 = ARB
>
> trivially holds (by definition). This is still not satisfied to me.
>
> Now I tried the following new definition which looks more reasonable:
>
> val extreal_div_def = Define
>`extreal_div x y = if y = Normal 0 then
>   (@x. (x = PosInf) \/ (x = NegInf))
>   else extreal_mul x (extreal_inv y)`;
>
> literally, it says anything (well, let's ignore zero) divides zero is
> equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
> irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
> 0 = y`` being proved, in which y is a literal extreal. For example, if I
> try to prove ``!x. x / 0 = ARB``:
>
> (* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
> be proved, e.g.
> val test_div = prove (
>`!x. extreal_div x (Normal 0) = ARB`,
> RW_TAC std_ss [extreal_div_def]
>  >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>  >- RW_TAC std_ss []
>  >> MATCH_MP_TAC SELECT_ELIM_THM
>  >> RW_TAC std_ss [] (* 3 gubgoals *)
>NegInf = ARB
>
>PosInf = ARB
>
>∃x. (x = PosInf) ∨ (x = NegInf));
>  *)
>
> at the end I got 3 subgoals like above. I *believe*, no matter what
> value I put instead of ARB, at least one of the subgoals must be false.
> Thus the theorem should be unprovable. (am I right?)
>
> Can I adopt this new definition of `extreal_div` in the future? Any
> objection or suggestion?
>
> --Chun
>
> Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> > I'm going to use the following definition for `extreal_div`:
> >
> > (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> > val extreal_div_def = Define
> >`extreal_div x y = extreal_mul x (extreal_inv y)`;
> >
> >new definition of `extreal_div`, excluding the case `0 / 0`: *)
> > val extreal_div_def = Define
> >`extreal_div x y = if (y = Normal 0) then ARB
> >   else extreal_mul x (extreal_inv y)`;
> >
> > previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
> >  antecedent, which makes perfectly senses.
> >
> > P.S. the division of extended reals in HOL4 are not used until the
> > statement and proof of Radon-Nikodým theorem, then the conditional
> > probability.
> >
> > --Chun
> >
> > Il 15/02/19 17:39, Mark Adams ha scritto:
> >> I think there is definitely an advantage in keeping ``x/y`` undefined
> >> (even granted that it will always be possible to prove ``?y. x/0 = y``),
> >> namely that it means that your proofs are much more likely to directly
> >> translate to other formalisms of real numbers where '/' is not total.
> >>
> >> Of course there is also a disadvantage, in that it makes proof harder.
> >> But then, arguably, being forced to justify that we are staying within
> >> the "normal" domain of the function is probably a good thing (in a
> >> similar way as being forced to conform to a type system is a good
> >> thing).  I understand that, historically, it is this disadvantage of
> >> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
> >> much easier for automated routines if they don't have to consider side
> >> conditions.
> >>
> >> Mark.
> >>
> >> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
> >>> Thanks to all kindly answers.
> >>>
> >>> Even I wanted ``0 / 0 = 0`` to be excluded from at least
> >>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I
> >>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
> >>> going to happen, I do case analysis instead.
> >>>
> >>> --Chun
> >>>
> >>> Il 14/02/19 18:12, Konrad Slind ha scritto:
>  It's a deliberate choice. See the discussion in Section 1.2 of
> 
> 
> http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf
> 
> 
> 
> 
>  On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
>  mailto:binghe.l...@gmail.com>> wrote:
> 
>  Hi,
> 
>  in HOL's realTheory, division is defined by multiplication:
> 
>  [real_div]  Definition
> 
>    ⊢ ∀x y. x / y = x * y⁻¹
> 
>  and zero multiplies any other real number equals to zero, which is
>  definitely true:
> 
> [REAL_MUL_LZERO]  Theorem
> 
>    ⊢ ∀x. 0 * x = 0
> 
>  However, above two theorems together gives ``0 / 0 = 0``, as shown
>  below:
> 
>  > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
>  val it = ⊢ 0 / 0 = 0: thm
> 
>  How do I understand this result? Is there anything "wrong"?
> 
>  (The same problems happens also in extrealTheory, 

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

Some further updates:

With my last definition of `extreal_div`, I still have:

 |- !x. x / 0 = ARB

and

 |- 0 / 0 = ARB

trivially holds (by definition). This is still not satisfied to me.

Now I tried the following new definition which looks more reasonable:

val extreal_div_def = Define
   `extreal_div x y = if y = Normal 0 then
  (@x. (x = PosInf) \/ (x = NegInf))
  else extreal_mul x (extreal_inv y)`;

literally, it says anything (well, let's ignore zero) divides zero is
equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
0 = y`` being proved, in which y is a literal extreal. For example, if I
try to prove ``!x. x / 0 = ARB``:

(* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
be proved, e.g.
val test_div = prove (
   `!x. extreal_div x (Normal 0) = ARB`,
RW_TAC std_ss [extreal_div_def]
 >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
 >- RW_TAC std_ss []
 >> MATCH_MP_TAC SELECT_ELIM_THM
 >> RW_TAC std_ss [] (* 3 gubgoals *)
   NegInf = ARB

   PosInf = ARB

   ∃x. (x = PosInf) ∨ (x = NegInf));
 *)

at the end I got 3 subgoals like above. I *believe*, no matter what
value I put instead of ARB, at least one of the subgoals must be false.
Thus the theorem should be unprovable. (am I right?)

Can I adopt this new definition of `extreal_div` in the future? Any
objection or suggestion?

--Chun

Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
> I'm going to use the following definition for `extreal_div`:
> 
> (* old definition of `extreal_div`, which allows `0 / 0 = 0`
> val extreal_div_def = Define
>`extreal_div x y = extreal_mul x (extreal_inv y)`;
> 
>new definition of `extreal_div`, excluding the case `0 / 0`: *)
> val extreal_div_def = Define
>`extreal_div x y = if (y = Normal 0) then ARB
>   else extreal_mul x (extreal_inv y)`;
> 
> previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
>  antecedent, which makes perfectly senses.
> 
> P.S. the division of extended reals in HOL4 are not used until the
> statement and proof of Radon-Nikodým theorem, then the conditional
> probability.
> 
> --Chun
> 
> Il 15/02/19 17:39, Mark Adams ha scritto:
>> I think there is definitely an advantage in keeping ``x/y`` undefined
>> (even granted that it will always be possible to prove ``?y. x/0 = y``),
>> namely that it means that your proofs are much more likely to directly
>> translate to other formalisms of real numbers where '/' is not total.
>>
>> Of course there is also a disadvantage, in that it makes proof harder. 
>> But then, arguably, being forced to justify that we are staying within
>> the "normal" domain of the function is probably a good thing (in a
>> similar way as being forced to conform to a type system is a good
>> thing).  I understand that, historically, it is this disadvantage of
>> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
>> much easier for automated routines if they don't have to consider side
>> conditions.
>>
>> Mark.
>>
>> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
>>> Thanks to all kindly answers.
>>>
>>> Even I wanted ``0 / 0 = 0`` to be excluded from at least
>>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I
>>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
>>> going to happen, I do case analysis instead.
>>>
>>> --Chun
>>>
>>> Il 14/02/19 18:12, Konrad Slind ha scritto:
 It's a deliberate choice. See the discussion in Section 1.2 of

 http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf




 On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
 mailto:binghe.l...@gmail.com>> wrote:

     Hi,

     in HOL's realTheory, division is defined by multiplication:

     [real_div]  Definition

           ⊢ ∀x y. x / y = x * y⁻¹

     and zero multiplies any other real number equals to zero, which is
     definitely true:

        [REAL_MUL_LZERO]  Theorem

           ⊢ ∀x. 0 * x = 0

     However, above two theorems together gives ``0 / 0 = 0``, as shown
     below:

     > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
     val it = ⊢ 0 / 0 = 0: thm

     How do I understand this result? Is there anything "wrong"?

     (The same problems happens also in extrealTheory, since the
 definition
     of `*` finally reduces to `*` of real numbers)

     Regards,

     Chun Tian

     ___
     hol-info mailing list
     hol-info@lists.sourceforge.net
 
     https://lists.sourceforge.net/lists/listinfo/hol-info

>>>
>>>
>>> 

Re: [Hol-info] 0 / 0 = 0 ???

[Michael.Norrish]

Note that many/most interesting properties of division still pick up 
side-conditions involving the non-zero-ness of y. (The attachment is all HOL4's 
"simple" theorems about division from realTheory, which establishes the basic 
properties of the reals and their operations.)

Michael

On 16/2/19, 04:38, "Mark Adams"  wrote:

I think there is definitely an advantage in keeping ``x/y`` undefined 
(even granted that it will always be possible to prove ``?y. x/0 = y``), 
namely that it means that your proofs are much more likely to directly 
translate to other formalisms of real numbers where '/' is not total.

Of course there is also a disadvantage, in that it makes proof harder.  
But then, arguably, being forced to justify that we are staying within 
the "normal" domain of the function is probably a good thing (in a 
similar way as being forced to conform to a type system is a good 
thing).  I understand that, historically, it is this disadvantage of 
harder proofs that was the reason for making ``0/0=0`` in HOL.  It's 
much easier for automated routines if they don't have to consider side 
conditions.

Mark.

On 15/02/2019 08:56, Chun Tian (binghe) wrote:
> Thanks to all kindly answers.
> 
> Even I wanted ``0 / 0 = 0`` to be excluded from at least
> "extreal_div_def" (in extrealTheory), I found no way to do that. All I
> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
> going to happen, I do case analysis instead.
> 
> --Chun
> 
> Il 14/02/19 18:12, Konrad Slind ha scritto:
>> It's a deliberate choice. See the discussion in Section 1.2 of
>> 
>> 
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf
>> 
>> 
>> 
>> On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
>> mailto:binghe.l...@gmail.com>> wrote:
>> 
>> Hi,
>> 
>> in HOL's realTheory, division is defined by multiplication:
>> 
>> [real_div]  Definition
>> 
>>   ⊢ ∀x y. x / y = x * y⁻¹
>> 
>> and zero multiplies any other real number equals to zero, which is
>> definitely true:
>> 
>>[REAL_MUL_LZERO]  Theorem
>> 
>>   ⊢ ∀x. 0 * x = 0
>> 
>> However, above two theorems together gives ``0 / 0 = 0``, as shown
>> below:
>> 
>> > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
>> val it = ⊢ 0 / 0 = 0: thm
>> 
>> How do I understand this result? Is there anything "wrong"?
>> 
>> (The same problems happens also in extrealTheory, since the 
>> definition
>> of `*` finally reduces to `*` of real numbers)
>> 
>> Regards,
>> 
>> Chun Tian
>> 
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net 
>> 
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


   [(("real", "ABS_DIV"),
 (⊢ ∀y. y ≠ 0 ⇒ ∀x. abs (x / y) = abs x / abs y, Thm)),
(("real", "div_rat"),
 (⊢ x / y / (u / v) =
if (u = 0) ∨ (v = 0) then x / y / unint (u / v)
else if y = 0 then unint (x / y) / (u / v)
else x * v / (y * u), Thm)),
(("real", "div_ratl"),
 (⊢ x / y / z =
if y = 0 then unint (x / y) / z
else if z = 0 then unint (x / y / z)
else x / (y * z), Thm)),
(("real", "div_ratr"),
 (⊢ x / (y / z) =
if (y = 0) ∨ (z = 0) then x / unint (y / z) else x * z / y, Thm)),
(("real", "NUM_FLOOR_DIV"),
 (⊢ 0 ≤ x ∧ 0 < y ⇒  (x / y) * y ≤ x, Thm)),
(("real", "NUM_FLOOR_DIV_LOWERBOUND"),
 (⊢ 0 ≤ x ∧ 0 < y ⇒ x < &(flr (x / y) + 1) * y, Thm)),
(("real", "real_div"), (⊢ ∀x y. x / y = x * y⁻¹, Def)),
(("real", "REAL_DIV_ADD"), (⊢ ∀x y z. y / x + z / x = (y + z) / x, 
Thm)),
(("real", "REAL_DIV_DENOM_CANCEL"),
 (⊢ ∀x y z. x ≠ 0 ⇒ (y / x / (z / x) = y / z), Thm)),
(("real", "REAL_DIV_DENOM_CANCEL2"),
 (⊢ ∀y z. y / 2 / (z / 2) = y / z, Thm)),
(("real", "REAL_DIV_DENOM_CANCEL3"),
 (⊢ ∀y z. y / 3 / (z / 3) = y / z, Thm)),
(("real", "REAL_DIV_INNER_CANCEL"),
 (⊢ ∀x y z. x ≠ 0 ⇒ (y / x * (x / z) = y / z), Thm)),
(("real", "REAL_DIV_INNER_CANCEL2"),
 (⊢ ∀y z. y / 2 * (2 / z) = y / z, Thm)),
(("real", "REAL_DIV_INNER_CANCEL3"),
 (⊢ 

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

I'm going to use the following definition for `extreal_div`:

(* old definition of `extreal_div`, which allows `0 / 0 = 0`
val extreal_div_def = Define
   `extreal_div x y = extreal_mul x (extreal_inv y)`;

   new definition of `extreal_div`, excluding the case `0 / 0`: *)
val extreal_div_def = Define
   `extreal_div x y = if (y = Normal 0) then ARB
  else extreal_mul x (extreal_inv y)`;

previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as
 antecedent, which makes perfectly senses.

P.S. the division of extended reals in HOL4 are not used until the
statement and proof of Radon-Nikodým theorem, then the conditional
probability.

--Chun

Il 15/02/19 17:39, Mark Adams ha scritto:
> I think there is definitely an advantage in keeping ``x/y`` undefined
> (even granted that it will always be possible to prove ``?y. x/0 = y``),
> namely that it means that your proofs are much more likely to directly
> translate to other formalisms of real numbers where '/' is not total.
> 
> Of course there is also a disadvantage, in that it makes proof harder. 
> But then, arguably, being forced to justify that we are staying within
> the "normal" domain of the function is probably a good thing (in a
> similar way as being forced to conform to a type system is a good
> thing).  I understand that, historically, it is this disadvantage of
> harder proofs that was the reason for making ``0/0=0`` in HOL.  It's
> much easier for automated routines if they don't have to consider side
> conditions.
> 
> Mark.
> 
> On 15/02/2019 08:56, Chun Tian (binghe) wrote:
>> Thanks to all kindly answers.
>>
>> Even I wanted ``0 / 0 = 0`` to be excluded from at least
>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I
>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
>> going to happen, I do case analysis instead.
>>
>> --Chun
>>
>> Il 14/02/19 18:12, Konrad Slind ha scritto:
>>> It's a deliberate choice. See the discussion in Section 1.2 of
>>>
>>> http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf
>>>
>>>
>>>
>>>
>>> On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
>>> mailto:binghe.l...@gmail.com>> wrote:
>>>
>>>     Hi,
>>>
>>>     in HOL's realTheory, division is defined by multiplication:
>>>
>>>     [real_div]  Definition
>>>
>>>           ⊢ ∀x y. x / y = x * y⁻¹
>>>
>>>     and zero multiplies any other real number equals to zero, which is
>>>     definitely true:
>>>
>>>        [REAL_MUL_LZERO]  Theorem
>>>
>>>           ⊢ ∀x. 0 * x = 0
>>>
>>>     However, above two theorems together gives ``0 / 0 = 0``, as shown
>>>     below:
>>>
>>>     > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
>>>     val it = ⊢ 0 / 0 = 0: thm
>>>
>>>     How do I understand this result? Is there anything "wrong"?
>>>
>>>     (The same problems happens also in extrealTheory, since the
>>> definition
>>>     of `*` finally reduces to `*` of real numbers)
>>>
>>>     Regards,
>>>
>>>     Chun Tian
>>>
>>>     ___
>>>     hol-info mailing list
>>>     hol-info@lists.sourceforge.net
>>> 
>>>     https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Mark Adams]

I think there is definitely an advantage in keeping ``x/y`` undefined 
(even granted that it will always be possible to prove ``?y. x/0 = y``), 
namely that it means that your proofs are much more likely to directly 
translate to other formalisms of real numbers where '/' is not total.


Of course there is also a disadvantage, in that it makes proof harder.  
But then, arguably, being forced to justify that we are staying within 
the "normal" domain of the function is probably a good thing (in a 
similar way as being forced to conform to a type system is a good 
thing).  I understand that, historically, it is this disadvantage of 
harder proofs that was the reason for making ``0/0=0`` in HOL.  It's 
much easier for automated routines if they don't have to consider side 
conditions.


Mark.

On 15/02/2019 08:56, Chun Tian (binghe) wrote:

Thanks to all kindly answers.

Even I wanted ``0 / 0 = 0`` to be excluded from at least
"extreal_div_def" (in extrealTheory), I found no way to do that. All I
can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
going to happen, I do case analysis instead.

--Chun

Il 14/02/19 18:12, Konrad Slind ha scritto:

It's a deliberate choice. See the discussion in Section 1.2 of

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf



On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
mailto:binghe.l...@gmail.com>> wrote:

Hi,

in HOL's realTheory, division is defined by multiplication:

[real_div]  Definition

      ⊢ ∀x y. x / y = x * y⁻¹

and zero multiplies any other real number equals to zero, which is
definitely true:

   [REAL_MUL_LZERO]  Theorem

      ⊢ ∀x. 0 * x = 0

However, above two theorems together gives ``0 / 0 = 0``, as shown
below:

> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
val it = ⊢ 0 / 0 = 0: thm

How do I understand this result? Is there anything "wrong"?

(The same problems happens also in extrealTheory, since the 
definition

of `*` finally reduces to `*` of real numbers)

Regards,

Chun Tian

___
hol-info mailing list
hol-info@lists.sourceforge.net 


https://lists.sourceforge.net/lists/listinfo/hol-info




___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

Thanks to all kindly answers.

Even I wanted ``0 / 0 = 0`` to be excluded from at least
"extreal_div_def" (in extrealTheory), I found no way to do that. All I
can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
going to happen, I do case analysis instead.

--Chun

Il 14/02/19 18:12, Konrad Slind ha scritto:
> It's a deliberate choice. See the discussion in Section 1.2 of
> 
> http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf
> 
> 
> 
> On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>> wrote:
> 
> Hi,
> 
> in HOL's realTheory, division is defined by multiplication:
> 
> [real_div]  Definition
> 
>       ⊢ ∀x y. x / y = x * y⁻¹
> 
> and zero multiplies any other real number equals to zero, which is
> definitely true:
> 
>    [REAL_MUL_LZERO]  Theorem
> 
>       ⊢ ∀x. 0 * x = 0
> 
> However, above two theorems together gives ``0 / 0 = 0``, as shown
> below:
> 
> > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
> val it = ⊢ 0 / 0 = 0: thm
> 
> How do I understand this result? Is there anything "wrong"?
> 
> (The same problems happens also in extrealTheory, since the definition
> of `*` finally reduces to `*` of real numbers)
> 
> Regards,
> 
> Chun Tian
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Michael.Norrish]

You could write

  HD ([]:’a list) = @x:’a. T

or, equivalently, HD [] = ARB.

Michael

From: "buday.gerg...@uni-eszterhazy.hu" 
Date: Friday, 15 February 2019 at 15:34
To: hol-info , "Norrish, Michael (Data61, 
Acton)" 
Subject: Re: [Hol-info] 0 / 0 = 0 ???

Is HD [] at all possible to define? For some fixed list type yes but in general 
for [] : 'a list ?
- Gergely
Az Android Outlook<https://aka.ms/ghei36> letöltése



On Fri, Feb 15, 2019 at 12:00 AM +0100, 
mailto:michael.norr...@data61.csiro.au>> wrote:
The author of LENGTH_TL probably didn’t have access to the updated definition 
of TL.  Once upon a time, the philosophy was to keep more things unspecified so 
that one could not know which list TL [] denoted.  I assume, not having looked 
into the relevant history, that LENGTH_TL dates back to that earlier period.  
In that vein, natural number division does not define what x DIV 0 might happen 
to be at all.

Pleasantly, the feature of starting out with things unspecified is that it is 
sound to later specify exactly what the border cases might be.  TAKE, DROP and 
ZIP have also picked up defined values for what were unspecified cases 
relatively recently.  (These functions all map into ranges where halfway 
reasonable defaults seem to exist.  It’s harder to imagine what HD [] should 
be. )

Michael

From: Thomas Sewell 
Date: Friday, 15 February 2019 at 04:15
To: "Chun Tian (binghe)" , hol-info 

Subject: Re: [Hol-info] 0 / 0 = 0 ???


This is one of the most common questions about HOL.



HOL is a logic of total functions. There are some expressions, like division by 
zero and the head of an empty list, which we often intuitively think of as 
special exceptional values. But HOL's type system doesn't have special 
exceptional values, so ``HD []`` and ``0 \ 0`` have to be values of the correct 
type.



We could choose to define HD and the division operator so that it was not 
possible to prove what these unusual values are. But that doesn't mean quite 
the same thing as an exception. For instance, however HD and division were 
defined, we can still prove equalities about them:

``HD [] + (0 / 0) - HD [] - (0 / 0) = 0``.



Since we have to have normal values, it's often convenient to pick sensible 
defaults, since they make some theorems true without side conditions. For 
instance, we pick that "0 - 1 = 0" in numerals, and "TL [] = []", which happens 
to make "LENGTH (TL xs) = (LENGTH xs - 1)" unconditionally true. Curiously, in 
HOL4, the author of the LENGTH_TL theorem didn't seem to realise that.



If this bothers you a lot, you can consider the HOL ``x \ y`` expression to map 
to the expression "if x = 0 then 0 else (x \ y)" in whatever your intuitive 
logic is.



Cheers,

Thomas.





Cheers,

Thomas.






From: Chun Tian (binghe) 
Sent: Thursday, February 14, 2019 5:40:36 PM
To: HOL
Subject: [Hol-info] 0 / 0 = 0 ???

Hi,

in HOL's realTheory, division is defined by multiplication:

[real_div]  Definition

  ⊢ ∀x y. x / y = x * y⁻¹

and zero multiplies any other real number equals to zero, which is
definitely true:

   [REAL_MUL_LZERO]  Theorem

  ⊢ ∀x. 0 * x = 0

However, above two theorems together gives ``0 / 0 = 0``, as shown below:

> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
val it = ⊢ 0 / 0 = 0: thm

How do I understand this result? Is there anything "wrong"?

(The same problems happens also in extrealTheory, since the definition
of `*` finally reduces to `*` of real numbers)

Regards,

Chun Tian
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[buday.gergely]

Is HD [] at all possible to define? For some fixed list type yes but in general 
for [] : 'a list ?




- Gergely




Az Android Outlook letöltése







On Fri, Feb 15, 2019 at 12:00 AM +0100,  wrote:




















The author of LENGTH_TL probably didn’t have access to the updated definition 
of TL.  Once upon a time, the philosophy was to keep more things unspecified so 
that one could not know which list TL [] denoted.  I assume,
 not having looked into the relevant history, that LENGTH_TL dates back to that 
earlier period.  In that vein, natural number division does not define what x 
DIV 0 might happen to be at all.


 


Pleasantly, the feature of starting out with things unspecified is that it is 
sound to later specify exactly what the border cases might be.  TAKE, DROP and 
ZIP have also picked up defined values for what were unspecified
 cases relatively recently.  (These functions all map into ranges where halfway 
reasonable defaults seem to exist.  It’s harder to imagine what HD [] should 
be. )


 


Michael


 



From: Thomas Sewell 

Date: Friday, 15 February 2019 at 04:15

To: "Chun Tian (binghe)" , hol-info 


Subject: Re: [Hol-info] 0 / 0 = 0 ???




 





This is one of the most common questions about HOL.


 


HOL is a logic of total functions. There are some expressions, like division by 
zero and the head of an empty list, which we often intuitively think of as 
special exceptional values. But HOL's type system doesn't
 have special exceptional values, so ``HD []`` and ``0 \ 0`` have to be values 
of the correct type.


 


We could choose to define HD and the division operator so that it was not 
possible to prove what these unusual values are. But that doesn't mean quite 
the same thing as an exception. For instance, however HD and
 division were defined, we can still prove equalities about them:


``HD [] + (0 / 0) - HD [] - (0 / 0) = 0``.


 


Since we have to have normal values, it's often convenient to pick sensible 
defaults, since they make some theorems true without side conditions. For 
instance, we pick that "0 - 1 = 0" in numerals, and "TL [] =
 []", which happens to make "LENGTH (TL xs) = (LENGTH xs - 1)" unconditionally 
true. Curiously, in HOL4, the author of the LENGTH_TL theorem didn't seem to 
realise that.


 


If this bothers you a lot, you can consider the HOL ``x \ y`` expression to map 
to the expression "if x = 0 then 0 else (x \ y)" in whatever your intuitive 
logic is.


 


Cheers,


    Thomas.


 


 


Cheers,


    Thomas.


 


 







From: Chun Tian (binghe) 

Sent: Thursday, February 14, 2019 5:40:36 PM

To: HOL

Subject: [Hol-info] 0 / 0 = 0 ??? 



 






Hi,



in HOL's realTheory, division is defined by multiplication:



[real_div]  Definition



  ⊢
∀x y. x / y = x * y⁻¹



and zero multiplies any other real number equals to zero, which is

definitely true:



   [REAL_MUL_LZERO]  Theorem



  ⊢
∀x. 0 * x = 0



However, above two theorems together gives ``0 / 0 = 0``, as shown below:



> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);

val it = ⊢ 0 / 0 = 0: thm



How do I understand this result? Is there anything "wrong"?



(The same problems happens also in extrealTheory, since the definition

of `*` finally reduces to `*` of real numbers)



Regards,



Chun Tian









___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Jeremy Dawson]

Sorry for my previous confusing email, this is something I didn't know 
about. It seems now TL and TL_T are the same.

Jeremy

On 02/15/2019 09:59 AM, michael.norr...@data61.csiro.au wrote:
> the updated definition of TL.

___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Konrad Slind]

It's a deliberate choice. See the discussion in Section 1.2 of

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf



On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) 
wrote:

> Hi,
>
> in HOL's realTheory, division is defined by multiplication:
>
> [real_div]  Definition
>
>   ⊢ ∀x y. x / y = x * y⁻¹
>
> and zero multiplies any other real number equals to zero, which is
> definitely true:
>
>[REAL_MUL_LZERO]  Theorem
>
>   ⊢ ∀x. 0 * x = 0
>
> However, above two theorems together gives ``0 / 0 = 0``, as shown below:
>
> > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
> val it = ⊢ 0 / 0 = 0: thm
>
> How do I understand this result? Is there anything "wrong"?
>
> (The same problems happens also in extrealTheory, since the definition
> of `*` finally reduces to `*` of real numbers)
>
> Regards,
>
> Chun Tian
>
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info