What is this operator?

Stream: maths

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Mario Carneiro]

I put parentheses in to clarify

[Mario Carneiro]

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

[Mario Carneiro]

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]

"nonempty implication" instead of "positive application"?

[Johan Commelin]

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

[Eric Wieser]

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]

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

[Mario Carneiro]

Oh that's how that works

[Mario Carneiro]

The syntax of notation commands is a mystery to me

[Eric Wieser]

Maybe adjusting the binding precedence can make >> work

[Eric Wieser]

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

[Mario Carneiro]

oh, so it does

[Eric Wieser]

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]

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]

ah yes, that's an interesting example

[Mario Carneiro]

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"