$ sudo brew update$ sudo brew install pyenv~/.bash_profile に export PATH="$HOME/.pyenv/shims:$PATH"$ pyenv install -l で最新版を確認$ pyenv install anaconda-2.1.0$ pyenv rehash$ pyenv local anaconda-2.1.0$ pyenv global anaconda-2.1.0
Theorem nat_ind_3 : forall P: nat -> Prop,
P 0 -> P 1 -> P 2 -> (forall n, P n -> P (S(S(S n)))) ->
forall n, P n.
Fixpoint div3(n:nat):nat :=
match n with | S(S(S n')) => S (div3 n') | _ => 0 end.
Fixpoint mod3(n:nat):nat :=
match n with | S(S(S n')) => mod3 n' | _ => n end.
Lemma mod3_012 : forall n,
(mod3 n = 0) \/ (mod3 n = 1) \/ (mod3 n = 2). mod 3に関しては下記のような性質を証明し、以後の書き換えで使用します。
Lemma mod3_idem : forall n, mod3 (mod3 n) = mod3 n. Lemma mod3_add_hom: forall p q, mod3 (mod3 p + mod3 q) = mod3 (p + q). Lemma mod3_mul_hom: forall p q, mod3 (mod3 p * mod3 q) = mod3 (p * q). mod3_012で場合分けと、mod3_add_homでの書き換えを行えばOKです。
Theorem mod3_square_01 : forall a, (mod3 (a*a) = 0) \/ (mod3 (a*a) = 1). a, b, cについて３で割った余りについて計算すればなんとかなります。
Theorem all_mod3_0 : forall a b c, a*a + b*b = 3*c*c -> (mod3 a = 0) /\ (mod3 b = 0) /\ (mod3 c = 0).
Lemma mod3_0_q : forall n, mod3 n = 0 -> exists q, n = 3*q. a, b, cはそれぞれ３の倍数であることが言え、次の様な補題が言えます。
Lemma shrink_by_3 : forall a b c, a*a + b*b = 3*c*c -> (exists a' b' c', a = 3*a' /\ b = 3*b' /\ c = 3*c' /\ a'*a' + b'*b' = 3*c'*c').
Theorem infinite_descent :
forall P : nat -> Prop, (forall n : nat, P n -> exists2 m : nat, m < n & P m) -> forall n : nat, ~ P n.
Lemma cond_of_a: forall a, ~( ~(a=0) /\ (exists b c:nat, a*a+b*b = 3*c*c)). Lemma cond_of_b: forall b, ~( ~(b=0) /\ (exists a c:nat, a*a+b*b = 3*c*c)). Lemma cond_of_c: forall c, ~( ~(c=0) /\ (exists a b:nat, a*a+b*b = 3*c*c)). shrink_by_3を用いて証明出来ます。
この３つから問題３の証明を出来ます。
Theorem abc_are_0 : forall a b c:nat, a*a+b*b = 3*c*c -> (a = 0 /\ b = 0 /\ c = 0). scala> import basic._
import basic._
val f13_1_grevlex = Poly(Seq(
(Mono(Seq(5,0,0))(grevlex), Q(1,1)),
(Mono(Seq(0,4,0))(grevlex), Q(1,1)),
(Mono(Seq(0,0,3))(grevlex), Q(1,1)),
(Mono(Seq(0,0,0))(grevlex), Q(-1,1))
))(grevlex) //> f13_1_grevlex : basic.Poly = x^5 + y^4 + z^3 + -1
val f13_2_grevlex = Poly(Seq(
(Mono(Seq(3,0,0))(grevlex), Q(1,1)),
(Mono(Seq(0,2,0))(grevlex), Q(1,1)),
(Mono(Seq(0,0,2))(grevlex), Q(1,1)),
(Mono(Seq(0,0,0))(grevlex), Q(-1,1))
))(grevlex) //> f13_2_grevlex : basic.Poly = x^3 + z^2 + y^2 + -1
val buch3_base13_grevlex = Poly.reduce(Poly.buchberger(Seq(f13_1_grevlex, f13_2_grevlex))(grevlex))(grevlex)
//> buch3_base13_grevlex : Seq[basic.Poly] = List(
//| x^3 + z^2 + y^2 + -1,
//| y^4 + -x^2z^2 + -x^2y^2 + z^3 + x^2 + -1)
scala> val lex = LexOrder(List('x,'y,'z))
lex: basic.LexOrder = LexOrder(List('x, 'y, 'z))
scala> val f13_1_lex = Poly(Seq(
| (Mono(Seq(5,0,0))(lex), Q(1,1)),
| (Mono(Seq(0,4,0))(lex), Q(1,1)),
| (Mono(Seq(0,0,3))(lex), Q(1,1)),
| (Mono(Seq(0,0,0))(lex), Q(-1,1))
| ))(lex)
f13_1_lex: basic.Poly = x^5 + y^4 + z^3 + -1
scala> val f13_2_lex = Poly(Seq(
| (Mono(Seq(3,0,0))(lex), Q(1,1)),
| (Mono(Seq(0,2,0))(lex), Q(1,1)),
| (Mono(Seq(0,0,2))(lex), Q(1,1)),
| (Mono(Seq(0,0,0))(lex), Q(-1,1))
| ))(lex)
f13_2_lex: basic.Poly = x^3 + y^2 + z^2 + -1
scala> val buch3_base13_lex = Poly.reduce(Poly.buchberger(Seq(f13_1_lex, f13_2_lex))(lex))(lex)
buch3_base13_lex: Seq[basic.Poly] = List(x^3 + y^2 + z^2 + -1, x^2y^2 + x^2z^2 + -x^2 + -y^4 + -z^3 + 1, xy^4 + xz^3 + -x + y^4 + 2y^2z^2 + -2y^2 + z^4 + -2z^2 + 1, xy^2z + -xy^2 + 273/1408xz^12 + 1011/1408xz^11 + -227/1408xz^10 + -9665/4224xz^9 + 211/704xz^8 + 85/32xz^7 + -749/528xz^6 + 1/2xz^4 + -1/2xz^3 + -xz + x + -81/1408y^14 + -459/1408y^12z^2 + -9/176y^12z + 321/704y^12 + -819/1408y^10z^4 + -273/704y^10z^3 + 1323/704y^10z^2 + 39/176y^10z + -4373/4224y^10 + 273/1408y^8z^6 + -501/352y^8z^5 + 2329/1408y^8z^4 + 8551/4224y^8z^3 + -5871/1408y^8z^2 + 13/88y^8z + 395/352y^8 + -819/704y^6z^7 + 8373/1408y^6z^6 + 3213/704y^6z^5 + -3341/176y^6z^4 + -7555/2112y^6z^3 + 1219/66y^6z^2 + 53/88y^6z + -23341/4224y^6 + 273/704y^4z^9 + 9189/1408y^4z^8 + 773/352y^4z^7 + -33823/1056y^4z^6 + -17/3y^4z^5…
scala> buch3_base13_lex.length
res0: Int = 7
scala> buch3_base13_lex(0)
res2: basic.Poly = x^3 + y^2 + z^2 + -1
scala> buch3_base13_lex(1)
res3: basic.Poly = x^2y^2 + x^2z^2 + -x^2 + -y^4 + -z^3 + 1
scala> buch3_base13_lex(2)
res4: basic.Poly = xy^4 + xz^3 + -x + y^4 + 2y^2z^2 + -2y^2 + z^4 + -2z^2 + 1
scala> buch3_base13_lex(4)
res5: basic.Poly = xz^11 + 4xz^10 + xz^9 + -10xz^8 + -4xz^7 + 8xz^6 + 13145211549469524099276049970825174332001934982726555617/49464457656842324243991404386798887698363025825966149632y^22 + 336469772395565067430728152218633828000517403338752050447/98928915313684648487982808773597775396726051651932299264y^20z^2 + 41246821025682957247777391063405260354876124127586033329/98928915313684648487982808773597775396726051651932299264y^20z + -186688514037649654164494156802783046785181037030518263195/49464457656842324243991404386798887698363025825966149632y^20 + 3748115348128909106405657431258725581362590226678884005481/197857830627369296975965617547195550793452103303864598528y^18z^4 + 532878767777869557858761862556643001207912197601994175895/98928915313684648487982808773597775396726051651932299264...
scala> buch3_base13_lex(5)
res6: basic.Poly = y^12 + -y^10 + 3y^8z^3 + -5y^8z^2 + 2y^8 + -10y^6z^4 + 20y^6z^2 + -10y^6 + -7y^4z^6 + 30y^4z^4 + -6y^4z^3 + -30y^4z^2 + 13y^4 + -5y^2z^8 + 20y^2z^6 + -30y^2z^4 + 20y^2z^2 + -5y^2 + -z^10 + z^9 + 5z^8 + -13z^6 + 10z^4 + 3z^3 + -5z^2
scala> buch3_base13_lex(6)
res7: basic.Poly = x^2z^4 + x^2z^3 + -2x^2z^2 + -1/6xz^10 + -2/3xz^9 + -1/4xz^8 + 7/6xz^7 + -1/12xz^6 + -xz^5 + xz^4 + 1/2y^10z^2 + 1/3y^10z + -5/12y^10 + -1/6y^8z^4 + 1/3y^8z^3 + 1/4y^8z^2 + 1/2y^8 + y^6z^5 + -5/3y^6z^4 + -17/6y^6z^3 + 17/6y^6z^2 + 2/3y^6z + -1/3y^6 + -1/3y^4z^7 + -7/2y^4z^6 + -3y^4z^5 + 131/12y^4z^4 + 23/4y^4z^3 + -13y^4z^2 + -8/3y^4z + 29/6y^4 + -17/6y^2z^8 + -4y^2z^7 + 119/12y^2z^6 + 17/2y^2z^5 + -16y^2z^4 + -14/3y^2z^3 + 12y^2z^2 + 5/3y^2z + -55/12y^2 + -7/6z^10 + -7/6z^9 + 55/12z^8 + 21/4z^7 + -31/4z^6 + -15/2z^5 + 83/12z^4 + 41/12z^3 + -31/12z^2
scala>
// buchberger
val buch_f1 = Poly(Seq(
(Mono(Seq(3,0,0))(grlex), Q(1,1)),
(Mono(Seq(1,1,0))(grlex), Q(-2,1))
))(grlex) //> buch_f1 : basic.Poly = x^3 + -2xy
val buch_f2 = Poly(Seq(
(Mono(Seq(2,1,0))(grlex), Q(1,1)),
(Mono(Seq(0,2,0))(grlex), Q(-2,1)),
(Mono(Seq(1,0,0))(grlex), Q(1,1))
))(grlex) //> buch_f2 : basic.Poly = x^2y + -2y^2 + x
val buch_base1 = Poly.buchberger(Seq(buch_f1, buch_f2))(grlex)
//> divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| buch_base1 : Seq[basic.Poly] = ArrayBuffer(x^3 + -2xy, x^2y + -2y^2 + x, -
//| x^2, -2xy, -2y^2 + x)
val buch_base2 = Poly.reduce(buch_base1)(grlex) //> buch_base2 : Seq[basic.Poly] = List(x^2, xy, y^2 + -1/2x)
val buch2_base1 = Poly.buchberger2(Seq(buch_f1, buch_f2))(grlex)
//> divmod
//| divmod
//| divmod
//| divmod
//| divmod
//| buch2_base1 : Seq[basic.Poly] = ArrayBuffer(x^3 + -2xy, x^2y + -2y^2 + x,
//| -x^2, -2y^2 + x, -2xy)
$ /Applications/cfep.app/OpenXM/bin/openxm asir [2189] G=gr([-x^3+y, x^2*y-z], [x,y,z], 0); [-z*x+y^2,y*x^2-z,-x^3+y] [2190] p_nf(x*y^3-z^2+y^5-z^3, G, [x,y,z], 0); 0
$ /Applications/cfep.app/OpenXM/bin/openxm asir
[1891] load("gr");
[1998] load("noro_pd.rr");
[2182] B=[u*t-x, 1-u-y, u+t-u*t-z];
[-x+t*u,-y-u+1,-z+(-t+1)*u+t]
[2183] V=[u,t,x,y,z];
[u,t,x,y,z]
[2184] G=gr(B,V,2);
[y*x+y^2+(z-2)*y-z+1,-x-y-z+t+1,-y-u+1]
[2185] noro_pd.elimination(G,[x,y,z]);
[y*x+y^2+(z-2)*y-z+1]
f divMod List(f1,f2)res7: (List[foo.Poly2], foo.Poly2) = (List(1x^6+1x^2,),1x^7+1x^3+-1y+1)
f divMod List(f2,f1)
res8: (List[foo.Poly2], foo.Poly2) = (List(, 1x^6+1x^2),1x^7+1x^3+-1y+1)
lex
f divMod List(f1,f2)
res7: (List[foo.Poly2], foo.Poly2) = (List(
1x^6+1x^5y+1x^4y^2+1x^4+1x^3y+1x^2y^2+2x^2+2xy+2y^2+2,
1x^6+1x^5y+1x^4+1x^3y+2x^2+2xy+2),
2y^3+-1y+1)
f divMod List(f2,f1)res8: (List[foo.Poly2], foo.Poly2) = (List(
1x^6y^2+1x^5y^5+1x^4y^8+1x^3y^11+1x^2y^14+1x^2y^2+1xy^17+1xy^5+1y^20+1y^8,
),
1y^23+1y^11+-1y+1)
{v: Int | v >= 0} の様に、論理式で修飾された型のことです。Coq などの依存型を用いた定理証明系でもこのような述語を伴った型を使ってプログラミングを出来るところは同じなのですが、liquid type は述語を決定可能なPresburger算術の範囲に限定し、SMTソルバーを用いて自動証明をさせようというところが大きく違います。まぁCoqの証明を書くのは大変だし、開発の現場で必要とされる検証課題はほぼPresburger算術で充分なのだとしたら、自動証明の方が普及までの敷居が低いのは自明。{-@ type Even = {v:Int | v mod 2 = 0} @-} みたいにHaskell のコメントとして、実際のHaskellのコードに註釈します。すると double xs = [x + x | x <- code="" xs=""> のようなHaskellの実装について、{-@ double :: [Nat] -> [Even] @-} の様な仕様を満たすことを自動証明してくれる、というのを試せます。
個人的には Coq で証明を書くの好きなんだけど、やはり前の会社(SIer)や今の会社で仕事をしてみた印象としては、自動証明器も必要なのかなぁとも思います。ならば Why3 とか使って開発すれば良いかなとも思うけど、Haskell みたいに既にメジャーな言語でこの手のツールが使えるというのは、やはり強みなのかなぁと思います。sealed abstract class List[+A] extends ... { def ::[B >: A] (x: B): List[B] = ... } みたいなイディオムを使わざるを得ないとか色々不便なところもあるのですが、この論文は新しい subtyping の定式化をしてみたよという話。OO言語関係に近い話題はこの一件だけでした。Scala などに興味がある人は ECOOP とか聞きに行くべきなんですかね。。。x+(y+z) = (x+y)+z や交換則 x+y=y+x のような規則を満たす演算子に関する場合にどうするかという話。Steinbach という人の論文が間違っているという論文があったけど実はそれは正しくてみたいな話とか、順序付けがNP-hardなことはこうやってSATに変換してとか、（詳細は理解出来ない）門外漢にも楽しめる発表でした。Require Import Relation_Definitions Setoid Morphisms. Require Import Arith Omega.
Inductive Z' : Set := | mkZ' : nat -> nat -> Z'. Definition eq'(z1 z2:Z') : Prop := match z1,z2 with | (mkZ' p1 n1),(mkZ' p2 n2) => (p1+n2 = p2+n1) end. Definition minus'(z:Z') := match z with | mkZ' a b => mkZ' b a end. Definition plus'(z1 z2:Z') := match z1,z2 with | (mkZ' a1 b1),(mkZ' a2 b2) => (mkZ' (a1+a2) (b1+b2)) end.
eq' が Z' の同値関係になっていることを示す必要があります。
以下の様に示します。Add Paramereic Relation 云々は setoid であることを Coq に登録する手続きです。
Lemma refl_eq' : reflexive _ eq'. Lemma sym_eq' : symmetric _ eq'. Lemma trans_eq' : transitive _ eq'. Add Parametric Relation : Z' eq' reflexivity proved by refl_eq' symmetry proved by sym_eq' transitivity proved by trans_eq' as Z'_setoid.
minus', plus' が well-defined であることを示す必要があります。どういうことかというと、$z, z' \in \mathbb{Z}'$ について、$z \sim z'$ ならば $z^{-1} \sim z'^{-1}$ などを示す必要があるということです。これも以下の様に示します。
Add Parametric Morphism : minus' with signature (eq' ==> eq') as minus'_mor. Add Parametric Morphism : plus' with signature (eq' ==> eq' ==> eq') as plus'_mor.
Class Group {S:Set}(eq:S->S->Prop)
(e:S)(inv:S->S)(op:S->S->S) := {
equiv : Equivalence eq ;
equiv_dec :
forall x y:S, {eq x y} + {~(eq x y)} ;
inv_mor :
forall x y:S, eq x y -> eq (inv x) (inv y) ;
op_mor :
forall x1 y1 x2 y2:S, eq x1 y1 -> eq x2 y2 ->
eq (op x1 x2) (op y1 y2) ;
op_assoc :
forall x y z:S, eq (op (op x y) z) (op x (op y z)) ;
left_unit :
forall x:S, eq (op e x) x ;
right_unit :
forall x:S, eq (op x e) x ;
left_inv :
forall x:S, eq (op (inv x) x) e ;
right_inv :
forall x:S, eq (op x (inv x)) e
}.
Instance Z'_group : Group eq' (mkZ' O O) minus' plus'.
A:Type とし、f : list A -> list A な関数とするとき、f (x::nil) = x::nilf (xs ++ ys) = f ys ++ f xsf = rev と言えるか？Require Import FunctionalExtensionality. Require Import List. Require Import Omega. Goal forall (A:Type)(f:list A->list A), (forall xs ys, f (xs++ys) = f ys ++ f xs) -> (forall x, f (x::nil) = x::nil) -> f = (@rev A). Proof. intros. assert(f nil = nil). specialize(app_length (f nil) (f nil)). intro. rewrite <- (H nil nil) in H1. simpl in H1. assert(length (f nil) = 0). omega. induction (f nil). auto. simpl in H2. discriminate H2. assert(forall x xs, f (x::xs) = f xs ++ (x::nil)). intros. replace (x::xs) with ((x::nil) ++ xs). rewrite H. rewrite H0. auto. simpl. auto. extensionality l. induction l. simpl. auto. simpl. rewrite H2. rewrite IHl. auto. Qed.
Inductive theorem : (Ensemble prop) -> prop -> Prop := | intro_and : forall G p q, (G |-- p) -> (G |-- q) -> (G |-- (p && q)) | elim_and_l : forall G p q, (G |-- (p && q)) -> (G |-- p) | elim_and_r : forall G p q, (G |-- (p && q)) -> (G |-- q) | intro_or_l : forall G p q, (G |-- p) -> (G |-- (p || q)) | intro_or_r : forall G p q, (G |-- q) -> (G |-- (p || q)) | elim_or : forall G p1 p2 q, (G |-- (p1 || p2)) -> ((p1::G) |-- q) -> ((p2::G) |-- q) -> (G |-- q) | intro_imp : forall G p q, ((p::G) |-- q) -> (G |-- (p --> q)) | elim_imp : forall G p q, (G |-- (p --> q)) -> (G |-- p) -> (G |-- q) | elim_not : forall G p, (G |-- !(!p)) -> (G |-- p) | intro_not : forall G p, ((p::G) |-- F) -> (G |-- !p) | reflex : forall G p, (p::G) |-- p | dilution : forall G G' p, (G |-- p) -> ((G _+_ G') |-- p) | intro_false : forall G p, (G |-- (p && (!p))) -> (G |-- F) | intro_true : forall G, G |-- T | rule_K : forall G a p q, G |-- ((K a (p --> q)) --> (K a p --> K a q)) | rule_T : forall G a p, G |-- (K a p --> p) | intro_C : forall G p, (O |-- p) -> (G |-- (C p)) | elim_C : forall G a p, G |-- (C p --> K a p) | rule_C_K : forall G p q, G |-- ((C (p --> q)) --> (C p --> C q)) | rule_R : forall G a p, G |-- (C p --> C (K a p)) where "G |-- p" := (theorem G p).
(* A1 may wear red hat (=M1) or white hat (= !M1).
A2 may wear red hat (=M2) or white hat (= !M2). *)
Parameter A1 A2: agent.
Parameter M1 M2: prop.
(* S1 = A1 that said "I do not know whether I wears a red hat".
Therefore, prop "A1 does not know M1",
is commom knowledge. *)
Definition S1 := C (!(K A1 M1)).
(* S2 = Because the king said "At least one of A1 and A2
wears the red hat". Therefore "M1 or M2" is
common knowledge. *)
Definition S2 := C(M2 || M1).
(* S3 = Because A1 can see the A2's hat, A1 would know
!M2 if !M2 stood, and this is common knowledge. *)
Definition S3 := C(!M2 --> K A1 (!M2)).
(* After A1 said "I do not know whether I wears a red hat",
using the common knowledge {S1, S2, S3}, it becomes the
common knowledge that A2 wears the red hat. *)
Theorem two_wise_men : S1::S2::S3::O |-- C M2.
を証明する、ということになります。assert union {
all s:set univ, p,q : univ -> univ |
s.(p + q) = s.p + s.q
}
check union for 4
で Counterexample が見つからない、従ってこの関係式は正しい、というのを確認する問題があった。Sets.Ensemblesというのもあるがここでは自前で集合演算などを定義して証明してみた。集合 S とは univ -> Prop というmembershipを表す述語であり、二項関係 xRy というのも univ -> univ -> Prop という述語であると言う点に注意すれば、あとは単に定義を述語論理で記述するだけである。Section Alloy_Ex. (* univ *) Variable univ : Set. (* relation *) Definition Rel1 := univ -> Prop. (* arity=1 *) Definition Rel2 := univ -> univ -> Prop. (* arity=2 *) (* set = Rel1 *) (* x is an element of s *) Definition In1 (s:Rel1)(x:univ):Prop := s x. (* A is a subset of B *) Definition subset1 (A B:Rel1):Prop := forall x:univ, In1 A x -> In1 B x. (* A = B iff A includes B and B includes A *) Definition eq1 (A B:Rel1):Prop := (subset1 A B) /\ (subset1 B A). (* join operation *) Definition join12 (s:Rel1)(p:Rel2):Rel1 := fun y:univ => (exists x:univ, In1 s x /\ p x y). (* union *) Definition union1 (p q:Rel1):Rel1 := fun x:univ => (p x \/ q x). Definition union2 (p q:Rel2):Rel2 := fun x:univ => fun y:univ => (p x y \/ q x y). Theorem alloy_ex_union : forall (s:Rel1)(p q:Rel2), eq1 (join12 s (union2 p q)) (union1 (join12 s p) (join12 s q)). Proof. intros s p q. unfold eq1. split. unfold subset1. intros x H. unfold In1 in *. unfold join12 in *. destruct H as [x0 [H1 H2]]. unfold union2 in H2. unfold union1. destruct H2; [left|right]; exists x0; split; auto. unfold subset1. intros x H. unfold In1 in *. unfold union1 in H. unfold join12. unfold union2. destruct H; unfold join12 in H; destruct H as [x0 [H1 H2]]; exists x0; split; auto. Qed.
Theorem plus_even_odd_odd : forall n m, even n -> odd m -> odd (n+m).これを証明するのは難しいです。
even, odd を定義します。Inductive even:nat->Prop := | even_0 : even 0 | even_S : forall n, odd n -> even (S n) with odd:nat->Prop := | odd_S : forall n, even n -> odd (S n).
Theorem plus_odd : forall n m, (even n -> odd m -> odd (n+m)) /\ (odd n -> odd m -> even (n+m)). Proof. induction n. intros. split. intros. simpl. auto. intros. inversion H. intros. split. intros. destruct (IHn m). simpl. apply odd_S. apply H2. inversion H. auto. auto. intros. destruct (IHn m). simpl. apply even_S. apply H1. inversion H. auto. auto. Qed.
Theorem plus_even_odd_odd : forall n m, even n -> odd m -> odd (n+m). Proof. intros. destruct (plus_odd n m). apply H1; auto. Qed.
omega などを使わずに証明出来ました。
U:Set として現し、その上の関係 univ -> univ は U -> U -> Prop として表現できる。後は、関係に対する join などの演算子を定義すれば、同等性の証明を Coq で確認することが出来る。U_dec: forall u u':U, {u=u'}+{u<>u'} や、Uが有限集合であることなどの性質を使わなくても等価であることが判る。Section Alloy1. (* See "Software Abstraction" Alloy Tutorial *) (* http://d.hatena.ne.jp/kencoba/20120212 *) (* univ *) Parameter U:Set. (* relation *) Definition relation := U -> U -> Prop. Definition JOIN(R S:relation):relation := fun x => (fun z => (exists y:U, R x y /\ S y z)). Definition INV(R:relation):relation := fun x => (fun y => (R y x)). Definition IN(R S:relation):Prop := forall x y:U, R x y -> S x y. Definition IDEN:relation := fun x => (fun y => (x=y)). Definition AND(R S:relation):relation := fun x => (fun y => R x y /\ S x y). Definition NO(R:relation):Prop := forall x y, ~(R x y). Definition SOME(R:relation):Prop := exists x, exists y, R x y. Lemma NonEmpty : forall r:relation, (SOME r) <-> (exists x, exists y, r x y). Proof. intros. split. unfold SOME. intro. assumption. intros. unfold SOME. assumption. Qed. Lemma Transitive : forall r:relation, (IN (JOIN r r) r) <-> (forall x y z, r x y -> r y z -> r x z). Proof. intros. split. intros. unfold IN in H. unfold JOIN in H. specialize (H x z). eapply H. exists y. split; assumption. intros. unfold IN. unfold JOIN. intros x z H0. destruct H0 as [y [H1 H2]]. eapply (H x y z). exact H1. exact H2. Qed. Lemma Irreflexive : forall r:relation, (NO (AND IDEN r)) <-> (forall x, ~r x x). Proof. intros. split. intros. unfold NO in H. unfold AND in H. unfold IDEN in H. specialize(H x x). intro. elim H. split. reflexivity. assumption. intros. unfold NO. unfold AND. unfold IDEN. intros. intro. destruct H0. rewrite <- H0 in *. elim (H x). assumption. Qed. Lemma Symmetric : forall r:relation, (IN (INV r) r) <-> (forall x y, r x y -> r y x). Proof. intros. split. intros. unfold IN in H. unfold INV in H. eapply H. assumption. intros. unfold IN. unfold INV. intros. eapply H. assumption. Qed. Lemma Functional : forall r:relation, (IN (JOIN (INV r) r) IDEN) <-> (forall x y1 y2, r x y1 -> r x y2 -> y1 = y2). Proof. intros. split. intros. unfold IN in H. unfold JOIN in H. unfold INV in H. unfold IDEN in H. specialize (H y1 y2). eapply H. exists x. split; assumption. intros. unfold IN. unfold JOIN. unfold INV. unfold IDEN. intros. destruct H0. destruct H0. eapply (H x0 x y); assumption. Qed. Lemma Injective : forall r:relation, (IN (JOIN r (INV r)) IDEN) <-> (forall x1 x2 y, r x1 y -> r x2 y -> x1=x2). Proof. intros. split. intros. unfold IN in H. unfold JOIN in H. unfold INV in H. unfold IDEN in H. specialize(H x1 x2). eapply H. exists y. split; assumption. intros. unfold IN. unfold JOIN. unfold INV. unfold IDEN. intros. destruct H0. destruct H0. eapply (H x y x0); assumption. Qed. Definition set := U -> Prop. Definition SIN(R S:set):Prop := forall x:U, R x -> S x. Definition UNIV:set := fun x:U => True. Definition JOIN_SR(S:set)(R:relation):set := fun y => (exists x:U, S x /\ R x y). Definition JOIN_RS(R:relation)(S:set):set := fun x => (exists y:U, R x y /\ S y). Lemma Total : forall r:relation, (SIN UNIV (JOIN_RS r UNIV)) <-> (forall x, exists y, r x y). Proof. intros. split. intros. unfold SIN in H. unfold JOIN_RS in H. unfold UNIV in H. specialize (H x). specialize(H I). destruct H. destruct H. exists x0. assumption. intros. unfold SIN. unfold JOIN_RS. unfold UNIV. intros. specialize(H x). destruct H. exists x0. split; auto. Qed. Lemma Surjective : forall r:relation, (SIN UNIV (JOIN_SR UNIV r)) <-> (forall y, exists x, r x y). Proof. intros. split. intros. unfold SIN in H. unfold JOIN_SR in H. unfold UNIV in H. specialize(H y). specialize(H I). destruct H. destruct H. exists x. auto. intros. unfold SIN. unfold JOIN_SR. unfold UNIV. intros. specialize(H x). destruct H. exists x0. split; auto. Qed. End Alloy1.
(fun x => f x) = f が言えないので、ライブラリ Logic.FunctionalExtensionality を Import してるとか extensionality というタクティックを使ってるとかが目新しいぐらいで、他は単に型クラス定義してインスタンスが公理を満たすのを証明するだけ。
Section PartialFunctionMonoid.
(* See http://stackoverflow.com/questions/9067904/scala-partialfunction-can-be-monoid *)
Require Import Logic.FunctionalExtensionality.
Class Monoid(T:Type) := {
op : T -> T -> T;
e : T;
left_id : forall t, op e t = t;
right_id : forall t, op t e = t;
assoc : forall t u v, op (op t u) v = op t (op u v)
}.
Variable A B:Type.
Definition pf := A -> option B.
Definition orElse(f g:pf):pf :=
fun a => match (f a) with
| None => g a
| Some b => Some b
end.
Instance pf_monoid : Monoid pf := {
op := orElse;
e := (fun a => None)
}.
Proof.
intros. unfold orElse. simpl.
extensionality a. auto.
intros. unfold orElse.
extensionality a. destruct (t a); auto.
intros. unfold orElse. extensionality a.
destruct (t a); auto.
Defined.
End PartialFunctionMonoid.
(** Group defined by one operation *)
(* Operator 'x/y' means xy^{-1}.
Probe that '/' and four axioms obout it defines a group. *)
Section Group2.
Parameter G:Set.
(* G is not an empty set. At least one element exists. *)
Parameter g0:G.
Parameter op:G->G->G.
Notation "a / b" := (op a b).
(* Axioms for / *)
Parameter G1: forall a b, a/a = b/b.
Parameter G2: forall a b, a/(b/b) = a.
Parameter G3: forall a b c, (a/a)/(b/c) = c/b.
Parameter G4: forall a b c, (a/c)/(b/c) = a/b.
Definition e:G := g0/g0.
Notation "1" := e.
Definition mult(a b:G) := (a/(1/b)).
Notation "a * b" := (mult a b).
Lemma op_refl_1 : forall a, a/a = 1.
Proof.
intro a. unfold "1". eapply G1.
Qed.
Lemma op_1 : forall a, a/1 = a.
Proof.
intro. unfold "1". rewrite G2. auto.
Qed.
Theorem left_id : forall a, 1*a = a.
Proof.
intro. unfold "1". unfold "*".
erewrite G3. eapply op_1.
Qed.
Theorem right_id : forall a, a*1 = a.
Proof.
intro. unfold "*". erewrite op_1.
erewrite op_1. auto.
Qed.
Definition inv(a:G) := (1/a).
Notation "! a" := (inv a) (at level 91).
Theorem left_inv : forall a, (!a)*a=1.
Proof.
intros. unfold "!". unfold "*".
rewrite G4. erewrite op_1. auto.
Qed.
Lemma inv_inv : forall a, 1/(1/a) = a.
Proof.
intros.
replace (1/(1/a)) with (1/1/(1/a)).
rewrite G3. eapply op_1.
erewrite op_1. auto.
Qed.
Theorem right_inv : forall a, a*(!a)=1.
Proof.
intros. unfold "!". unfold "*".
erewrite inv_inv. eapply op_refl_1.
Qed.
Lemma inv_op : forall a b, inv (a/b) = b/a.
Proof.
intros. unfold "!". unfold "1".
erewrite G3. auto.
Qed.
Lemma inv_idem : forall a, inv (inv a) = a.
Proof.
intros. unfold "!". eapply inv_inv.
Qed.
Lemma op_eq : forall a b c d,
a/b = c/d -> b/a = d/c.
Proof.
intros.
replace (b/a) with (1/1/(a/b)).
replace (d/c) with (1/1/(c/d)).
rewrite H. auto.
erewrite G3. auto.
erewrite G3. auto.
Qed.
Lemma op_mult : forall a b, (a/b)*b = a.
Proof.
intros. unfold "*". erewrite G4.
eapply op_1.
Qed.
Lemma rm_op_2 : forall a b c, a/c=b/c -> a=b.
Proof.
intros. assert(a/c*c = b/c*c).
rewrite H. auto.
erewrite op_mult in H0.
erewrite op_mult in H0. auto.
Qed.
Lemma rm_op_1 : forall a b c, a/b=a/c -> b=c.
Proof.
intros. specialize(op_eq a b a c H). intro.
eapply (rm_op_2 b c a H0).
Qed.
Lemma mult_op : forall a b, (a*b)/b = a.
Proof.
intros. unfold "*".
replace (a/(1/b)/b) with (a/(1/b)/(1/(1/b))).
rewrite G4. rewrite op_1. auto.
replace (1/(1/b)) with b. auto.
erewrite inv_inv. auto.
Qed.
Lemma assoc_2 : forall a b c, a/(b/c) = a*c/b.
intros.
replace (a/(b/c)) with ((a*c)/c/(b/c)).
rewrite G4. auto.
rewrite mult_op. auto.
Qed.
Lemma assoc_3 : forall a b c, a*(c/b) = a*c/b.
intros.
replace (a*(c/b)) with (a/(inv (c/b))).
unfold "!". replace (1/(c/b)) with (b/c).
rewrite assoc_2. auto.
replace (1/(c/b)) with (1/1/(c/b)).
rewrite G3. auto. rewrite op_1. auto.
unfold inv. unfold "*". auto.
Qed.
Lemma assoc_4 : forall a b c, a*(c*(inv b)) = a*c*(inv b).
intros. unfold inv.
replace (c*(1/b)) with (c/b).
replace (a*c*(1/b)) with (a*c/b).
eapply assoc_3.
unfold "*". rewrite inv_inv. auto.
unfold "*". rewrite inv_inv. auto.
Qed.
Theorem assoc : forall a b c, a*(b*c) = a*b*c.
intros.
replace c with (inv (inv c)).
eapply assoc_4.
eapply inv_idem.
Qed.
End Group2.