The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi, Victor --

An alternative would be to use ltac to implement the rewrites that you want and add an explicit guard to prevent the non-termination. Something like this:

Ltac rewrite_them :=

  match goal with

    | [ |- context [ ?X ?L ] ] =>

      match L with 

        | dual _ => fail 1

        | _ => rewrite ....

      end

   end.

On Tue, Jan 1, 2013 at 4:47 PM, Victor Porton <porton AT narod.ru> wrote:

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

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/