fact?

Stream: new members

[Damiano Testa]

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

[Adam Topaz]

assumption will work here, I suppose

[Damiano Testa]

I tried it:

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

[Adam Topaz]

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

[Adam Topaz]

Hmmmm....

[Ruben Van de Velde]

apply fact.out seems to work

[Damiano Testa]

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

[Adam Topaz]

Oh did fact change?

[Damiano Testa]

Ruben, thanks! Your approach works!

[Ruben Van de Velde]

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

[Damiano Testa]

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!

[Eric Wieser]

Yes, fact changed

[Eric Wieser]

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

[Mario Carneiro]

You can also use h.1

[Damiano Testa]

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

[Manuel Candales]

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?

[Alex J. Best]

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

[Manuel Candales]

wow, thanks! yeah that works

[Johan Commelin]

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.