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.
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.