coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] 2048

From: Laurent Théry <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] 2048
Date: Sun, 30 Mar 2014 17:01:47 +0200

On 03/30/2014 04:51 PM, Pierre-Yves Strub wrote:

With an oracle, thm1 is ok. For thm2...

Really cool!! Is it the shortest solution? Also it be good if we could find some regularity in the witness so to have a nice compressed form.

For thm2, I am also interested in the alternative form:

Lemma thm3 : exists seed, forall ms, ~ g2048 seed ms.

;-)

--
Laurent

[Coq-Club] 2048, Laurent Théry, 03/30/2014
- Re: [Coq-Club] 2048, Kevin Sullivan, 03/30/2014
- Re: [Coq-Club] 2048, Matthieu Sozeau, 03/30/2014
- Re: [Coq-Club] 2048, AUGER Cédric, 03/30/2014
  - Re: [Coq-Club] 2048, Pierre-Yves Strub, 03/30/2014
    - Re: [Coq-Club] 2048, Laurent Théry, 03/30/2014
  - Re: [Coq-Club] 2048, Laurent Théry, 03/30/2014
    - Re: [Coq-Club] 2048, Gabriel Scherer, 03/30/2014