Stream: Coq users

Topic: ✔ Creating new hypothesis using Ltac

Jerome Hugues (Mar 07 2023 at 21:52):

Hi,

I am trying to create new hypothesis using Ltac. I have the following MWE to illustrate my case

Set Default Timeout 1. (* recommended *)

Ltac plip' :=
  let H := fresh "H" in
    assert True as H ; [apply I|].

Ltac plop :=
  repeat match goal with
  | [  |- False ] => plip'
  end.

Ltac plop' :=
  repeat match goal with
  | [ H: True |- _ ] => plip'
  end.

Goal False.
  plip'. (* creates new hypothesis *)
  Fail plop. (* time out *)
  Fail plop'. (* time out *)
Abort.

Here, plip' always create a new hypothesis. But plop timeouts. I was expecting to use a match to create the new hypothesis from either current goal or current set of hypothesis.

Any idea what is causing this? I am using Coq 8.16.
Is there a recommended practice to achieve something similar, i.e., create new hypothesis from a given context?
I have a longer code snippet that would benefit from such pattern.

Thanks,

Jerome Hugues (Mar 07 2023 at 22:00):

Of course, it is always when you click that you realize that this "repeat" might create a fork bomb ...
Is it safe to assume that repeat rescans the list of goals every time a match occurs?

Laurent Théry (Mar 07 2023 at 22:22):

Yes, you can replace repeat by do n to see what is happening.

Ltac plop :=
  do 3 match goal with
  | [  |- False ] => plip'
  end.

Ltac plop' :=
  do 3  match goal with
  | [ H: True |- _ ] => plip'
  end.

Notification Bot (Mar 08 2023 at 03:43):

Jerome Hugues has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC