The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am studying Coq.

As far as I understand, the following cannot be done with Coq 8.4:

For example, let L is an instance variable denoting a lattice (in order 
theoretic sense).

Make a database of setoid equalities like:

A L<-> A' (dual L)
A' L <-> A (dual L)
forall A B: (meet L A B = (join (dual L) A B))
forall A B: (join L A B = (meet (dual L) A B))

etc.

(Here A, A' are some properties of lattices.)

Then create a tactic which could replace [A] with [dual A'], [meet X Y] with 
[dual (meet X Y)], in every subexpression.

(This is intended to match the resulting formula with a theorem about the 
lattice L, to finish the proof by duality.)

Here autorewrite could be used, but this would loop with (dual (dual .. A)).

So I see no way to do this effectively.

Am I wrong? Can be this done? Especially I see no way where store this 
database about duality, as auto and autorewrite databases are too specific 
and there seems be no other databases in Coq 8.4.

One more suggestion: Hint databases should be referable not only by ID but 
also by a reference to ID. This would allow for duality tactics e.g. for 
lattice and for categories share the same Ltac code.

Can we expect this in Cor 8.5? Or I again ask for a feature which is already 
implemented but I miss it?

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