[Coq] Sample of Setoid

先日のFormal Methods Forumで話したsetoidの話のCoqのコード。

Require Import Setoid.
Require Import Relation_Definitions.
Require Import Arith.
Require Import Compare_dec.
Require Import Omega.

Section MyZ.

(* 整数 Z' を構成するのに、nat * nat に同値関係 Z'eq を入れたものを用いる。
  (a,b) in nat*nat に対し、a-b でZ'を作る、と考えてよい。 *)

(* Z' のコンストラクタ *)
Inductive Z' : Set :=
| mkZ' : nat -> nat -> Z'.

(* 同値関係 : (a,b) =Z= (c,d) iff a+d = b+c *)
Definition Z'eq (z z':Z') : Prop :=
  let (a,b) := z in
  let (c,d) := z' in
  a + d = b + c.

Notation "a =Z= b" := (Z'eq a b) (at level 70).

(* 後々の証明で使いやすい補題 *)
Lemma Z'eq_inv : forall a b c d, (mkZ' a b) =Z= (mkZ' c d) ->
  {exists q, (a=c+q /\ b=d+q)} + {exists q, (a+q=c /\ b+q=d)}.
Proof.
  intros.  simpl in H.
  destruct (le_lt_dec a c).
    (* a <= c *)
    right.  exists (c - a).  omega.
    (* c < a *)
    left.  exists (a - c).  omega.
Qed.

(* Z'eq が同値関係であることを証明する *)
Print reflexive.
Lemma Z'eq_refl : reflexive Z' Z'eq.
Proof.
  unfold reflexive.  intros.  destruct x.
  unfold Z'eq.  omega.
Qed.

Print symmetric.
Lemma Z'eq_sym : symmetric Z' Z'eq.
Proof.
  unfold symmetric.  intros.  destruct x.  destruct y.
  unfold Z'eq in *.  omega.
Qed.

Print transitive.
Lemma Z'eq_trans : transitive Z' Z'eq.
Proof.
  unfold transitive.  intros.  destruct x. destruct y. destruct z.
  unfold Z'eq in *.  omega.
Qed.

(* Z'eq が同値関係であることが示せたので Setoid を構成する *)
Add Parametric Relation : Z' Z'eq
  reflexivity proved by Z'eq_refl
  symmetry proved by Z'eq_sym
  transitivity proved by Z'eq_trans
  as Z'_rel.

(* Z' 上の演算を定義する *)
Definition Z'plus (z z':Z') : Z' :=
  let (a,b) := z in
  let (c,d) := z' in
  mkZ' (a+c) (b+d).

Add Parametric Morphism : Z'plus with
  signature Z'eq ==> Z'eq ==> Z'eq as Z'_plus_mor.
Proof.
  (* Goal := x =Z= y -> x0 =Z= y0 -> Z'plus x x0 =Z= Z'plus y y0
  Z'plus が well-defined であることを示す必要がある *)
  intros.  destruct x; destruct y; destruct x0; destruct y0.
  unfold Z'eq in *.  unfold Z'plus.  omega.
Qed.

(* 準備 *)
Lemma Z'eq_plus_id_l : forall z a, Z'plus (mkZ' a a) z =Z= z.
Proof.
  intros.  destruct z.
  unfold Z'plus; unfold Z'eq.  omega.
Qed.

Lemma Z'eq_plus_comm : forall z z', Z'plus z z' =Z= Z'plus z' z.
Proof.
  intros.  destruct z; destruct z'.
  unfold Z'plus; unfold Z'eq.  omega.
Qed.

(* setoid_rewrite を使ってみる例 *)
Lemma Z'eq_plus_id_r : forall z a, Z'plus z (mkZ' a a) =Z= z. 
Proof.
  intros.
  setoid_rewrite (Z'eq_plus_comm z (mkZ' a a)).
  apply Z'eq_plus_id_l.
Qed.

End MyZ.

[7-Lang][Ruby] Seven Languages in Seven Weeks : Ruby Day 1

　Bruce TateのSeven Languages in Seven Weeksを読み始めました。
　最初の言語はRubyです。各言語をキャラクターに例えているのですが、Ruby = Merry Poppins らしい。
　１日目の課題はこんな感じでOKなのかしらん。

>> puts 'Hello, World!'
Hello, World!
=> nil
>> p "Hello, Ruby".index("Ruby")
7
=> nil
>> puts "@tmiya_\n"*10
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
@tmiya_
=> nil
>> (1..10).each {|n| puts "This is sentence number #{n}" }
This is sentence number 1
This is sentence number 2
This is sentence number 3
This is sentence number 4
This is sentence number 5
This is sentence number 6
This is sentence number 7
This is sentence number 8
This is sentence number 9
This is sentence number 10
=> 1..10

% ruby numberGuess.rb
5
too large
3
too large
1
too small
2
correct!
% cat numberGuess.rb
randomNumber = rand(10)
while ((guess = gets.to_i) != randomNumber)
  if guess < randomNumber then
    puts "too small"
  else
    puts "too large"
  end
end
puts "correct!"

[Misc] Blog Design Changed

Blogのデザインをちょっといじってみました。

[Memo] How to translate LaTeX file with po4a + OmegaT

忘れない様に作業手順メモ
Mac OS X 10.5 で po4a と OmegaT で TeX 文書を翻訳を参考に。

最初にファイルを作るのは

• そもそもTutorial.v.texはTutorial.texからmake tutorialとかで作る。CoqのMakefile参照。


• ~/usr/share/perl/po4a-0.41/po4a-gettextize -f latex -m Tutorial.v.tex -p Tutorial.v.pot


• 上記が通らない場合は po4a の LaTeX.pm, TeX.pm を無理に直したりする。po4a からは platex ではなく latex が呼ばれるのでスタイルも jsbook から book にしたり、フランス人の人名を ASCII の範囲にしたりなど最初に直す。
  

あとはOmegaTを使って翻訳。

• ~/coq/coq-8.2pl1/doc/tutorial/にあるCoq_TutorialというOmegaTプロジェクトを開いて翻訳する。一段落したら訳文ファイル生成。


• cd ~/coq/coq-8.2pl1/doc/tutorial/


• cp Coq_Tutorial/target/Tutorial.v.pot ja.pot


• ~/usr/share/perl/po4a-0.41/po4a-translate -f latex -m Tutorial.v.tex -p ja.pot -l ja.tex


• フォーマットを直す場合はbookじゃなくjsbookに直す。


• platex ja.tex ; platex ja.tex ; dvipdfmx ja.dvi