The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

The tactic you're looking for is either of these:

repeat

match goal with

| x : _ |- _ => progress unfold x

end.

repeat

match goal with

| x := _ : A |- _ => progress unfold x

end.

The match-with tactic only moves from one hypothesis to the next if a tactic fails. Examples:

Goal True -> let n1 := 0 in let n2 := 0 in True -> n1 = n2.

intros H1 ? ? H2.

match goal with

| x : _ |- _ => idtac x

end.

try

match goal with

| x : _ |- _ => progress idtac x

end.

unfold doesn't fail if there's nothing to unfold. progress t fails if t fails or if t succeeds but without making progress. try t always succeeds.

On Wed, Oct 2, 2013 at 7:48 PM, Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com> wrote:

I have just tried with

repeat match goal with

  [H := _  : A |- _] =>

    unfold H

end

but doesn't work either.

2013/10/2 Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>

Hi Coq Club,

Suppose you have some goal like this

H0 : P

H1 : Q

t1 := first_term : A

t2 := second_term : A

t3 := third_term : A

t4 := fourth_term t3 : A
==============

my_type t1 t2 = t4

I want to clean every [t_i] and replace the conclusion
with

my_type (first_term) (second_term) = fourth_term third_term

I'm trying to avoid doing:

unfold t1

unfold t2

unfold t3 in *

unfold t4

I don't know too much Ltac, but I tried to do

repeat match goal with

  [H : _ |- _] =>

    try unfold H

end

and it seems not to match with local variables.

Thank you!