The Coq mailing list

[Valentin ROBERT <valentin.robert.42 AT gmail.com>]

On Mon, Apr 23, 2012 at 15:22, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> 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?

Well, my naive thought was that, since the occurence of an unbound
name x in an Ltac tactic yields the error:
Error: The reference x was not found in the current environment.
then, having x as a parameter of the tactic would somehow bind x to be
what I pass in.

This does not address the problem of "what" are the things I can pass
in however, and what to do with it, since I did not specify what
"tactic argument type" was expected for rs and r.

The code I pasted actually contains lines that I did not expect to
work, I was just trying all sorts of calls to see what went through or
not. In particular, match_args_B and the use of rename are quite
irrelevant here. I present a shorter and cleaner version of the parts
relevant to me at the end of this message. I apologize for the
confusion with all the extra examples in the first snippet.

So I should rephrase my thought into: it seemed to do what I expected
sometimes (that is, work quite like if I had used a tactic notation
with constr(...)), but it also did something I did not expect to
happen (that is, accept match_args_A foo bar where foo and bar don't
exist). Now, I do not understand why I can pass these parameters,
while the behavior does not seem to depend on what I pass in.

I would be interested in knowing why (if) it was stupid of me to write
such a tactic in this fashion in the first place, assuming there is no
way it could work, so that hopefully I can learn not to make the same
mistake again.

Best regards,
- Valentin Robert

(* Beginning code: *)

Ltac match_args_A rs r :=
  match goal with H: rs = r |- _ =>
    idtac
  end.

Theorem test: forall (rs: nat) r, rs = r -> True.
Proof.
  intros.
  match_args_A rs r. (*works, as I expected*)
  match_args_A foo bar. (*works, I did not expect it to*)
  rename r into r0.
(*match_args_A foo bar. does not work, while I expected it to after
the previous attempt*)
  exact I.
Qed.

>> 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.
>>
>
>