The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/23/2012 09:09 AM, Valentin Robert wrote:
> The following snippet exposes some behaviors of Ltac's binding/matching that I
> fail to understand (or to find details about in the manual). I wonder whether
> it is a bug, a known problem, or possibly an expected behavior.
> My goal is to pass two arguments to the tactic to guide it towards which
> hypotheses it should use. Using Ltac, things do not work quite as I expect 
> them
> to.
>    

Can you explain how the behavior is different from what you expect?

> Using:
> Tactic Notation "my_tactic" constr(rs) constr(r)
> seems to solve this particular issue, but can I make such a tactic notation
> recursive?
> Or can I use constr(...) somehow in Ltac?
> Or do I need to mix Ltac and Tactic Notation to get the best of both worlds?
>
> Any advice on dealing with such issues would be greatly appreciated.
>
> - Valentin Robert
>
> (* Beginning Coq snippet.
> I have not tested it on trunk, the results shown here are for Coq 8.3pl4.
> *)
>
> Ltac match_args_A rs r :=
>    match goal with H: rs = r |- _ =>
>      let H' := fresh "H" in rename H into H'
>    end.
>
> Ltac match_args_B rs r :=
>    match goal with H: rs = r |- _ =>
>      let r' := fresh "r" in rename r into r'
>    end.
>
> Theorem test_0: 0 = 1 ->  True.
> Proof.
>    intros.
>    match_args_A 0 1. (*works*)
> (*match_args_B 0 1. No matching clauses for match goal*)
> (*match_args_A 1 2. No matching clauses for match goal*)
> (*match_args_B 1 2. No matching clauses for match goal*)
> (*match_args_A foo bar. No matching clauses for match goal*)
> (*match_args_B foo bar. No matching clauses for match goal*)
>    exact I.
> Qed.
>
> Theorem test_1: forall (rs: nat) r, rs = r ->  True.
> Proof.
>    intros.
> (*match_args_A 0 1. No matching clauses for match goal*)
> (*match_args_B 0 1. No matching clauses for match goal*)
> (*match_args_A 1 2. No matching clauses for match goal*)
> (*match_args_B 1 2. No matching clauses for match goal*)
>    match_args_A rs r. (*works*)
>    match_args_B rs r. (*works*)
> (*match_args_A foo bar. No matching clauses for match goal*)
>    rename r0 into r.
>    match_args_A foo bar. (*works!*)
> (*match_args_B foo bar. No matching clauses for match goal*)
>    exact I.
> Qed.
>