Zulip Chat Archive

Stream: new members

Topic: fact?


view this post on Zulip Damiano Testa (Mar 25 2021 at 14:06):

Dear All,

I am trying to fix a now broken proof and I am stuck with proving the lemma below: how do I extract the fact from the fact?

Thanks!

import data.nat.prime

lemma obvious (p : ) [fact (nat.prime p)] :
  nat.prime p :=
begin
  sorry
end

view this post on Zulip Adam Topaz (Mar 25 2021 at 14:09):

assumption will work here, I suppose

view this post on Zulip Damiano Testa (Mar 25 2021 at 14:09):

I tried it:

assumption tactic failed
state:
p : ,
_inst_1 : fact (nat.prime p)
 nat.prime p

view this post on Zulip Adam Topaz (Mar 25 2021 at 14:09):

Or you can name the fact [ h : fact ... ]

view this post on Zulip Adam Topaz (Mar 25 2021 at 14:10):

Hmmmm....

view this post on Zulip Ruben Van de Velde (Mar 25 2021 at 14:10):

apply fact.out seems to work

view this post on Zulip Damiano Testa (Mar 25 2021 at 14:10):

This gives:

lemma obvious (p : ) [h : fact (nat.prime p)] :
  nat.prime p :=
begin
  exact h,
-- invalid type ascription, term has type
--   fact (nat.prime p)
-- but is expected to have type
--   nat.prime p
end

view this post on Zulip Adam Topaz (Mar 25 2021 at 14:11):

Oh did fact change?

view this post on Zulip Damiano Testa (Mar 25 2021 at 14:11):

Ruben, thanks! Your approach works!

view this post on Zulip Ruben Van de Velde (Mar 25 2021 at 14:13):

Also apply fact.elim, assumption or apply fact.elim, apply_instance. Not sure what's the intended approach

view this post on Zulip Damiano Testa (Mar 25 2021 at 14:14):

For the record, this works:

lemma obvious (p : ) [h : fact (nat.prime p)] :
  nat.prime p :=
fact.out _

and also

lemma obvious (p : ) [h : fact (nat.prime p)] :
  nat.prime p :=
fact.elim h

Thanks Ruben!

view this post on Zulip Eric Wieser (Mar 25 2021 at 14:28):

Yes, fact changed

view this post on Zulip Eric Wieser (Mar 25 2021 at 14:28):

Because @[class] def isn't allowed by one of mathport and lean4

view this post on Zulip Mario Carneiro (Mar 25 2021 at 16:56):

You can also use h.1

view this post on Zulip Damiano Testa (Mar 25 2021 at 17:22):

Thanks, Mario! I was convinced that I had tried to project, but... apparently not!

view this post on Zulip Manuel Candales (Apr 01 2021 at 23:56):

How can I do the opposite? Get a fact from a hypothesis. For example, I have h : nat.prime p. How do I use that in a theorem like zmod.exists_pow_two_eq_neg_one_iff_mod_four_ne_three?

view this post on Zulip Alex J. Best (Apr 02 2021 at 00:01):

In tactic mode you should be able to do haveI := fact.mk h (untested)

view this post on Zulip Manuel Candales (Apr 02 2021 at 00:08):

wow, thanks! yeah that works

view this post on Zulip Johan Commelin (Apr 02 2021 at 04:43):

If fact foo is your goal, then you can also write \<h\>, where \< and \> are the things you type into VScode to get the funny angle brackets.


Last updated: May 11 2021 at 00:31 UTC