(*|
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.
Proof.
  intro.
  fold (bool_to_prop false).
  rewrite<- H.
  simpl.
  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.
Proof.
  apply propositional_extensionality.
  destruct b; simpl.
  -
    split.
    +
      reflexivity.
    +
      trivial.
  -
    split.
    +
      contradiction.
    +
      unfold is_true.
      intro.
      apply true_is_not_false.
      symmetry.
      assumption.
Qed.