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 / coq_if.v
Created January 21, 2015 03:18
Definition isO (n: nat) :=
if n then True else False.
Definition isNil {A: Type}(l: list A) :=
if l then True else False.
Goal isO 0.
simpl; auto.
Qed.
@mathink
mathink / cateogry_module.v
Created January 8, 2015 14:55
Module を使ってわかりやすく圏とかの構成が出来ないものか。
Require Import Coq.Setoids.Setoid Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Set Reversible Pattern Implicit.
Generalizable All Variables.
Delimit Scope cat_scope with cat.
Open Scope cat_scope.
@mathink
mathink / group_advent_2014.v
Created December 20, 2014 13:31
Theorem Prover Advent Calendar day 20.
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
@mathink
mathink / map_advent_2014.v
Last active August 29, 2015 14:11
Theorem Prover Advent Calendar day 15.
Set Implicit Arguments.
Unset Strict Implicit.
Require Import setoid_advent_2014.
Structure Map (X Y: Setoid) :=
{
map_body:> X -> Y;
@mathink
mathink / setoid_advent_2014.v
Last active August 29, 2015 14:11
Theorem Prover Advent Calendar day 10.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Basics Tactics Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
equal: relation carrier;
@mathink
mathink / code_monad.v
Last active August 29, 2015 14:08
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require ssreflect.
Import ssreflect.SsrSyntax.
Module ForSyntax.
Class Functor (T: Type -> Type): Type :=
@mathink
mathink / YonedaLemma.v
Created September 7, 2014 04:46
(* -*- mode: coq -*- *)
(* Time-stamp: <2014/9/7 13:46:31> *)
(*
Scratch.v
- mathink : Author
*)
(** * Category Theory 'on' Coq
米田の補題を目標にして進めていきます。
@mathink
mathink / YonedaLemma.v
Created September 6, 2014 13:44
(* -*- mode: coq -*- *)
(* Time-stamp: <2014/9/6 22:44:0> *)
(*
Scratch.v
- mathink : Author
*)
(** * Category Theory 'on' Coq *)
@mathink
mathink / Scratch.v
Last active August 29, 2015 14:06
(* -*- mode: coq -*- *)
(* Time-stamp: <2014/9/6 1:2:55> *)
(*
Scratch.v
- mathink : Author
*)
(** * Category Theory 'on' Coq *)
Set Implicit Arguments.
@mathink
mathink / bst_base.v
Created August 21, 2014 16:34
Require Import ssreflect eqtype ssrbool ssrfun ssrnat seq.
Require Import Adlibssr.btree Adlibssr.binsearch Adlibssr.order.
(* leq is total-order on nat *)
Program Canonical Structure leq: totalOrder nat := makeTotalOrder leq.
Next Obligation.
apply anti_leq.
Qed.