The Coq mailing list

[Victor Porton <porton AT narod.ru>]

02.01.2013, 17:52, "Gregory Malecha" <gmalecha AT eecs.harvard.edu>:

I'm not sure what you mean by "store the database for dualities of a lattice." The above Ltac doesn't use any hint databases.

 

Certainly, I realize that it does not use any hint databases.

 

The thing which I want is to introduce a new kind of hint databases, to be compatible with the below style of coding (that is compatible with [rewrite]).

 

This feature seems missing in Coq 8.4.

 

On Wed, Jan 2, 2013 at 2:54 AM, Victor Porton <porton AT narod.ru> wrote:

02.01.2013, 02:26, "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.

 

The trouble is not rewriting itself (which as you've shown above is possible in Coq), but no mean to store the database for dualities of a lattice.

 

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/

 

 

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

 

--
gregory malecha

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

 

 

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