The Coq mailing list

[Victor Porton <porton AT narod.ru>]

02.01.2013, 11:24, "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.

I think, this is not what I want, because L may be an ARBITRARY lattice, not 
an instantiation.

> 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

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