This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Zagier's one-sentence proof for the two-square theorem in Coq (SSReflect) *) | |
(* - D. Zagier, "A One-Sentence Proof That Every Prime p \equiv 1 (\mod 4) Is a Sum of Two Squares", | |
The American Mathematical Monthly, Vol. 97, No. 2 (Feb., 1990), p. 144 *) | |
Set Implicit Arguments. Unset Strict Implicit. | |
From mathcomp Require Import all_ssreflect. | |
Lemma odd_fixedpoints {X:eqType} (f:X->X) (D:seq X): | |
uniq D -> (forall x, x \in D -> (f x \in D) && (f (f x) == x)) -> | |
odd (size D) <-> odd (count [pred x | f x == x] D). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
concat (matchAll (["akira", "susumu", "tamotsu", "tomo"], ["blue", "green", "red", "white"], [1, 2, 3, 4]) | |
as (list something, multiset something, multiset something) with | |
| ([$x_1, $x_2, $x_3, $x_4], [$y_1, $y_2, $y_3, $y_4], [$z_1, $z_2, $z_3, $z_4]) | |
-> matchAll [(x_1, y_1, z_1), (x_2, y_2, z_2), (x_3, y_3, z_3), (x_4, y_4, z_4)] | |
as set (eq, eq, eq) with | |
| (#"akira", #"blue", !#1) :: | |
(#"susumu", !#"green", !#4) :: | |
(_, #"red", #2) :: | |
(_, #"white", $n) :: | |
(#"tamotsu", _, #(n - 1)) :: _ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data FizzDataType : Type where | |
FizzData : FizzDataType | |
data BuzzDataType : Type where | |
BuzzData : BuzzDataType | |
data FizzBuzzDataType : Type where | |
FizzBuzzData : FizzBuzzDataType | |
data NatDataType : (n : Nat) -> Type where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/python | |
# coding: utf-8 | |
# Print Graham's number | |
# | |
# Just a code for showing definition. | |
# It causes runtime error of maximum recursion. | |
def G(n): | |
# G function of Graham's number | |
if n == 0: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
Tarski's fixed-point theorem on sets (complete lattice) | |
Isabelle 2014 | |
*) | |
theory Tarski imports Main begin | |
lemma fp1: "mono F ==> F (Inter {X. F X <= X}) <= Inter {X. F X <= X}" | |
apply(rule subsetI) | |
apply(rule InterI) | |
apply(simp) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; -*- mode: scheme;-*- | |
; Implementation of resolution principle for first-order logic in Egison | |
(define $unordered-pair | |
(lambda [$m] | |
(matcher | |
{[<pair $ $> [m m] {[[$x $y] {[x y] [y x]}]}] | |
[$ [something] {[$tgt {tgt}]}]}))) | |
(define $positive? |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
bsort=foldr bs [] | |
where bs x []=[x] | |
bs x (y:ys)|x<=y =(x:y:ys) | |
|otherwise =(y:bs x ys) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- http://comonad.com/reader/2018/the-state-comonad/ | |
-- https://www.reddit.com/r/haskell/comments/7oav51/i_made_a_monad_that_i_havent_seen_before_and_i/ | |
{-# language DeriveFunctor #-} | |
import Control.Comonad | |
import Data.Semigroup | |
data Store s a = Store { peek :: s -> a, pos :: s } deriving Functor |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE KindSignatures, | |
TypeSynonymInstances, | |
FlexibleInstances | |
#-} | |
module FixPrime where | |
import Prelude hiding (Functor(..), map, succ, either) | |
pair (f, g) x = (f x, g x) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sig Element{} | |
one sig Group{ | |
elements: set Element, | |
unit: one elements, | |
mult: elements -> elements -> one elements, | |
inv: elements -> one elements | |
} | |
fact NoRedundantElements{ |
NewerOlder