The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 2019-11-13 12:14, Dan Christensen wrote:
> That's a nice way to avoid having to know the number of arguments that
> the lemma takes.  There are still two other places where I need to list
> the arguments, which I've pulled out into another helper function.
> 
> Ltac find_function fn term :=
>   match term with
>     | context[fn ?a1 ?a2 ?a3] => constr:(fn a1 a2 a3)
>     | context[fn ?a1 ?a2    ] => constr:(fn a1 a2)
>     | context[fn ?a1        ] => constr:(fn a1)
>     | context[fn            ] => constr:(fn)
>   end.

Use a tacitc to get the head of the term, then match that against fn, I think.

> Any ideas?

Not really.  You could special-case this situation.

> 2) I want to work with one side of the equation at a time, but
> the "set f as fn" applies to the whole goal.  Is there a way to
> do that substitution just in the lhs?  Not only would it be more
> efficient, it would avoid changing the rhs:
> 
> Goal forall m n, (4 * (m + (3 * n)) * 2) = m + n.
>   intros.
>   rewrite_in_lhs Nat.add_comm.
>   (* RHS changes to (fun n0 m0 : nat => n0 + m0) m n  *)
> Abort.

Use etransitivity before the rewrite?