Skip to content

Instantly share code, notes, and snippets.

View mathink's full-sized avatar

m mathink

11 followers · 1 following
View GitHub Profile
@mathink
mathink / gist:6901121
Created October 9, 2013 13:17
Ssreflect で tree を定義してみました． eqType の構成までやってます． seq を大いに参考にしております． http://ssr2.msr-inria.inria.fr/doc/ssreflect-1.4/Ssreflect.seq.html 使おうと思ったら，使う必要なかった．
(* Tree on Ssreflect *)
Require Import
Ssreflect.ssreflect
Ssreflect.ssrfun
Ssreflect.ssrbool
Ssreflect.eqtype
Ssreflect.ssrnat
Ssreflect.seq.
@mathink
mathink / dominator.v
Created October 26, 2013 06:50
(* Directed finite graph *)
Require Import
Ssreflect.ssreflect Ssreflect.ssrbool
Ssreflect.ssrfun Ssreflect.eqtype
Ssreflect.ssrnat Ssreflect.seq
Ssreflect.path Ssreflect.fintype
Ssreflect.fingraph.
Set Implicit Arguments.
@mathink
mathink / to1or145.hs
Last active December 27, 2015 05:29
digits :: (Integral a) => a -> [a]
digits n | n == 0 = []
| n < 10 = [n]
| otherwise = n `mod` 10:digits (n `div` 10)
sqrSum :: (Integral a) => [a] -> a
sqrSum = foldr (\x -> (x^2 +)) 0
compress :: (Integral a) => a -> a
compress = sqrSum.digits
@mathink
mathink / fin.v
Created December 3, 2013 11:43
Require Import
Ssreflect.ssreflect
Ssreflect.eqtype
Ssreflect.ssrbool
Ssreflect.fintype
Ssreflect.seq.
Goal
(forall (T : finType) (xs : seq T),
#|xs| = #|T| -> forall x, x \in xs).
@mathink
mathink / wf_fold.v
Last active August 29, 2015 14:01
Require Import Wellfounded.
Require Import List.
(** * Structural Recursive foldr & Well-founded Recursive foldr *)
Section FoldR.
Context {A B: Set}(op: A -> B -> B)(e: B).
(** ** normal foldr *)
Fixpoint foldr (l: list A) :=
@mathink
mathink / wf_fold.v
Created May 7, 2014 12:53
Require Import Wellfounded.
Require Import List.
(** * Structural Recursive fold & Well-founded Recursive fold
** foldr
*)
Section FoldR.
Context {A B: Set}(op: A -> B -> B)(e: B).
@mathink
mathink / wf_fold.v
Last active August 29, 2015 14:01
Require Import Wellfounded.
Require Import List.
(** * Structural Recursive fold & Well-founded Recursive fold
** foldr
*)
Section FoldR.
Context {A B: Set}(op: A -> B -> B)(e: B).
@mathink
mathink / leq.v
Created May 14, 2014 15:22
Inductive leq (n: nat): nat -> Set :=
| leq_n : leq n n
| leq_S (m: nat): n <= m -> leq n m -> leq n (S m).
Lemma leq_n_unique:
forall (n: nat)(H: leq n n),
H = leq_n n.
Proof.
intros n H.
destruct H. (* fail... *)
@mathink
mathink / Anomaly.v
Last active August 29, 2015 14:01
Module Type Ma.
Parameter R : Type.
End Ma.
Module Type Mb (A : Ma).
Include A.
Definition tmp := R.
Back.
Back.
Back.
@mathink
mathink / もなど.v
Last active August 29, 2015 14:01
(* モナドを作ってみましょう *)
Set Implicit Arguments.
Unset Strict Implicit.
Notation 型全体 := Type.
Notation 命題 := Prop.
Notation "T '上の変換'" := (T -> T) (at level 55, left associativity).
Notation "X 'から' Y 'への関数'" := (X -> Y) (at level 60, right associativity).