Stream: Coq users

Topic: Tactics for definitional equality

walker (Apr 13 2022 at 23:15):

Somehow in my assumptions I had something that looks like this:

filtered_var:= l : list A

I need to somehow convert to something that looks like:

H: filter_var = l

so I can use it with normal tactics as subst. The problem is that some places I see filtered_var used while in other places I see l used and I cannot get coq to replace with one term.

Paolo Giarrusso (Apr 13 2022 at 23:34):

filtered_var is a local definition, so unfold filtered_var will replace it by its body l; you can also do simpl before intros, as in the snippet I posted recently

Paolo Giarrusso (Apr 13 2022 at 23:35):

(in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Dependent.20vectors)

walker (Apr 13 2022 at 23:36):

oh I see, I always had the pattern of intros;subst;simpl in *. but thanks for the unfold trick!

walker (Apr 13 2022 at 23:36):

never noticed that order matters

Paolo Giarrusso (Apr 14 2022 at 02:01):

easy part: simpl only acts on the conclusion, otherwise you want simpl in * to do each hypothesis.

Paolo Giarrusso (Apr 14 2022 at 02:01):

Sorry, not easy, but it comes up often

Paolo Giarrusso (Apr 14 2022 at 02:02):

It's less common to have let in goals, so these subtleties come up less often

Pierre Courtieu (Apr 23 2022 at 09:53):

lazy zeta can also be more focused on just unfolding lets than simpl.

Last updated: Oct 05 2023 at 02:01 UTC