Stream: new members
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.
Yury G. Kudryashov (Dec 09 2019 at 23:29):
all k, divides n k -> ...
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))
Ender Doe (Dec 09 2019 at 23:37):
Ahh I see thank you very much.
Kevin Buzzard (Dec 10 2019 at 00:06):
And remember that that's
Last updated: May 12 2021 at 04:19 UTC