Stream: Coq users

Topic: ✔ Empty context in ltac


view this post on Zulip Julin S (Oct 12 2022 at 10:25):

How can we denote empty context in ltac1 while writing patterns for match?

I wanted my tactic to apply simpl when there are no hypotheses in the context.

How can that be done?

Doing [ |- _] => auto seems to match for any number of hypotheses. How can we restrict it to zero number of hypotheses?

Ltac foo :=
  match goal with
  | [ |- _ ] => simpl
  end.

view this post on Zulip Li-yao (Oct 12 2022 at 10:28):

Maybe have a branch that matches on a hypothesis and fails?

view this post on Zulip Julin S (Oct 12 2022 at 10:32):

So have a branch like _ |- _ , check if it fails and then do simpl?

If that's so, how can we check failure on branch match? It will just go to the next branch, right?

view this post on Zulip Gaëtan Gilbert (Oct 12 2022 at 11:05):

Goal True -> 1 + 1 = 2.
Proof.
  intros H.
  match goal with
  | _ : _ |- _ => idtac
  | _ => simpl
  end.
  (* goal: H : True |- 1 + 1 = 2 *)

  clear H.
  match goal with
  | _ : _ |- _ => idtac
  | _ => simpl
  end.
  (* goal: |- 2 = 2 *)

view this post on Zulip Julin S (Oct 12 2022 at 13:28):

Got it, thanks.

view this post on Zulip Notification Bot (Oct 12 2022 at 13:28):

Julin S has marked this topic as resolved.


Last updated: Jun 15 2024 at 08:01 UTC