昨年の年末から作っていたBrzozowski'sの正規表現アルゴリズム（去年の年末にLtUで話題になった正規表現の微分を使ったYacc is Deadのやつ）のCoqライブラリ化（実装がKleene代数の公理を満たす事を証明）が完成してCoqのUser contributionsに載ったので、その話をしました。（当日のプレゼン資料に一部加筆）
もうレポート提出期限も過ぎたので、今年のGarrigue先生の授業のレポート課題をみんなで解いてみよう、というのをしました。
私の証明はこんな感じ。最初の命題論理の証明は問題無かった様子。
Section Coq1.
Variables P Q R : Prop.
Theorem and_compose : (P -> Q) -> (P -> R) -> P -> Q /\ R.
Proof.
intros pq pr p.
split.
apply (pq p).
apply (pr p).
Qed.
Theorem or_modus : P \/ (Q -> R) -> Q -> P \/ R.
Proof.
intros p_qr q.
destruct p_qr as [p|qr].
left. apply p.
right. apply (qr q).
Qed.
End Coq1.
次が append に関する性質で、これは解けた人が多かったです。
Section Coq2.
Require Import List.
Variable A : Set.
Fixpoint append (l1 l2 : list A) {struct l1} :=
match l1 with
| nil => l2
| a :: l => a :: append l l2
end.
Theorem append_inv_head : forall l l1 l2 : list A,
append l l1 = append l l2 -> l1 = l2.
Proof.
induction l.
intros. simpl in H. auto.
intros. simpl in H. inversion H.
eapply IHl. auto.
Qed.
後半の問題は難しいみたいでした。私の解答は下記です。最初に幾つか補題を定義して目的の定理を証明しました、というのは嘘で、目的の定理を証明してる最中に欲しくなった補題を戻って証明しただけです。inversionが使えれば解ける問題だと思うので、やはりCoq初心者脱出の鍵はinversionを使える様になる、かと思う。
Lemma append_nil : forall l, append l nil = l.
Proof.
induction l; simpl; [|erewrite IHl]; auto.
Qed.
Lemma append_l1_a_l2 : forall a l1 l2,
append l1 (a::l2) = append (l1 ++ a::nil) l2.
Proof.
induction l1; intros; simpl; [|erewrite IHl1]; auto.
Qed.
Lemma append_cons_not_nil : forall (a:A) l l', l ++ a::l' <> nil.
Proof.
induction l; simpl; intros; intro; discriminate H.
Qed.
Lemma append_inv_a : forall (a:A) l1 l2,
l1 ++ a :: nil = l2 ++ a :: nil -> l1 = l2.
Proof.
induction l1; induction l2; simpl; intros.
(* l1 = nil, l2 = nil *)
auto.
(* l1 = nil, l2 = a0::l2 *)
inversion H.
specialize(append_cons_not_nil a0 l2 nil). intros.
rewrite <- H2 in H0. elim H0. auto.
(* l1 = a::l1, l2 = nil *)
inversion H.
specialize(append_cons_not_nil a l1 nil). intros.
rewrite H2 in H0. elim H0. auto.
(* l1 = a::l1, l2 = a0::l2 *)
inversion H.
rewrite (IHl1 l2 H2). auto.
Qed.
Theorem append_inv_tail : forall l l1 l2 : list A,
append l1 l = append l2 l -> l1 = l2.
Proof.
induction l; intros; simpl in H.
(* l = nil *)
repeat erewrite append_nil in H. auto.
(* l = a::l *)
rewrite (append_l1_a_l2 a l1 l) in H.
rewrite (append_l1_a_l2 a l2 l) in H.
eapply (append_inv_a a). eapply (IHl _ _ H).
Qed.
End Coq2.
revして前の定理に帰着せせる、という解答もありました。そっちは思いつかなかった。
あとは、HOL-OCLというのがあるよ、とか。OCLってどの程度メジャーなんでしょうか。広く使われていて需要がありそうならIsabelleも勉強すべきかなぁ、とか。
