Stream: Coq users

Topic: ✔ Empty context in ltac

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.

Li-yao (Oct 12 2022 at 10:28):

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

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?

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 *)

Julin S (Oct 12 2022 at 13:28):

Got it, thanks.

Notification Bot (Oct 12 2022 at 13:28):

Julin S has marked this topic as resolved.

Last updated: Oct 01 2023 at 19:01 UTC