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.                  

fetburner

import Data.Bits
import Control.Parallel

cutoff = 1000000

rsqrt2 :: Int -> Int -> Integer
rsqrt2 d n = iter 32 $ (floor $ approx * 2 ** 64) `shiftL` (d - 64)
  where
    approx = 1.0 / sqrt (fromIntegral n :: Double)
    mult x y = (x * y) `shiftR` d

fetburner

Require Import Relations.
From mathcomp Require Import all_ssreflect.
From Autosubst Require Import Autosubst.

Hint Constructors clos_refl_trans.

Section ARS.
  Variable A : Type.
  Variable R : A -> A -> Prop.

fetburner

From mathcomp Require Import ssreflect ssrbool ssrnat seq eqtype.

Inductive type :=
  | Int
  | Bool
  | Arrow of type & type.

Inductive sub : type -> type -> Set :=
  | sub_int : sub Int Int
  | sub_bool : sub Bool Bool

fetburner

import java.util.function.Function;
import java.util.function.IntFunction;
import java.util.function.BinaryOperator;

/* セグ木 */
interface SegTree<T, S extends BinaryOperator<T>>
{
	/* 要素数 */
	int size();
	/* 

fetburner

let rec divisors (acc, acc') i n =
  match compare n (i * i) with
  | -1 -> List.rev_append acc acc'
  | 0  -> List.rev_append acc (i :: acc')
  | 1  -> divisors (if 0 < n mod i then (acc, acc') else (i :: acc, n / i :: acc')) (i + 1) n
let divisors = divisors ([], []) 1

let true = 
  Array.fold_left ( && ) true @@ Array.init 10000 @@ fun n ->
    ( = ) (divisors n) @@

fetburner

module WeightedDirectedGraph
  (Vertex : sig
    type t
    val compare : t -> t -> int
  end)
  (Weight : sig
    type t
    val zero : t
    val ( + ) : t -> t -> t
    val compare : t -> t -> int

fetburner

let radix_sort : int list -> int list = fun ns ->
  let ns =
    Array.fold_left (fun ns i ->
      let l, r = List.partition (fun n -> n land (1 lsl i) = 0) ns in
      l @ r) ns @@ Array.init 62 @@ fun i -> i in
  let l, r = List.partition (fun n -> n land (1 lsl 62) = 0) ns in
  r @ l;;

Random.self_init ();;
let true =

fetburner

From mathcomp Require Import all_ssreflect.

Notation var := nat.
Notation pos := nat.

Inductive term :=
  | Var of var & pos
  | App of term & term
  | Lam of term
  | Let of seq term & term.

fetburner

let rec floor_sqrt acc acc_x_2_x_r sq_acc_minus_z r sq_r =
  if r = 0 then acc
  else
    let sq_acc_minus_z' = sq_acc_minus_z + acc_x_2_x_r + sq_r in
    ( if sq_acc_minus_z' <= 0 then
        floor_sqrt (acc + r) ((acc_x_2_x_r lsr 1) + sq_r) sq_acc_minus_z'
      else
        floor_sqrt acc (acc_x_2_x_r lsr 1) sq_acc_minus_z ) (r lsr 1) (sq_r lsr 2)
let floor_sqrt z = floor_sqrt 0 0 (~-z) (1 lsl 30) (1 lsl 60)