The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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?

My guess would be that the typeclasses mechanism should be able to
handle this.  What I'm thinking of might go something like this
(although I haven't tested it in detail):

Class Le (X:Type) : Type :=
| le : X -> X -> Prop.
Class Wedge (X:Type) : Type :=
| wedge : X -> X -> X.
...

Inductive dual (X:Type) : Type :=
| dual_element : X -> dual X.
Instance DualLe {X} `{Le X} : Le (dual X) :=
  fun x y : dual X =>
  match x, y with
  | dual_element x0, dual_element y0 => le y0 x0
  end.
Instance DualWedge {X} `{Vee X} : Wedge (dual X) :=
  fun x y : dual X =>
  match x, y with
  | dual_element x0, dual_element y0 => dual_element (vee x0 y0)
  end.
...

Class Duality (P Q:Prop) : Prop :=
| duality : P <-> Q.
Class DualTerm {X:Type} (x:X) (y:dual X) : Prop :=
| dual_term_eq : dual_element x = y.

Instance DualTermBase {X:Type} (x:X) :
  DualTerm x (dual_element x) | 5 :=
eq_refl.
Instance WedgeDualVee {X:Type} `{Wedge X}
  (x y:X) (x' y':dual X) `{DualTerm x x') `{DualTerm y y'} :
  DualTerm (wedge x y) (vee x' y').
Proof. ... Qed.
...

Instance LeDuality {X:Type} (x y:X)
  (x' y':dual X) `{DualTerm x x'} `{DualTerm y y'} :
  Duality (le x y) (le y' x').
Proof. ... Qed.

Example sample_duality {X} `{Lattice X} :
  forall x y:X, le (wedge x y) x.
Proof.
intros.
rewrite duality.  (* should hopefully rewrite to
  le (dual_element x) (vee (dual_element x) (dual_element y)). *)
...
Qed.
-- 
Daniel Schepler