写真

某所の人からTwitterで呼び出されたので,「あれ俺の荷物なんか置いたまんまだっけ」と思って焦って某所に行くと,「集合写真をとってほしい」といわれる.まあミーティング中だったが別に自分のターンじゃないからいいかと思って,とりあえず了承.感想:なんで写真撮るだけであんな時間がかかるんだ! まあ,残るものだから,多少こだわりが強いのは仕方ないか.

卒研発表の練習は無事に終わる.ちょっと字が小さいかもしれないと言われたが,若干fixが大変そうなので,なおすかどうか迷う."比較的"高齢な方もご覧になるだろうし…...ところで自分の発表になにかまともな質問は来るのだろうか? 一応Coqの無矛盾性とかどうなっているのか調べておくか 1(そんな質問来ないて

多分 Gödel の第二不完全性定理から,「俺の信じるCoqを信じろ」的なことになってしまうのではないかと思うけど,どうだろう.そういや直観主義上の不完全性定理ってどんな感じになってるのかよく知らない.と,思ったけど,いわゆる二重否定変換を使うと直観主義論理は古典論理に埋め込めるので無問題なのかな.こんどしっかり考える.

まあ細かいことは置いといて,とりあえず一応ペアノ算術(Coq 上なのでハイティング算術というべき?)の公理を全部 Coq で示しておいた.雰囲気を出すために,一応,自家製の自然数を作るところからやっておく.あんまり意味はないけど.

Inductive Nat : Type :=
  O : Nat
| S : Nat -> Nat.

Fixpoint plus (x : Nat) (y : Nat) : Nat :=
  match x with
  | O    => y
  | S x' => S (plus x' y)
  end.

Notation "x + y" := (plus x y).

Fixpoint mult (x : Nat) (y : Nat) : Nat :=
  match x with
  | O    => O
  | S x' => y + (mult x' y)
  end.

Notation "x * y" := (mult x y).

Theorem PA1 :
  forall x : Nat , ~(O = S x).
Proof.
  intros x.
  discriminate.
Qed.

Theorem PA2 :
  forall x y : Nat , (S x = S y -> x = y).
Proof.
  intros x y H.
  inversion H.
  reflexivity.
Qed.  

Theorem PA3 :
  forall x : Nat , (x + O = x).
Proof.
  intros x.
  induction x.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHx.
    reflexivity.
Qed.

Theorem PA4 :
  forall x y : Nat , (x + S y = S (x + y)).
Proof.
  intros x y.
  induction x.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHx.
    reflexivity.
Qed.

Lemma plus_assoc :
  forall x y z : Nat , x + y + z = x + (y + z).
Proof.
  intros x y z.
  induction x.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHx.
    reflexivity.
Qed.

Theorem PA5 :
  forall x : Nat , (x * O = O).
Proof.
  intros x.
  induction x.
  - simpl.
    reflexivity.
  - simpl.
    exact IHx.
Qed.

Theorem PA6 :
  forall x y : Nat , (x * S y = x * y + x).
Proof.
  intros x y.
  induction x.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHx.
    rewrite PA4.
    rewrite plus_assoc.
    reflexivity.
Qed.    

Theorem PA7 :
  forall P : Nat -> Prop ,
    P O -> (forall x : Nat , P x -> P (S x)) -> (forall x : Nat , P x).
Proof.
  exact Nat_ind.
Qed.

特に最後のexact Nat_indがウケる.

閑話休題.卒論が,水を得た増えるワカメのように増えて行く.いいことなのか?


  1. 読んでないけど, https://jfr.unibo.it/article/view/1695/1316 とか参考になるっぽい?