天泣記

Coq は直感主義なので一般には命題の 2重否定の除去はできないのだが、 is_true b という形の bool から作られる命題の 2重否定は除去できたっけ? と思って試す

From mathcomp Require Import all_ssreflect.

Lemma test2 (b : bool) : ~ ~ b <-> b.
Proof.
  case: b; split => //.
  move=> _.
  by apply.
Qed.

うむ、できるよな (b は bool であって命題ではないが、SSReflect では bool から Prop への coercion として is_true が指定されていて、~ ~ b <-> b は実は ~ ~ (is_true b) <-> (is_true b) となっている)

not をもっと並べてみる

Lemma test4 (b : bool) : ~ ~ ~ ~ b <-> b.
Proof.
  case: b; split => //.
    move=> _.
    rewrite /not.
    by do 2 apply.
  move=> H.
  exfalso.
  apply H.
  by apply.
Qed.

Lemma test6 (b : bool) : ~ ~ ~ ~ ~ ~ b <-> b.
Proof.
  case: b; split => //.
    move=> _.
    rewrite /not.
    by do 3 apply.
  move=> H.
  exfalso.
  apply H.
  by do 2 apply.
Qed.

Lemma test8 (b : bool) : ~ ~ ~ ~ ~ ~ ~ ~ b <-> b.
Proof.
  case: b; split => //.
    move=> _.
    rewrite /not.
    by do 4 apply.
  move=> H.
  exfalso.
  apply H.
  by do 3 apply.
Qed.

まぁ、偶数個なら問題なくいけるようだ

一般的に証明してみよう

Fixpoint even_nots (n : nat) (P : Prop) : Prop :=
  match n with
  | 0 => P
  | m.+1 => ~ ~ (even_nots m P)
  end.

Lemma test_even (n : nat) (b : bool) : even_nots n b <-> b.
Proof.
  case: b; split => //.
    move=> _.
    elim: n => //= n IH.
    by apply.
  elim: n => //= n IH H.
  exfalso.
  by apply H => /IH.
Qed.

特に問題なく証明できるようだ

奇数個ならどうか

Lemma test3 (b : bool) : ~ ~ ~ b <-> ~ b.
Proof.
  case: b; split => //.
    move=> H.
    exfalso.
    apply H.
    by apply.
  move=> _.
  by apply.
Qed.

Lemma test5 (b : bool) : ~ ~ ~ ~ ~ b <-> ~ b.
Proof.
  case: b; split => //.
    move=> H.
    exfalso.
    apply H.
    by do 2 apply.
  move=> _.
  by do 2 apply.
Qed.

Lemma test7 (b : bool) : ~ ~ ~ ~ ~ ~ ~ b <-> ~ b.
Proof.
  case: b; split => //.
    move=> H.
    exfalso.
    apply H.
    by do 3 apply.
  move=> _.
  by do 3 apply.
Qed.

まぁ、できるようだな

一般的に証明してみよう

Fixpoint odd_nots (n : nat) (P : Prop) : Prop :=
  match n with
  | 0 => ~ P
  | m.+1 => ~ ~ (odd_nots m P)
  end.

Lemma test_odd (n : nat) (b : bool) : odd_nots n b <-> ~ b.
Proof.
  case: b; split => //.
    elim: n => //= n IH H.
    exfalso.
    apply: H => H.
    by apply IH.
  move=> _.
  elim: n => //= n IH.
  by apply.
Qed.

ちゃんとできるな

天泣記

2023-02-08 (Wed)

2023-02-28 (Tue)