The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, I guess there is a way to trick autorewrite into doing what you wish. The idea is to give it something to consume to force termination.

Definition marked (L:Lattice) : Lattice := L.

Then you define all your autorewrite hint like:

forall (L:Lattice) (a b:L), meet (marked L) a b = join (dual L) a b

You can then make a tactic dualize (let's say we're only concerned in the conclusion of the goal, for now)

Ltac mark A := change A with (marked A).

Ltac dualize A := mark A; autorewrite with dualize.

On 3 January 2013 18:15, Victor Porton <porton AT narod.ru> wrote:

03.01.2013, 18:20, "Tom Prince" <tom.prince AT ualberta.net>:

> Victor Porton <porton AT narod.ru> writes:
>
>>  So I see no way to do this effectively.
>
> This would be fairly straightforward to implement as an ocaml plugin.

OK, but we should implement general hints databases for "rewrite", so the main idea could be implemented in Ltac, not programming in ocaml for every new situation.

--
Victor Porton - http://portonvictor.org