fetburner

require "gmp"

def series(l, r)
  if r - l <= 1
    p = (2 * r - 1) * (6 * r - 5) * (6 * r - 1)
    q = r * r * r * 10939058860032000
    a = (r % 2 == 0 ? 1 : -1) * (13591409 + 545140134 * r)

    [p, q, a * p].map { GMP.Z(_1) }
  else

fetburner

require "bigdecimal"

def formula(i, d)
  return [
    (1 - 4 * i) * (2 * i - 1) * (4 * i - 3),
    24893568 * i * i * i * (21460 * i - 20337),
    24893568 * i * i * i,
  ] if d <= 0

  a0, b0, c0 = formula(2 * i - 1, d - 1)

fetburner

Require Import Recdef.
From mathcomp Require Import all_ssreflect zify.

Lemma double_uphalf n : (uphalf n).*2 = odd n + n.
Proof. lia. Qed.

Lemma double_half n : n./2.*2 = n - odd n.
Proof. lia. Qed.

Definition lsb n := nat_of_bool (odd n).

fetburner

Require Import Program.
From mathcomp Require Import all_ssreflect.

Section Segtree.
  Variable A : Type.
  Variable idm : A.
  Hypothesis mul : Monoid.law idm.
  Local Notation "x * y" := (mul x y).

  Variable table : nat -> nat -> A.

fetburner

Require Import Program.
From mathcomp Require Import all_ssreflect.

Lemma eq_bool : forall b1 b2 : bool, b1 <-> b2 -> b1 = b2.
Proof.
  move => [ ] ? [ H12 H21 ]; apply /Logic.eq_sym.
  - exact /H12.
  - by apply /negbTE /negP => /H21.
Qed.

fetburner

From mathcomp Require Import all_ssreflect.

Section Dijkstra.
  Import Order.TTheory.

  Variable V : finType.
  Variable C : orderType tt.

  Variable adj : V -> V -> C -> C.
  Hypothesis adj_increase : forall v u c, (c <= adj v u c)%O.

fetburner

let rec interleave xs ys () =
  match xs () with
  | Seq.Nil -> ys ()
  | Seq.Cons (x, xs) -> Seq.Cons (x, interleave ys xs)

let rec perm_aux n s0 s xs () =
  if n <= 0
  then Seq.return xs ()
  else
    match s () with

fetburner

Require Import ssreflect Nat Arith Lia.

Lemma iter_S A f : forall m x,
  @Nat.iter m A f (f x) = Nat.iter (S m) f x.
Proof. elim => //= ? IH ?. by rewrite IH. Qed.

Lemma iter_plus A f n x : forall m,
  @Nat.iter (m + n) A f x = Nat.iter m f (Nat.iter n f x).
Proof. by elim => //= ? ->. Qed.

fetburner

(* チャーチ数 *)
type church_nat = { nat_fold : 'a. ('a -> 'a) -> 'a -> 'a }
(* チャーチエンコーディングした二進数 *)
type church_bin = { bin_fold : 'a. f0:('a -> 'a) -> f1:('a -> 'a) -> 'a -> 'a }

(* チャーチ数nを受け取って，
   n.nat_fold succ 1
   = m.bin_fold ~f0:(fun x -> 2 * x) ~f1:(fun x -> 2 * x + 1) 1
   が成り立つような二進数mを返す関数church_bin_of_church_natを記述せよ． *)

fetburner

Require Import Classical.
From mathcomp Require Import all_ssreflect.

Section Drinker.
  Variable P : Type.
  Variable p : P.
  Variable D : P -> Prop.

  Theorem drinker : exists (x : P), D x -> forall y, D y.
  Proof.