Bool型

From Stdlib Require Import Logic.PropExtensionality.

Definition bool_to_prop
  (b : bool)
  : Prop
  := if b then True else False.

以下の補題は intro. inversion H. だけでも証明できるが、それが本質的に行なっていることは以下の証明と同じである。

Lemma true_is_not_false : true <> false.
true <> false
Proof.
true <> false
  intro.
H: true = false
False
  fold (bool_to_prop false).
H: true = false
bool_to_prop false
  rewrite<- H.
H: true = false
bool_to_prop true
  simpl.
H: true = false
True
  trivial.
Qed.

bool_to_prop は以下のようにも定義できる。

Definition is_true
  (b : bool)
  : Prop :=
  b = true.

Lemma bool_to_prop_is_true (b : bool) :
  bool_to_prop b = is_true b.
b: bool
bool_to_prop b = is_true b
Proof.
b: bool
bool_to_prop b = is_true b
  apply propositional_extensionality.
b: bool
bool_to_prop b <-> is_true b
  destruct b; simpl.
True <-> is_true true
False <-> is_true false
  -
True <-> is_true true
    split.
True -> is_true true
is_true true -> True
    +
True -> is_true true
      reflexivity.
    +
is_true true -> True
      trivial.
  -
False <-> is_true false
    split.
False -> is_true false
is_true false -> False
    +
False -> is_true false
      contradiction.
    +
is_true false -> False
      unfold is_true.
false = true -> False
      intro.
H: false = true
False
      apply true_is_not_false.
H: false = true
true = false
      symmetry.
H: false = true
false = true
      assumption.
Qed.