Zulip Chat Archive

Stream: new members

Topic: Syntax question about universal quantification ∀


view this post on Zulip Ender Doe (Dec 09 2019 at 22:46):

Hi, I am going through chapter 4 in the documentation. I have a question about ∀. Is there a nice syntactic way to put a condition on a forall? For example I am going through the exercises where you define prime numbers. What I came up with was this :
def prime (n : ℕ) : Prop :=(n > 1) ∧ (∀ k : ℕ, (k = 1) ∨ ¬(divides n k)).
It seems like the ∨ part at the end is somewhat burdensome for describing a constraint. Some of the later exercises such as the Goldbach weak Conjecture were even hairier when using ∨ as a constraint mechanism.

view this post on Zulip Yury G. Kudryashov (Dec 09 2019 at 23:29):

all k, divides n k -> ...

view this post on Zulip Marc Huisinga (Dec 09 2019 at 23:33):

you can do the following:
first, transform to the variant you probably intended (you're missing the k = n case and the order in divides is mixed up)

def prime (n : ℕ) : Prop := (n > 1) ∧ (∀ k : ℕ, (k = 1) ∨ (k = n) ∨ ¬(divides k n))

then, use implication instead of or (as described by yury).

def prime (n : ℕ) : Prop := (n > 1) ∧ (∀ k : ℕ, divides k n → (k = 1) ∨ (k = n))

then, using the notation described in TPIL, you can do the following:

def prime (n : ℕ) : Prop := (n > 1) ∧ (∀ k ∣ n, (k = 1) ∨ (k = n))

view this post on Zulip Ender Doe (Dec 09 2019 at 23:37):

Ahh I see thank you very much.

view this post on Zulip Kevin Buzzard (Dec 10 2019 at 00:06):

And remember that that's \| not |


Last updated: May 12 2021 at 04:19 UTC