The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 30 Mar 2014 01:14:35 +0100,
Laurent Théry 
<Laurent.Thery AT inria.fr>
 a écrit :

For a small increase in performances, it would have been better to
remember only the exponent, instead of the whole natural number (unary
integers are not very good wrt Coq memory when they can become quite
big).

I "patched" it by stripping "strip" and replace cumul with:

(* Cumulative action on a line *)
Fixpoint cumul (n : nat) (l m : list nat) : list nat :=
  match l with
  | nil => if n then m else (n::m)
  | hd :: tl => if hd
                then cumul n tl (O :: m)
                else if beq_nat n hd
                     then (S hd) :: (cumul O tl (O :: m))
                     else if n
                          then cumul hd tl m
                          else n :: (cumul hd tl m)
  end.

(* Cumulative action + strip on lines *)
Definition icumul (n : nat) := map (fun l => cumul O l nil).

Then of course, (2::4::nil) must be replaced with (1::2::nil), and 2048
with 11.

Furthermore, running "strip" at each iteration of "cumul" is needless,
as you can simply call it once before running cumul for the same result.

> Hi,
> 
> if you are addicted to the new "productivity killer" app 2048 :
> 
> http://gabrielecirulli.github.io/2048/
> 
> you can now turn it into a proving activity with Coq :
> 
> http://www-sop.inria.fr/marelle/Laurent.Thery/T2048.v
> 
> Have fun!
> 
> --
> Laurent
> 
> Ps: if you manage to prove thm1 or thm2 please send me an email ;-)