Skip to content

Instantly share code, notes, and snippets.

@fetburner
fetburner / gauss.rb
Created June 9, 2024 04:22
ガウス・ルジャンドルのアルゴリズムで円周率を求める
require "gmp"
def pi(n)
prec_bits = Math.log2(10).*(n).ceil
an = GMP.F(1, prec_bits)
bn = GMP.F(2, prec_bits).rec_sqrt
tn = GMP.F(0.25, prec_bits)
(0...Math.log2(n) - 1).each do |n|
an1 = (an + bn) * GMP.F(0.5, 1)
@fetburner
fetburner / chudnovsky.rb
Last active April 5, 2024 09:21
Chudnovskyの公式で円周率を計算するプログラム
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
fetburner / ramanujan.rb
Created March 23, 2024 14:28
ラマヌジャンの公式で円周率を計算するプログラム
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
fetburner / Segtree.v
Last active June 4, 2022 17:16
完全二分木に限らない、セグ木の配列への埋め込み
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
fetburner / Segtree.v
Last active February 19, 2022 20:00
セグメント木を用いた高速な区間積と、セグメント木上の二分探索の検証
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
fetburner / DoublingLca.v
Last active September 2, 2021 14:12
最小共通祖先
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
fetburner / Dijkstra.v
Last active March 1, 2021 07:55
ダイクストラ法の正当性
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
fetburner / perm.ml
Created November 3, 2020 04:57
ストリームの要素からn要素を選ぶ順列のストリーム
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
fetburner / CycleDetection.v
Created May 20, 2020 10:07
フロイドの循環検出アルゴリズム
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.
(* チャーチ数 *)
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を記述せよ. *)