Skip to content

Instantly share code, notes, and snippets.

View yoshihiro503's full-sized avatar

YOSHIHIRO Imai yoshihiro503

92 followers · 44 following
View GitHub Profile
@yoshihiro503
yoshihiro503 / contrapositive_bool.v
Created September 25, 2022 11:55
Theorem contrapositive_bool : forall (p q : bool),
(p = true -> q = true) -> (q = false -> p = false).
Proof.
intros p q H Hq.
destruct p. (* pで場合分け*)
- (* pがtrueのとき *)
rewrite H in Hq.
+ discriminate Hq.
+ reflexivity.
- (* pがfalseのとき*)
@yoshihiro503
yoshihiro503 / placticing_mathcomp.v
Last active September 20, 2022 00:30
From mathcomp Require Import all_ssreflect.
Lemma rensyu : forall i x y,
i != 0 -> (x - y) = 0 -> x.+1 - y <= i.
Proof.
move=> i x y i0 /eqP xy.
rewrite -addn1.
rewrite leq_subLR.
apply: leq_add.
by [].
@yoshihiro503
yoshihiro503 / verify_plebeia_merkle_proof.ml
Last active July 1, 2022 10:18
open SCaml
let empty_bytes = Bytes "0x"
let is_empty_bytes b = (Bytes.length b = Nat 0)
let bytes_concat sep ss =
match ss with
| [] -> empty_bytes
| s0 :: ss ->
List.fold_left' (fun (acc, s) -> Bytes.concat (Bytes.concat acc sep) s) s0 ss
@yoshihiro503
yoshihiro503 / TheEvolutionOfACoqProgrammer.v
Last active June 21, 2022 09:10
(** * Draft: The evolution of a Coq programmer *)
(** ** Freshman Coq programmer *)
Fixpoint fac n :=
match n with
| O => 1
| S p => n * fac p
end.
(* begin hide *) Reset fac. (* end hide *)
@yoshihiro503
yoshihiro503 / 国民年金法第三十七条遺族基礎年金の支給要件.v
Last active June 9, 2022 12:35
Require Import Nat.
Inductive Person :=
| CPerson : nat -> option Person -> Person.
Definition 年齢 p :=
let 'CPerson 年齢 配偶者 := p in 年齢.
Definition 配偶者 p :=
let 'CPerson 年齢 配偶者 := p in 配偶者.
@yoshihiro503
yoshihiro503 / tezosにMR送る前にやることたち.md
Last active April 1, 2022 10:32

formatting

フォーマットに準拠しているか検査

dune build @fmt

強制的にフォーマット

dune build @fmt --auto-promote
@yoshihiro503
yoshihiro503 / hoge.c
Created December 17, 2021 05:41
int hoge(x) {
int y = x + 1;
return y;
}
@yoshihiro503
yoshihiro503 / replay_1600000-1610000.log
Last active August 19, 2021 00:29
This file has been truncated, but you can view the full file.
Aug 18 15:38:43.133 - external_block_validator: initialized
Aug 18 15:38:43.260 - external_block_validator: block validator process started with pid 3093
Aug 18 15:38:44.027 - external_block_validator: shutting down
Aug 18 15:38:44.035 - external_block_validator: process terminated normally
Aug 18 15:40:14.584 - external_block_validator: initialized
Aug 18 15:40:14.713 - external_block_validator: block validator process started with pid 3726
Aug 18 15:40:14.722 - external_block_validator: shutting down
Aug 18 15:40:14.726 - external_block_validator: process terminated normally
Aug 18 15:53:56.974 - external_block_validator: initialized
Aug 18 15:53:57.102 - external_block_validator: block validator process started with pid 5518
@yoshihiro503
yoshihiro503 / List_map_length.v
Created April 21, 2021 10:35
list mapがリストの長さを変えないことを証明する例です
Require Import List.
Import ListNotations.
Fixpoint list_map {A B:Type} (f : A -> B) (xs : list A) :=
match xs with
| [] => []
| x :: xs => f x :: list_map f xs
end.
Theorem list_map_length : forall (A B: Type) (f: A -> B) xs,
@yoshihiro503
yoshihiro503 / Teztを使ってみる.md
Last active August 3, 2020 10:12

概要

ブロックチェーン Tezos において、ノードの立ち上げやクライアントを使ったインタラクションをOCaml上で実行できるフレームワーク Tezt が爆誕したので試してみる。

Tezt とはなに？

Tezos開発者がOCamlでTezosの tezos プロジェクトに内包される形で提供されようとして現在 Merge Request が出ている段階である。