coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?

From: Tom Prince <tom.prince AT ualberta.net>
To: Victor Porton <porton AT narod.ru>, coq-club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?
Date: Thu, 03 Jan 2013 09:20:03 -0700

Victor Porton
<porton AT narod.ru>
writes:
> So I see no way to do this effectively.

This would be fairly straightforward to implement as an ocaml plugin.

Tom

[Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Victor Porton, 01/01/2013
- Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Daniel Schepler, 01/01/2013
- Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Gregory Malecha, 01/02/2013
  - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Victor Porton, 01/02/2013
    - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Gabriel Scherer, 01/02/2013
      - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Victor Porton, 01/02/2013
    - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Gregory Malecha, 01/02/2013
      - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Victor Porton, 01/02/2013
- Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Tom Prince, 01/03/2013
  - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Victor Porton, 01/03/2013
    - Re: [Coq-Club] Implementing proof by duality. Is it possible at all in Coq?, Arnaud Spiwack, 01/04/2013