Stream: Coq users

Topic: Tactic to refine a function branch


view this post on Zulip Gabriel Alfour (Nov 09 2023 at 18:21):

Very often, I have code that is similar to f x = Some case -> .... I'd like to infer as much as possible from x automatically as possible.

Consider the following:

match main ctx f with
| Succeed (Fun in_ty out_ty) => if type_beq in_ty t then Succeed out_ty else Fail
| _ => Fail
end = Succeed ty -> ...

Here, I'd like to intro all of the following at the same time:

Is there a tactic that does this, or an easy way to define a tactic that does this?

view this post on Zulip Gabriel Alfour (Nov 09 2023 at 18:26):

Current way:

      destruct (main ctx arg) ; try (repeat intro ; discriminate) .
      destruct (main ctx f) as [|in_ty] ; try (repeat intro ; discriminate) .
      destruct in_ty as [|in_ty out_ty] ; try (repeat intro ; discriminate) .
      destruct (type_beq in_ty t) ; try (repeat intro ; discriminate) .

view this post on Zulip Paolo Giarrusso (Nov 09 2023 at 21:56):

stdpp's case_match and simplify_eq do a lot of this


Last updated: Jun 13 2024 at 19:02 UTC