Extracting from a forall

Stream: new members

[Dev-Indra]

Suppose I am given ha: ∀ (n_1 : ℕ). How do I extract this n_1 for my proof? When we are given an existential statement we can uses cases h1 with u hu. Is there an analogous way for forall?

[Dev-Indra]

As an example here is my tactic state:

n : ℕ,
ge : n ≥ 2,
a : n ≥ 2 ∧ ∀ (n_1 : ℕ), dvd n_1 n → n_1 = 1 ∨ n_1 = n,
a1 b : ℕ,
hb : n = a1 * b ∧ a1 ≤ b ∧ b < n,
h1 : n = a1 * b,
temp : a1 ≤ b ∧ b < n,
h2 : a1 ≤ b,
h3 : b < n
⊢ false

[Dev-Indra]

and just in case def dvd (m n: ℕ): Prop := ∃ k, n = m * k

[Jalex Stark]

forall meant that you get the property for any n_1 whatsoever. You should be feeding it a witness, not the other way around!

[Jalex Stark]

code is generally preferred to tactic states by people trying to give help, since then we can recreate the tactic state in our own environment and figure out what works

[Dev-Indra]

So how do I feed in a witness?

[Jalex Stark]

it's a function

[Jalex Stark]

so for example a.right b : dvd b n → b = 1 ∨ b = n

[Dev-Indra]

def dvd (m n: ℕ): Prop := ∃ k, n = m * k
def prime (p : ℕ) : Prop := p ≥ 2 ∧ ∀ n, dvd n p → n = 1 ∨ n = p
def composite (d : ℕ): Prop:= ∃ (a b: ℕ), d = a*b ∧ a ≤ b ∧ b < d

lemma composite_not_prime (n:ℕ ) (ge: n≥ 2): ( composite n ==> ¬ (prime n) ) :=
begin
       intros h,
      rw composite at h,
      by_contradiction,
      rw prime at a,

      cases h with a1 ha1,
      cases ha1 with b hb,

 have h1: n = a1*b, from and.left hb,
      have temp: a1 ≤ b ∧ b < n, from and.right hb,
      have h2: a1 ≤ b, from and.left temp,
      have h3: b < n, from and.right temp,
end

[Dev-Indra]

So how would I use this function in my code above?

[Dev-Indra]

I want to use by statement h1 in my tactic state previously to show that dvd n b I want to use b as my n_1.

[Jalex Stark]

Like I said before, a.right b should be a term whose type is interesting to you

[Jalex Stark]

you could write e.g. have hb := a.right b,

[Dev-Indra]

@Jalex Stark Thanks

[Jalex Stark]

what's the deal with this ==> arrow? it doesn't compile for me ant I had to replace it with →

[Bryan Gin-ge Chen]

The ASCII version of → should be ->.

[Dev-Indra]

my bad