Zulip Chat Archive

Stream: maths

Topic: What is this operator?


view this post on Zulip Mario Carneiro (Dec 07 2020 at 13:46):

This is kind of a weird question, but I find myself needing to make use of the following logical operator:

def foo {α : Type} (P Q : α  Prop) : Prop := ( x, P x)  ( x, (P x  Q x))

notation `𝔽` P ` >> ` Q := foo P Q

variables {α : Type} (P Q : α  Prop)
#check 𝔽 (λx, P x) >> (λx, Q x)
-- #check 𝔽 x, P x >> Q x

What would you call it? Bonus points if you can figure out how to declare the commented notation

view this post on Zulip Damiano Testa (Dec 07 2020 at 13:52):

Though not completely related, a porism is a statement that, as long as it is true once, it is always true (see Poncelet's porism). Hope that this helps!

(I may have completely misunderstood the question, though...)

view this post on Zulip Mario Carneiro (Dec 07 2020 at 13:57):

the working title for it is "positive implication". It's pretty weird since it isn't monotone or antitone wrt the first argument. You might gloss it as "P implies Q, but not vacuously"

view this post on Zulip Damiano Testa (Dec 07 2020 at 13:59):

It comes up "often": a topological space is connected if it is non-empty and [something else]. It is frequent to simply check the something else, though. I rarely like this...

view this post on Zulip Damiano Testa (Dec 07 2020 at 14:00):

A natural number is prime if it is at least 2 and had only 1 and itself as prime divisors. The latter condition is often the only one to be checked...

view this post on Zulip Damiano Testa (Dec 07 2020 at 14:00):

(Often, likely outside of the crowd of Lean users...)

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:01):

well, notice that the same P has to be used in both conjuncts

view this post on Zulip Damiano Testa (Dec 07 2020 at 14:01):

Actually, I was using the same P and the same Q! Sorry!

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:01):

the connectedness example might fit this, if [something else] is a statement about every point in the space

view this post on Zulip Damiano Testa (Dec 07 2020 at 14:04):

Hmmm, to be honest, I am now a little skeptical that either of my examples fit what you want....

view this post on Zulip Damiano Testa (Dec 07 2020 at 14:05):

I think that I read your initial statement as (∃ x, P x) ∧ ∀ x, P x. My examples might fit this operator...

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:06):

I put parentheses in to clarify

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:07):

I think this operator has been considered as a way to read the natural language "if then"

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:09):

That is, "when I go to lunch, I order a sandwich" is nominally a universal conditional, but there is some additional pragmatic content that implies that I go to lunch sometimes (or else it would be a weird thing to say)

view this post on Zulip Sebastien Gouezel (Dec 07 2020 at 14:10):

"nonempty implication" instead of "positive application"?

view this post on Zulip Johan Commelin (Dec 07 2020 at 14:15):

@Mario Carneiro didn't you just suggest a name? when, or the when-then operator.

view this post on Zulip Eric Wieser (Dec 07 2020 at 14:15):

For the bonus points:

notation `𝔽` binders `, ` s:(scoped P, P) ` >>' ` r:(scoped P, P) := foo s r

variables {α : Type} (P Q : α  Prop)

#check 𝔽 x, P x >>' Q x

view this post on Zulip Eric Wieser (Dec 07 2020 at 14:15):

>> doesn't seem to work because it's already an operator

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:16):

Oh that's how that works

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:16):

The syntax of notation commands is a mystery to me

view this post on Zulip Eric Wieser (Dec 07 2020 at 14:16):

Maybe adjusting the binding precedence can make >> work

view this post on Zulip Eric Wieser (Dec 07 2020 at 14:17):

Also your original version #check 𝔽 (λx, P x) >> (λx, Q x) seems to poison the parser on the following line

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:17):

oh, so it does

view this post on Zulip Eric Wieser (Dec 07 2020 at 14:17):

With your version, this fails on the second line:

#check 𝔽 (λx, P x) >> (λx, Q x)
#check 𝔽 (λx, P x) >> (λx, Q x)

view this post on Zulip Damiano Testa (Dec 07 2020 at 14:30):

Let me try with another example. In the case in which α = ℕ and Q n = P n.succ your operator is "eventual induction", right?

For instance, P n := 37 \leq n and Q n := 37 \leq n.succ fit the requirements?

Kind of a silly example, however, P 36 is false, while Q 36 is true. Otherwise, they are either both true or both false.

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:32):

ah yes, that's an interesting example

view this post on Zulip Mario Carneiro (Dec 07 2020 at 14:35):

The context where this came up for me was in the safety property for a nondeterministic state machine: if s is "safe" then this means that there exists s' such that s -> s', and every s' such that s -> s' is "safe"


Last updated: May 18 2021 at 07:19 UTC