Stream: Coq users

Topic: ✔ Ltac to unfold a function after a predicate

Daniel Hilst Selli (May 12 2022 at 19:12):

I have some code like this

Lemma foo : P (f ...).

Where f varies, I'm looking for a ltac way of unfolding f, I tried match goal but it doesn't work as I expect

Parameter Foo : forall {a : Set}, a -> Prop.
Definition f {A : Set} (x : A) := x.
Lemma foo  {A : Set} (x : A) : Foo (f x).
Proof.
  match goal with
  | |- Foo (?g _) => unfold g
  end.

In my case f will have arbitrary number of arguments, I don't want to match to the number of the arguments, I want to match to an application of a function to any number of arguments greater or equal to 1. Something like g _ g _ _ g _ _ _ ...

Guillaume Melquiond (May 12 2022 at 19:21):

Ltac head f :=
  match f with
  | ?g _ => head g
  | _ => f
  end.

Lemma foo  {A : Set} (x : A) : Foo (f x).
Proof.
match goal with
| |- Foo ?g => let g := head g in unfold g
end.

Daniel Hilst Selli (May 12 2022 at 19:30):

Thank you Guillaume I'm adapting to my real-world case :)

Notification Bot (May 12 2022 at 19:48):

Daniel Hilst Selli has marked this topic as resolved.

Daniel Hilst Selli (May 13 2022 at 16:57):

I just realize that I could have used Hint Unfold f : foo_db and then autounfold with foo_db :face_palm:

Last updated: Oct 03 2023 at 02:34 UTC