Zulip Chat Archive

Stream: new members

Topic: Extracting from a forall


view this post on Zulip Dev-Indra (Apr 26 2020 at 17:22):

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?

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:23):

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

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:24):

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

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:34):

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

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:35):

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

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:36):

So how do I feed in a witness?

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:36):

it's a function

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:37):

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

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:37):

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

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:38):

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

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:39):

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.

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:40):

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

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:40):

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

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:42):

@Jalex Stark Thanks

view this post on Zulip Jalex Stark (Apr 26 2020 at 17:44):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 26 2020 at 17:45):

The ASCII version of should be ->.

view this post on Zulip Dev-Indra (Apr 26 2020 at 17:48):

my bad


Last updated: May 14 2021 at 03:27 UTC