Zulip Chat Archive

Stream: general

Topic: applyI

Reid Barton (Sep 07 2018 at 08:02):

Is there a variant on apply or refine which turns [...] arguments which couldn't be solved into new goals?

Simon Hudon (Sep 07 2018 at 08:03):

What are [...] arguments?

Reid Barton (Sep 07 2018 at 08:05):

Class arguments

Reid Barton (Sep 07 2018 at 08:05):

Or instances rather

Johannes Hölzl (Sep 07 2018 at 08:05):

apply_with allows you to provide a apply_cfg structure. I think { instances := ff }should add them to the goals.

Reid Barton (Sep 07 2018 at 08:05):

Ooh

Reid Barton (Sep 07 2018 at 08:12):

Yes, it worked.

Kevin Buzzard (Sep 07 2018 at 08:53):

Does convert work? I'm a big convert to convert. It seems to allow me to write proofs forwards like a mathematician would. "This term is actually the answer; I'll now pick up the pieces".

Reid Barton (Sep 07 2018 at 09:00):

Huh, it does!

Reid Barton (Sep 07 2018 at 09:04):

That's really good to know--I already wrote a couple "backwards" proofs involving instances (which I think are really forwards, in the sense that you are building up new known statements from old ones, rather than breaking down the goal) and I was annoyed that I couldn't write them in the normal fashion.

Kevin Buzzard (Sep 07 2018 at 09:05):

How long has convert existed? I can't believe I didn't notice it wasn't there. I only found it was there about a week ago and now I kind of feel stupid that I hadn't realised that I wanted it.

Reid Barton (Sep 07 2018 at 09:06):

For example

begin
  letI : Π (A : K ↝ Type v), is_iso (colimit.pre A (F.comp G)) :=
  begin intro A, rw colimit.pre_comp, apply_instance, end,
  apply is_cofinal_of_induced_is_iso
end

is now

begin
  convert is_cofinal_of_induced_is_iso _,
  intro A, rw colimit.pre_comp, apply_instance
end

Johan Commelin (Sep 07 2018 at 09:07):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/ZFC.20equality/near/127216190
We need better documentation!

Reid Barton (Sep 07 2018 at 09:07):

April
https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/apply.20with.20new.20equality.20goals/near/125558382

Reid Barton (Sep 07 2018 at 10:41):

Maybe it would still be good to have an applyI tactic which is just apply with { instances := ff }, though.

Kenny Lau (Sep 07 2018 at 10:48):

maybe we should have 32768 names for our 15 boolean configurations of simp

Patrick Massot (Sep 07 2018 at 10:58):

Indeed I would love to read more examples of using convert.

Last updated: Dec 20 2023 at 11:08 UTC