Re: [isabelle-dev] not-exists problem

[Makarius]

On 13/09/16 01:46, Lawrence Paulson wrote:
> We have a problem with the ∄ operator, when existential quantifiers are 
> nested:
> 
> lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
>   by (rule refl)
> 
> Note that ∄x y. P x y would be fine.

Back to this thread. There is now the following change:

changeset:   63912:9f8325206465
user:wenzelm
date:Sun Sep 18 17:59:28 2016 +0200
files:   src/HOL/HOL.thy
description:
clarified notation: iterated quantifier is negated as one chunk;


This is rather unspectacular. Instead of the 2005 version of negating
the term operator, the resulting syntax is negated via plain translations.

Hopefully this does not cause other confusions. If there are remaining
problems, we should sort them out before the release.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Lawrence Paulson]

The symmetry between the variables in ~(∃x y. P x y) is completely lost in ∄x. 
∃y. P x y. It’s a terrible notation.
Larry

> On 13 Sep 2016, at 22:56, Jasmin Blanchette  
> wrote:
> 
>> I’m not sure that this suggestion addresses my original problem: that the 
>> use of the negated quantifier (by an output translation, i.e., not by 
>> request) produced a confusing output. This output already contains only a 
>> single variable bound by ∄.
> 
> But to what extent do you find it confusing? Perhaps because our brains are 
> damaged by too much logic and too little math, many of us on this list seemed 
> to have no real issues parsing your example correctly.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Tobias Nipkow]

This discussion clearly shows that ∃! with multiple bound variables is a recipe 
for confusion and should be avoided.


Tobias

On 14/09/2016 09:49, Peter Lammich wrote:

On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au
wrote:

Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd
xy).

If you were going to support ∃!x y at all (and I can certainly see
the argument for forbidding it outright), I'd expect it to map to the
first formula above, and not the second.


So there seems to be no consensus on the meaning of "∃!x y".

Btw: I would strongly argue that a proposition like
"∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x.
∃!y"-semantics.

--
  Peter





Michael

On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber"  wrote:

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

+1

Best,
Tjark


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
abelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Peter Lammich]

On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au
wrote:
> Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd
> xy).
> 
> If you were going to support ∃!x y at all (and I can certainly see
> the argument for forbidding it outright), I'd expect it to map to the
> first formula above, and not the second.

So there seems to be no consensus on the meaning of "∃!x y".

Btw: I would strongly argue that a proposition like 
"∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x.
∃!y"-semantics.

--
  Peter



> 
> Michael
> 
> On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber"  le-dev-boun...@mailbroy.informatik.tu-muenchen.de on behalf of tjark.
> we...@it.uu.se> wrote:
> 
> On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> > I would have expected:
> > (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> > and
> > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))
> 
> +1
> 
> Best,
> Tjark
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> abelle-dev
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Michael.Norrish]

Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd xy).

If you were going to support ∃!x y at all (and I can certainly see the argument 
for forbidding it outright), I'd expect it to map to the first formula above, 
and not the second.

Michael

On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber" 
 wrote:

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

+1

Best,
Tjark


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Jasmin Blanchette]

> On 13.09.2016, at 23:33, Lawrence Paulson  wrote:
> 
> I’m not sure that this suggestion addresses my original problem: that the use 
> of the negated quantifier (by an output translation, i.e., not by request) 
> produced a confusing output. This output already contains only a single 
> variable bound by ∄.

But to what extent do you find it confusing? Perhaps because our brains are 
damaged by too much logic and too little math, many of us on this list seemed 
to have no real issues parsing your example correctly.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Lawrence Paulson]

I’m not sure that this suggestion addresses my original problem: that the use 
of the negated quantifier (by an output translation, i.e., not by request) 
produced a confusing output. This output already contains only a single 
variable bound by ∄.

Larry

> On 13 Sep 2016, at 19:56, Makarius  wrote:
> 
> Looking briefly over this thread, my impression is that the simplest
> solution is to disallow multiple variables for
> ∄ and ∃! as well.
> 
> We already have special quantifiers like ∃x:A that cannot be repeated
> (for very basic technical reasons). This means users are used to
> non-iterated quantifiers: it should cause less surprise than extra
> syntax that is unclear.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Makarius]

On 13/09/16 01:46, Lawrence Paulson wrote:
> We have a problem with the ∄ operator, when existential quantifiers are 
> nested:
> 
> lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
>   by (rule refl)
> 
> Note that ∄x y. P x y would be fine.

Looking briefly over this thread, my impression is that the simplest
solution is to disallow multiple variables for
∄ and ∃! as well.

We already have special quantifiers like ∃x:A that cannot be repeated
(for very basic technical reasons). This means users are used to
non-iterated quantifiers: it should cause less surprise than extra
syntax that is unclear.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Lawrence Paulson]

When mathematicians use such notations, they are communicating informally and 
they can count on the reader to understand what they mean. But that’s not how 
it works for us. Any notation that could be misinterpreted should be input only 
(assuming we support it at all). That way, the user immediately sees how it was 
interpreted.
Larry

> On 13 Sep 2016, at 11:27, Manuel Eberl  wrote:
> 
> The desired multi-variable semantics of ∄ seem obvious enough to me and I 
> think that this should be allowed.
> 
> For ∃!, the implicit complexity introduced by the pairing seems too much to 
> me, so I think this should be forbidden.
> 
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Manuel Eberl]

