The Coq mailing list

["Devisschere Yann" <devissch AT enseirb.fr>]

I'm trying to prove the completeness of a tactic on a lemma familly, but I'm in front of a problem with autorewrite.

 

Let's suppose I've got a tree type with three sons (left, middle, right) and indexed nodes.

(for example, (A,B,C)i is a tree if A, B and C are trees and i is the index of the root)

Let's suppose I've got a function f allowing tree modifications

Let's suppose now that I've proved 3 lemmas between f and trees :

lemma1 : forall A B C, f (A,B,C)j = (f B,f A,f C)j
lemma2 : forall A B C, f (A,B,C)i = (f A,f C,f B)i
lemma3 : forall A B C, f (A,B,(C,D,E)j)i = (f A,(f D,f C,f E)j,f B)i
(lemma3 can be obtain composing lemma1 and lemma2)

Nethertheless, let's suppose I only add lemma2 and lemma3 to a database (db) I use in tactic for rewriting.

 

In a tacic, at a time, I use "autorewrite with db" on a current goal containing "f (A,B,(C,D,E)j)i"

I cannot (for genericity reasons) specify that I want to use "lemma3" to obtain "(f A,(f D,f C,f E)j,f B)i" (the lemma name may change).

But both lemma2 and lemma3 can be applied and if lemma2 is used, I get "(f A,f (C,D,E)j,f B)i". If that's it, my tactic would fail.

That's why I'd like to know how are applied the rewriting rules.

Is there an order, according to the "hint rewrite ..." or does autorewrite try to use the more specific rewriting rule or the more general ?

 

I don't find explanations of that neither in Coq'art nor in the Coq reference manual. (all the examples use specific excluding rules)

 

Please help me.

Thanks.

 

(Hoping this tiny example is enough clear and representative of my whole problem.)

 

Yann Devisschere