Re: [isabelle-dev] not-exists problem
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
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
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
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
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
> 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
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
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
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
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
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
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
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
> On 13.09.2016, at 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, Like you I find ∄x. ∃y. P x y clear (albeit weird), but ∄x y. P x y is probably a better way to display the same thing. > lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))" > by (rule refl) That looks like a serious flaw. > lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))" > by (rule refl) Ditto. > We should either forbid multiple variables on those quantifiers, or try > to figure out whether there is a widely-accepted consensus on their > meaning. The best would be to forbid multiple variables for ∃!. For ∄, the situation is more complicated. We can forbid them, or we can interpret a single multi-variable ∄ as ∄∃...∃ (and in the other direction for printing). 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
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
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