Skip to content

Instantly share code, notes, and snippets.

View yoshihiro503's full-sized avatar

YOSHIHIRO Imai yoshihiro503

94 followers · 45 following
View GitHub Profile
@yoshihiro503
yoshihiro503 / file0.txt
Created June 12, 2013 06:14
OMakeで「OCaml.om: line 563,」と言われたときの対処法 ref: http://qiita.com/items/5aec4ee72344ef3c6480
File /usr/lib/omake/build/OCaml.om: line 563,
failed on target: hoge.cmi
@yoshihiro503
yoshihiro503 / ImplicitClosureTest.scala
Created July 26, 2013 01:21
無名関数の引数にimplicitがついた時の挙動
package controllers
import play.api.mvc._
object ImplicitClosureTest extends Controller {
def foo(implicit f:Flash) = f.toString
def hoge = Action {
implicit request => Ok(foo)
@yoshihiro503
yoshihiro503 / s_execute.v
Last active December 20, 2015 07:29
ソフトウェアの基礎 Imp_J.vの練習問題 stack_compiler
(*
スタック言語のプログラムを評価する関数
*)
Fixpoint s_execute (st : state) (stack : list nat)
(prog : list sinstr)
: list nat :=
match (prog, stack) with
| (nil, _) => stack
| (SPush n :: prog', _) => s_execute st (n::stack) prog'
@yoshihiro503
yoshihiro503 / Equiv_J.v
Created October 26, 2013 12:41
第33回 #ProofCafe での練習問題のssreflectを使った解答例。 ref: http://qiita.com/yoshihiro503/items/0bca75e5ab52e40f01f6
Require Import ssreflect.
(* **** Exercise: 3 stars (swap_if_branches) *)
(** **** 練習問題: ★★★ (swap_if_branches) *)
Theorem swap_if_branches: forall b e1 e2,
cequiv
(IFB b THEN e1 ELSE e2 FI)
(IFB BNot b THEN e2 ELSE e1 FI).
Proof.
move => b e1 e2.
split => H.
@yoshihiro503
yoshihiro503 / Sample.scala
Created December 25, 2013 06:59
Scala 2.10.0 で型変数の実行時判定ができなくなる警告が出ないことがあるかも ref: http://qiita.com/yoshihiro503/items/2e73c4d9d6acb8a3c6b0
type LS = List[String]
def f(x : Any) = x match {
case (x : LS) => Some(x)
case _ => None
}
@yoshihiro503
yoshihiro503 / WHILE_true.v
Created December 28, 2013 06:49
Equiv_Jの練習問題 WHILE_true ref: http://qiita.com/yoshihiro503/items/260b9342ab049778ef11
Theorem WHILE_true: forall b c,
bequiv b BTrue ->
cequiv
(WHILE b DO c END)
(WHILE BTrue DO SKIP END).
Proof.
move => b c H.
unfold cequiv => st st'.
split => HH.
- destruct(WHILE_true_nonterm b c st st' H). by assumption.
@yoshihiro503
yoshihiro503 / assign_equiv.v
Created December 28, 2013 08:02
Equiv_Jの練習問題assign_equivの証明 #ProofCafe ref: http://qiita.com/yoshihiro503/items/5a6eb6f0c8d2b96c4d4c
(** **** 練習問題: ★★, recommended (assign_aequiv) *)
Theorem assign_aequiv : forall X e,
aequiv (AId X) e ->
cequiv SKIP (X ::= e).
Proof.
move=> X e H. split => HH.
- inversion HH. subst.
assert (st' = update st' X (st' X)).
- apply functional_extensionality => x.
by rewrite update_same; reflexivity.
@yoshihiro503
yoshihiro503 / example.pml
Last active January 2, 2016 16:48
Basic Spin Manual「もうひとつの例 (Another Example）」
#define MAX 5
mtype = { mesg, ack, nak, err };
proctype sender(chan in_, out)
{ byte o, s, r;
o=MAX-1;
do
:: o = (o+1)%MAX; /* next msg */
@yoshihiro503
yoshihiro503 / file0.txt
Created April 24, 2014 10:38
なぜCoqが重要か ref: http://qiita.com/yoshihiro503/items/7e6a9994eb37ed7c3bf9
Theorem map_length: forall A B:Type f xs,
length (map f xs) = length xs.
Proof.
intros A B f xs. induction xs.
reflexivity.
simpl. rewrite IHxs. reflexivity.
Qed.
@yoshihiro503
yoshihiro503 / SsreflectSample.v
Created April 26, 2014 00:33
Ssreflect Tutorial最初のコード ref: http://qiita.com/yoshihiro503/items/6a1f0c6933daafd4754b
Require Import ssreflect ssrbool eqtype ssrnat.
Section HilbertSaxiom.
Variables A B C : Prop.
Lemma HilbertS : (A -> B -> C) -> (A -> B) -> A -> C.
Proof.
move=> hAiBiC hAiB hA.
move: hAiBiC.