Zulip Chat Archive

Stream: new members

Topic: what is "have key := [...]" the backwards way


Mason McBride (Apr 06 2022 at 02:22):

If I have (h : P -> Q) and (g : Q -> R) and (p : P) how do I make an r : R without using "have q := h p" "have r := g q"? I feel like it's apply but I always think I can do "apply succ_ne_zero at H"

Julian Berman (Apr 06 2022 at 02:30):

import tactic
example {P Q R : Prop} (h : P  Q) (g : Q  R) (p : P) : R := by library_search
 -- Try this: exact g (h p)

Mason McBride (Apr 06 2022 at 02:44):

I appreciate it. So what's the difference between exact and apply?

Julian Berman (Apr 06 2022 at 03:00):

exact basically is you saying "I want to solve the goal now, here's a term"

Julian Berman (Apr 06 2022 at 03:01):

apply is your arguing backwards, but you can't do it to a hypothesis, only to the goal

Julian Berman (Apr 06 2022 at 03:02):

You could instead do have hr := g (h p) which will give you a new hypothesis of type R -- but then once you have that hypothesis, now you do exact hr to close the goal.

Jireh Loreaux (Apr 06 2022 at 03:24):

If your goal is R, then you could also do refine g _ to end up with a goal of Q. refine is like exact except that you can give it holes (underscores), and any that it can't automatically fill it will create new goals for. So, for example, if your goal is R and foo : P → Q → R, then refine foo _ _ would give you two goals, namely P and Q.


Last updated: Dec 20 2023 at 11:08 UTC