Stream: Beginner Questions

Topic: Conditions after the "for all" quantifier

Chris_Y (Jul 06 2023 at 12:10):

Hi everyone, sorry this might be a trivial question, but how would you add conditions to the variable after the "for all" quantifier?

For example, I'd like to write "For all naturals N such that N mod m = m - 1, there exists integers b and r with certain properties" and I'm not sure how to write the such that bit. I tried writing the statement in this way:

have "∃r::nat. (r≤m-3) ∧ [N=b1+r] (mod m)" if asm3:"(N::nat) mod m =m-1"

and from here I can deduce

proof (state)
this:
  N mod m = m - 1 ⟹ ∃b r. r ≤ m - 3 ∧ [int N = b + int r] (mod int m) ∧ (b = b1 ∨ b = b2)

However, I'm not sure whether this contains the ∀N::nat. requirement. I'm guessing not, as at the end of my proof Isabelle is unable to combine to following to show the intended goal (either by auto or sledgehammer)

using this:
    ∀N. N mod m = m - 1 ∨ N mod m = m - 2 ∨ N mod m ≤ m - 3
    N mod m ≤ m - 3 ⟹ ∃b r. r ≤ m - 3 ∧ [int N = b + int r] (mod int m) ∧ (b = b1 ∨ b = b2)
    N mod m = m - 2 ⟹ ∃b r. r ≤ m - 3 ∧ [int N = b + int r] (mod int m) ∧ (b = b1 ∨ b = b2)
    N mod m = m - 1 ⟹ ∃b r. r ≤ m - 3 ∧ [int N = b + int r] (mod int m) ∧ (b = b1 ∨ b = b2)

goal (1 subgoal):
 1. ∀N. ∃b r. r ≤ m - 3 ∧ [int N = b + int r] (mod int m) ∧ (b = b1 ∨ b = b2)

Any help or advice would be greatly appreciated! Thank you!

Mathias Fleury (Jul 06 2023 at 12:21):

   have X if Y for N

Mathias Fleury (Jul 06 2023 at 12:21):

very useful version of have

Manuel Eberl (Jul 06 2023 at 12:51):

Yes. Makarius calls these "eigencontexts". They've been available for a few years and I use them a lot.

Manuel Eberl (Jul 06 2023 at 12:52):

of course you can also write ∀N. P N ⟶ Q N or, using the meta for-all quantifier, ⋀N. P n ⟹ Q X.

Chris_Y (Jul 06 2023 at 13:38):

That works! No words could describe my happiness. Thank you!

Last updated: Apr 27 2024 at 16:16 UTC