## Stream: maths

### Topic: What is this operator?

#### 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

#### 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...)

#### 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"

#### 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...

#### 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...

#### Damiano Testa (Dec 07 2020 at 14:00):

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

#### Mario Carneiro (Dec 07 2020 at 14:01):

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

#### Damiano Testa (Dec 07 2020 at 14:01):

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

#### 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

#### 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....

#### 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...

#### Mario Carneiro (Dec 07 2020 at 14:06):

I put parentheses in to clarify

#### 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"

#### 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)

#### Sebastien Gouezel (Dec 07 2020 at 14:10):

"nonempty implication" instead of "positive application"?

#### Johan Commelin (Dec 07 2020 at 14:15):

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

#### 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

#### Eric Wieser (Dec 07 2020 at 14:15):

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

#### Mario Carneiro (Dec 07 2020 at 14:16):

Oh that's how that works

#### Mario Carneiro (Dec 07 2020 at 14:16):

The syntax of notation commands is a mystery to me

#### Eric Wieser (Dec 07 2020 at 14:16):

Maybe adjusting the binding precedence can make >> work

#### 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

oh, so it does

#### 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)

#### 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.

#### Mario Carneiro (Dec 07 2020 at 14:32):

ah yes, that's an interesting example

#### 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