Print bool. Print bool_rect. Print bool_ind. Print bool_rec. (* negate *) 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. (* forall (A : Type) (b : bool) (vT vF : A), if_spec b vT vF (b = false) b (if b then vT else vF) *) Print if_spec. (* CoInductive if_spec (A : Type) (b : bool) (vT vF : A) (not_b : Prop) : bool -> A -> Set := IfSpecTrue : b -> if_spec b vT vF not_b true vT | IfSpecFalse : not_b -> if_spec b vT vF not_b false vF *) (* upon case analysis, match (a subterm in) the goal with "(if b then vT else vF)" and generate to goals: 1. b is replaced with true, b is pushed on the stack 1. b is replaced with false, not_b is pushed on the stack *) 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. (* forall b1 : bool, alt_spec b1 b1 b1 *) Check (boolP (0 == 1)). (* alt_spec (0 == 1) (0 == 1) (0 == 1) *) Check alt_spec. Print alt_spec. (* two combinations possible: P b true P b false upon case analysis, there are two branches: - "(0 == 1)" is replaced by true and the hypothesis "(0 == 1) (= true)" is pushed - "(0 == 1)" is replaced by false and the hypothesis "~~ (0 == 1)" = "(0 != 1)" is pushed *)