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: Victor Porton <porton AT narod.ru>
To: Tom Prince <tom.prince AT ualberta.net>,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 19:15:44 +0200
Envelope-from: porton AT yandex.ru

03.01.2013, 18:20, "Tom Prince"
<tom.prince AT ualberta.net>:
> 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.

OK, but we should implement general hints databases for "rewrite", so the
main idea could be implemented in Ltac, not programming in ocaml for every
new situation.

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

[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