pptx

情報科学概論
第6回
1
Logic
〜Coqにおける論理〜
2
Coqにおける論理演算子
組込み
帰納的定義
(Inductive)
全称記号(∀)
ならば,含意(→)
派生
(組込みから作られる)
かつ,連言
または,宣言
否定
存在量化子
等号
．．．
3
量化子と含意
∀
(_:P), Q
Definition funny_prop1 :=
∀n, ∀(E : beautiful n), beautiful (n+3).
Definition funny_prop1'' :=
∀n, beautiful n → beautiful (n+3).
P→Q
糖衣構文
4
かつ ∧
P, QもProp
Inductive and (P Q : Prop) : Prop :=
conj : P → Q → (and P Q).
Notation "P ∧ Q" := (and P Q) : type_scope.
型のスコープ
conj p q は and P Q の根拠
← p は P の根拠，かつ q は Q の根拠
前項がand P Q の根拠を与える唯一の方法
5
conj の型
P, Qは命題
Check conj.
(* ===> forall P Q : Prop,
P -> Q -> P /\ Q *)
根拠
根拠
根拠
6
連言を用いた証明対象
Theorem and_example :
(beautiful 0) /\ (beautiful 3).
Proof.
split でも可
apply conj.
(* Case "left". *) apply b_0.
(* Case "right". *) apply b_3. Qed.
Print and_example.
(* ===> conj (beautiful 0) (beautiful 3) b_0 b_3
: beautiful 0 /\ beautiful 3 *)
7
(復習) Curry-Howard同型対応
論理の世界
命題
根拠
計算の世界
型
データ
計算の世界のことばで
論理の世界を解釈できる
8
P /\ Q の Inversion
Theorem proj1 : forall P Q : Prop,
P /\ Q -> P.
Proof.
intros P Q H.
inversion H as [HP HQ].
apply HP. Qed.
9
inversion の練習
Theorem even__ev : ∀n : nat,
(even n → ev n) ∧ (even (S n) → ev (S n)).
Proof.
induction n as [|n'].
split.
Case "n = O".
intros H. apply ev_0.
intros H. inversion H.
Case "n = S n'".
split.
SCase "left". intros H. apply proj2 in IHn'.
apply IHn'. apply H.
SCase "Right". intros H. apply proj1 in IHn'.
apply IHn' in H. apply ev_SS. apply H.
Qed.
10
Iff, ↔
Definition iff (P Q : Prop) :=
(P
→
Q)
∧
(Q
→
P).
Notation "P ↔ Q" :=
(iff P Q)
(at level 95, no associativity)
: type_scope.
11
または, 選言 ∨
Inductive or (P Q : Prop) : Prop :=
| or_introl : P
| or_intror : Q
→
→
or P Q
or P Q.
Notation "P ∨ Q" := (or P Q)
: type_scope.
12
選言を用いた証明対象
Theorem or_commut : forall P Q : Prop,
P \/ Q -> Q \/ P.
Proof.
intros P Q H.
left でも可
inversion H as [HP | HQ].
Case "left". apply or_intror. apply HP.
Case "right". apply or_introl. apply HQ.
Qed.
right でも可
13
∧ ,∨ と andb, orb の関係
論理
計算
Theorem andb_true__and :
andb b c = true
→
∧
c,
b = true
Theorem and__andb_true :
b = true
∀b
c = true
→
∀b
∧
c = true.
c,
andb b c = true.
14
偽
Inductive False : Prop := .
コンストラクタ
が無い(根拠を与
えられない)
Theorem ex_falso_quodlibet : ∀(P:Prop),
False → P.
Proof.
前提が偽なら
(* WORKED IN CLASS *)
何でもいえる
intros P contra.
inversion contra. Qed.
15
否定
偽なら
全体が真
Definition not (P:Prop) := P → False.
Notation "~ x" := (not x) : type_scope.
不等号
Notation "x <> y" := (~ (x = y)) : type_scope.
16
存在量化子
Inductive ex (X:Type) (P : X→Prop) : Prop :=
ex_intro : ∀(witness:X), P witness → ex X P.
Definition some_nat_is_even : Prop :=
ex nat ev.
Definition snie : some_nat_is_even :=
ex_intro _ ev 4 (ev_SS 2 (ev_SS 0 ev_0)).
根拠
Notation "'exists' x , p" := (ex _ (fun x => p)) …
Notation "'exists' x : X , p" := (ex _ (fun x:X =>
p)) …
∃
17
例：存在量化子
Example exists_example_1 :
exists n, n + (n * n) = 6.
Proof.
apply ex_intro with (witness:=2).
reflexivity.
exists 2. でも可
Qed.
Inductive ex (X:Type) (P : X→Prop) : Prop :=
ex_intro : ∀(witness:X), P witness → ex X P.
18
等価性
Inductive eq (X:Type) : X → X → Prop :=
refl_equal : ∀x, eq X x x.
Notation "x = y" := (eq _ x y) …
Inductive eq' (X:Type) (x:X) : X → Prop :=
refl_equal' : eq' X x x.
Notation "x =' y" := (eq' _ x y) …
Coqでの
定義
19
命題としての関係
Inductive le : nat → nat → Prop :=
| le_n : ∀n, le n n
| le_S : ∀n m, (le n m) → (le n (S m)).
Inductive le (n:nat) : nat → Prop :=
| le_n : le n n
| le_S : ∀m, (le n m) → (le n (S m)).
Notation "m <= n" := (le m n).
21
Imp
〜単純な命令型プログラム〜
Impの構文と意味論
後の章では、
プログラムの等価性や
ホーア論理
23
例
Z ::= X;
Y ::= 1;
WHILE not (Z = 0) DO
Y ::= Y * Z;
Z ::= Z - 1
END
24
概要
算術式と論理式
変数の導入
コマンド
代入、条件、連接、繰り返し
25
算術式と論理式：BNF
aexp ::=
|
|
|
nat
aexp '+' aexp
aexp '-' aexp
aexp '*' aexp
bexp ::=
|
|
|
|
|
true
false
aexp '=' aexp
aexp '<=' aexp
bexp 'and' bexp
'not' bexp
26
算術式と論理式：抽象構文
Inductive aexp : Type :=
| ANum : nat → aexp
| APlus : aexp → aexp → aexp
| AMinus : aexp → aexp → aexp
| AMult : aexp → aexp → aexp.
Inductive bexp : Type :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp → aexp → bexp
| BLe : aexp → aexp → bexp
| BNot : bexp → bexp
| BAnd : bexp → bexp → bexp.
27
算術式の評価
Fixpoint aeval (e : aexp) : nat :=
match e with
| ANum n => n
| APlus a1 a2 => (aeval a1) + (aeval a2)
| AMinus a1 a2 => (aeval a1) - (aeval a2)
| AMult a1 a2 => (aeval a1) * (aeval a2)
end.
Example test_aeval1:
aeval (APlus (ANum 2) (ANum 2)) = 4.
Proof. reflexivity. Qed.
28
論理式の評価
Fixpoint beval (e : bexp) : bool :=
match e with
| BTrue => true
| BFalse => false
| BEq a1 a2 => beq_nat (aeval a1) (aeval a2)
| BLe a1 a2 => ble_nat (aeval a1) (aeval a2)
| BNot b1 => negb (beval b1)
| BAnd b1 b2 => andb (beval b1) (beval b2)
end.
29
最適化: 0+e  e
Fixpoint optimize_0plus (e:aexp) : aexp :=
match e with
| ANum n =>
省く
ANum n
| APlus (ANum 0) e2 =>
optimize_0plus e2
| APlus e1 e2 =>
APlus (optimize_0plus e1) (optimize_0plus e2)
| AMinus e1 e2 =>
AMinus (optimize_0plus e1) (optimize_0plus e2)
| AMult e1 e2 =>
AMult (optimize_0plus e1) (optimize_0plus e2)
end.
30
最適化をテスト
Example test_optimize_0plus:
optimize_0plus (APlus (ANum 2)
(APlus (ANum 0)
(APlus (ANum 0) (ANum 1))))
= APlus (ANum 2) (ANum 1).
Proof. reflexivity. Qed.
31
最適化の正しさを証明
Theorem optimize_0plus_sound: ∀e,
aeval (optimize_0plus e) = aeval e.
Proof.
intros e. induction e.
Case "ANum". reflexivity.
Case "APlus". destruct e1.
SCase "e1 = ANum n". destruct n.
SSCase "n = 0". simpl. apply IHe2.
SSCase "n <> 0". simpl. rewrite IHe2. reflexivity.
SCase "e1 = APlus e1_1 e1_2".
simpl. simpl in IHe1. rewrite IHe1.
rewrite IHe2. reflexivity.
SCase "e1 = AMinus e1_1 e1_2".
simpl. simpl in IHe1. rewrite IHe1.
rewrite IHe2. reflexivity.
繰り返しが
SCase "e1 = AMult e1_1 e1_2".
多い
simpl. simpl in IHe1. rewrite IHe1.
rewrite IHe2. reflexivity.
Case "AMinus".
simpl. rewrite IHe1. rewrite IHe2. reflexivity.
Case "AMult".
simpl. rewrite IHe1. rewrite IHe2. reflexivity. Qed.
32
証明の自動化
タクティカル
タクティックを引数にとるタクティック
高階タクティック
新しいタクティック記法の定義
omegaタクティック
その他のタクティック
33
repeat タクティカル
Theorem ev100 : ev 100.
Proof.
repeat (apply ev_SS).
(* ev_SS を50回適用 *)
apply ev_0.
Qed.
34
try タクティカル
try T は、
成功したら T と同じ、
失敗したら何もしない
35
; タクティカル
T; T’
タクティックTで生成された各サブゴールに
タクティックT’を行う
36
例2
Theorem optimize_0plus_sound'': ∀e,
aeval (optimize_0plus e) = aeval e.
Proof.
intros e.
induction e;
(* ほとんどの場合は IH、または *)
try (simpl; rewrite IHe1; rewrite IHe2; reflexivity);
(* 定義で充分 *)
try reflexivity.
(* e = APlus e1 e2 のケースだけが興味深い… *)
Case "APlus".
destruct e1; try (simpl; simpl in IHe1; rewrite IHe1;
rewrite IHe2; reflexivity).
SCase "e1 = ANum n". destruct n;
simpl; rewrite IHe2; reflexivity. Qed.
38
; タクティカル (一般形)
T; [T1 | T2 | ... | Tn]
T;T’ は、以下の通り
T; [T' | T' | ...
| T']
39
新しいタクティック記法の定義
タクティック･スクリプトをプログラミン
グする方法が用意されている…
40
omega タクティック
プレスバーガー算術の判定手順
Omegaアルゴリズム
対象：ゴールが以下から作られ、
全称的に閉じた式
数定数、加算(+ and S)、減算(- and pred)、乗
算
等号(= and <>)、不等号(<=)
論理結合子 ∧, ∨, ~, and →
41
omega タクティック(例)
Example silly_presburger_example :
∀m n o p,
m + n <= n + o ∧ o + 3 = p + 3 →
m <= p.
Proof.
intros. omega.
Qed.
42
その他のタクティック
(自習)
43

Download Report