The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Could you instead prove your result parametrized by the lattice, and
then instantiate them both for the original lattice and its dual? This
way, no need to use sophisticated automations to change proofs.

On Wed, Jan 2, 2013 at 8: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