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 / SigSample.v
Created July 22, 2014 09:49
sig_sample
Require Import Arith.
Definition x : {n | n > 0}.
Proof.
refine (@exist nat (fun n => n > 0) 10 _).
auto 10.
auto with arith.
Defined.
@yoshihiro503
yoshihiro503 / SsreflectTutorial_3.4_edivnP_right.v
Created July 26, 2014 06:02
Lemma edivnP_right : forall m d, edivn_spec_right m d (edivn m d).
Proof.
Check edivnP.
move=> m d.
case: (edivnP m d) => q r eq_m_dqr impl_0d_rd.
by apply: EdivnSpec_right.
Qed.
@yoshihiro503
yoshihiro503 / SsreflectTutorial_3.4_edivnP_left.v
Created July 26, 2014 06:07
Lemma edivnP_left : forall m d, edivn_spec_left m d (edivn m d).
Proof.
move=> m d.
case: (edivnP m d) => q r eq impl.
by apply EdivnSpec_left.
Qed.
@yoshihiro503
yoshihiro503 / CoqCodingRules.md
Last active August 29, 2015 14:22
@yoshihiro503
yoshihiro503 / Make
Last active August 29, 2015 14:23
AffeldtさんのSsreflectチュートリアルのソースをビルドする ref: http://qiita.com/yoshihiro503/items/f5a5d6d59e5d844b4779
-R .
bigop2_example.v
group_example.v
predicative_example.v
bigop_example.v
ssrbool_example.v
dependent_example.v
logic_example.v
ssrnat_example.v
eqtype_example.v
@yoshihiro503
yoshihiro503 / logical_example.v
Last active August 29, 2015 14:25
AffeldtさんのSsreflect練習問題exo4 ref: http://qiita.com/yoshihiro503/items/bd142fdb69c1fd64ab86
Lemma exo4 : False \/ True.
Proof.
right. exact I.
Qed.
@yoshihiro503
yoshihiro503 / Make
Last active August 29, 2015 14:27
coqdocで日本語を含むPDFを生成する ref: http://qiita.com/yoshihiro503/items/2e3035cc602301c7c9fc
-R src JapaneseCoqdocSampleProject
src/Hoge.v
src/Piyo.v
-custom "platex Proof.tex; platex Proof.tex" "Proof.tex $(VOFILES) $(VFILES:.v=.tex)" "Proof.dvi"
-custom "dvipdfmx Proof.dvi" "Proof.dvi" Proof.pdf
@yoshihiro503
yoshihiro503 / Ninja.v
Created August 13, 2015 11:13
Coqでもあのニンジャパターンマッチが使えるぜ ref: http://qiita.com/yoshihiro503/items/c83fb2a6e2a6318db108
let '(x, y, z) := (1, 2, 3) in
...
@yoshihiro503
yoshihiro503 / Otoshiana.v
Created August 28, 2015 10:33
なぞなぞ：Coqの関数定義でなぜか戻り値がSetじゃないとダメと起こられる例:
Definition foo (b : bool) : nat =
if b then 0 else 1.
@yoshihiro503
yoshihiro503 / 未解決問題.v
Last active September 11, 2015 05:00
Require Import Program Arith.
(** * リストモジュールの拡張 *)
Module List.
Require Export List.
Fixpoint _index_of_loop {A:Type} (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs i :=
match xs with
| nil => None
| x::xs => if eq_dec x a then Some i else _index_of_loop eq_dec a xs (S i)