The desired multi-variable semantics of ∄ seem obvious enough to me and 
I think that this should be allowed.


For ∃!, the implicit complexity introduced by the pairing seems too much 
to me, so I think this should be forbidden.



On 13/09/16 10:41, Johannes Hölzl wrote:

There is even a third one: ∄!

I would vote to forbid the multiple variable case. At least for the
next release. Is it possible to restrict this by a mixfix syntax or
does it require to write a ML parse translations.

  - Johannes

Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb Tobias Nipkow:

There is a method to this madness: if B is a binder, "B x y. t" is
short for "B
x. B y. t". However, I agree that for ∄ and ∃! this is confusing and
one of the
solutions proposed should be adopted.

Tobias

On 13/09/2016 09:45, Peter Lammich wrote:

On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:

We have a problem with the ∄ operator, when existential
quantifiers
are nested:

lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
   by (rule refl)

I do not see a particular problem with this, however, not-exists
and
also exists-one have funny semantics when used with multiple
variables:

lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
 by (rule refl)

lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
 by (rule refl)

this leads to funny lemmas like:

lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
   by presburger

lemma also_strange: "∃!x y. x = abs (y::int)"
   by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
equal_neg_zero)


I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
and
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



We should either forbid multiple variables on those quantifiers, or
try
to figure out whether there is a widely-accepted consensus on their
meaning.

--
   Peter




Note that ∄x y. P x y would be fine.

Larry

~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
abel
le-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
elle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Johannes Hölzl]

There is even a third one: ∄!

I would vote to forbid the multiple variable case. At least for the
next release. Is it possible to restrict this by a mixfix syntax or
does it require to write a ML parse translations.

 - Johannes

Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb Tobias Nipkow:
> There is a method to this madness: if B is a binder, "B x y. t" is
> short for "B 
> x. B y. t". However, I agree that for ∄ and ∃! this is confusing and
> one of the 
> solutions proposed should be adopted.
> 
> Tobias
> 
> On 13/09/2016 09:45, Peter Lammich wrote:
> > 
> > On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:
> > > 
> > > We have a problem with the ∄ operator, when existential
> > > quantifiers
> > > are nested:
> > > 
> > > lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
> > >   by (rule refl)
> > I do not see a particular problem with this, however, not-exists
> > and
> > also exists-one have funny semantics when used with multiple
> > variables:
> > 
> > lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
> > by (rule refl)
> > 
> > lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
> > by (rule refl)
> > 
> > this leads to funny lemmas like:
> > 
> > lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
> >   by presburger
> > 
> > lemma also_strange: "∃!x y. x = abs (y::int)"
> >   by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
> > equal_neg_zero)
> > 
> > 
> > I would have expected:
> > (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> > and
> > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))
> > 
> > 
> > 
> > We should either forbid multiple variables on those quantifiers, or
> > try
> > to figure out whether there is a widely-accepted consensus on their
> > meaning.
> > 
> > --
> >   Peter
> > 
> > 
> > > 
> > > 
> > > Note that ∄x y. P x y would be fine.
> > > 
> > > Larry
> > > 
> > > ~/isabelle/Repos/src/HOL: hg id
> > > dca6fabd8060 tip
> > > 
> > > ___
> > > isabelle-dev mailing list
> > > isabelle-...@in.tum.de
> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> > > abel
> > > le-dev
> > ___
> > isabelle-dev mailing list
> > isabelle-...@in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> > 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Tjark Weber]

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

+1

Best,
Tjark


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Tobias Nipkow]

There is a method to this madness: if B is a binder, "B x y. t" is short for "B 
x. B y. t". However, I agree that for ∄ and ∃! this is confusing and one of the 
solutions proposed should be adopted.


Tobias

On 13/09/2016 09:45, Peter Lammich wrote:

On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:

We have a problem with the ∄ operator, when existential quantifiers
are nested:

lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
  by (rule refl)


I do not see a particular problem with this, however, not-exists and
also exists-one have funny semantics when used with multiple
variables:

lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
by (rule refl)

lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
by (rule refl)

this leads to funny lemmas like:

lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
  by presburger

lemma also_strange: "∃!x y. x = abs (y::int)"
  by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
equal_neg_zero)


I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
and
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



We should either forbid multiple variables on those quantifiers, or try
to figure out whether there is a widely-accepted consensus on their
meaning.

--
  Peter




Note that ∄x y. P x y would be fine.

Larry

~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Peter Lammich]

On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:
> We have a problem with the ∄ operator, when existential quantifiers
> are nested:
> 
> lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
>   by (rule refl)

I do not see a particular problem with this, however, not-exists and
also exists-one have funny semantics when used with multiple
variables:

lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
by (rule refl)

lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
by (rule refl)

this leads to funny lemmas like:

lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
  by presburger

lemma also_strange: "∃!x y. x = abs (y::int)"
  by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
equal_neg_zero)


I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
and
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



We should either forbid multiple variables on those quantifiers, or try
to figure out whether there is a widely-accepted consensus on their
meaning.

--
  Peter


> 
> Note that ∄x y. P x y would be fine.
> 
> Larry
> 
> ~/isabelle/Repos/src/HOL: hg id
> dca6fabd8060 tip
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] not-exists problem

[Lawrence Paulson]

We have a problem with the ∄ operator, when existential quantifiers are nested:

lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
  by (rule refl)

Note that ∄x y. P x y would be fine.

Larry

~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev