Skip to content

Instantly share code, notes, and snippets.

View pi8027's full-sized avatar

Kazuhiko Sakaguchi pi8027

161 followers · 13 following
View GitHub Profile
@pi8027
pi8027 / rosetree.v
Last active September 5, 2022 19:10
From mathcomp Require Import all_ssreflect.
Inductive tree := branch : seq tree -> tree.
Fixpoint size (t : tree) :=
let: branch ts := t in
(fix size_rec ts :=
if ts is t :: ts then
size t + size_rec ts
else 1) ts.
@pi8027
pi8027 / perf.data
Last active January 24, 2022 16:22
Perf and Memtrace data of `Lemma from_sander`
This file has been truncated, but you can view the full file.
View raw
@pi8027
pi8027 / trace.ctf
Last active January 24, 2022 16:22
Memtrace of Apery
This file has been truncated, but you can view the full file.
View raw
@pi8027
pi8027 / meta.v
Created March 6, 2021 23:06
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype path tuple finfun bigop finset order.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section EqSeq.
Variables (T : eqType).
@pi8027
pi8027 / catIl.v
Last active June 21, 2020 20:39
Require Import all_ssreflect.
Section cat.
Variable (A : Type).
Lemma catIr : right_injective (@cat A).
Proof. by elim => //= ? ? IH ? ? [] /IH. Qed.
Lemma catIl : left_injective (@cat A).
Proof.
@pi8027
pi8027 / demo.v
Last active September 25, 2019 03:26
Validating Mathematical Structures (Coq Workshop 2019)
Section from_ssrfun.
Local Set Implicit Arguments.
Local Unset Strict Implicit.
Local Unset Printing Implicit Defensive.
Variables S T R : Type.
Definition left_inverse e inv (op : S -> T -> R) := forall x, op (inv x) x = e.
@pi8027
pi8027 / minimal_hitting_sets.v
Last active June 5, 2018 12:03 — forked from msakai/minimal_hitting_sets.v
Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# ＼ (f∪g)#'.
From mathcomp Require Import ssreflect fintype finset seq ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(******************************************************************************
Coq/SSReflect formalization of the proof of 'f# ↘ (f∪g)# = f# ＼ (f∪g)#'.
Checked with Coq 8.8.0 and MathComp 1.7.0.
@pi8027
pi8027 / autoperm.v
Last active February 27, 2018 09:17
Require Import all_ssreflect all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Perm.
Variable (A : eqType) (le : A -> A -> bool).
@pi8027
pi8027 / vec.v
Created December 12, 2017 09:06
Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Fixpoint vec (n : nat) (A : Type) : Type :=
if n is n'.+1 then A * vec n' A else unit.
Fixpoint vcat (n m : nat) (A : Type) : vec n A -> vec m A -> vec (n + m) A :=
@pi8027
pi8027 / gist:01fc48c13f2ed893e326439bd9a266b1
Last active February 4, 2022 04:29
Hilbert-Post Completeness of BoolState
以下は Lecture 1: Algebraic Effects I （Gordon Plotkin） - Exercise 5 の解である。
http://cs.ioc.ee/ewscs/2015/plotkin/plotkin-slides-exercises1.pdf
p. 31 の等式理論 BoolState より、いかなる式に対しても
read(write_b1(x), write_b2(y)) (x, yは変数)
という形の normal form が自然に与えられる。
以下のように、2つの異なる normal form に関する等式を仮定する:
read(write_b1(x), write_b2(y)) ＝ read(write_b1'(x'), write_b2'(y')) (b1 ≠ b1' ∨ x ≠ x' ∨ b2 ≠ b2' ∨ y ≠ y')