Library ssrbool_example

Print bool.

Print bool_rect.
Print bool_ind.
Print bool_rec.

Definition match_true := match true with true => false | false => true end.

Check match_true.
Eval compute in match_true.

Definition nat_of_bool := bool_rec (fun _ => nat) 1 0.

Check (nat_of_bool : bool -> nat).

Eval compute in (nat_of_bool false).

Definition dep_of_bool := bool_rec (fun b => match b with true => nat | false => bool end) 1 true.

Check (dep_of_bool : forall b, match b with true => nat | false => bool end).

Eval compute in (dep_of_bool false).

Definition dep_of_bool2 b : match b with true => nat | false => bool end :=
  match b with
      true => 1
    | false => true
  end.

Goal dep_of_bool = dep_of_bool2.
reflexivity.
Qed.

Check dep_of_bool2.

From Ssreflect Require Import ssreflect ssrfun ssrbool.

Print andb.
Print negb.
Print orb.

Goal forall a b : bool, ~~ (a && b) = (~~ a) || (~~ b).
by case; case.
Qed.

From Ssreflect Require Import eqtype ssrnat.

Lemma ifP_example : forall n : nat, odd (if odd n then n else n.+1).
Proof.
move=> n.
case: ifP.
  done.
move=> Hn.
rewrite -addn1.
rewrite odd_add.
by rewrite Hn.
Qed.

Check ifP.
Print if_spec.

Lemma exo23 : forall n : nat, n * n - 1 < n ^ n.
Proof.
move=> n.
case: (boolP (n == O)).
  admit.
move=> n0.
case: (boolP (n == 1)).
  admit.
move=> n1.
have [m Hm] : exists m, n = m.+2.
  admit.
admit.
Abort.

Check boolP.
Check (boolP (0 == 1)).
Check alt_spec.
Print alt_spec.