Library ssrnat_example

From Ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat.


Goal forall n, n + n = 2 * n.
Show Proof.
elim.
  Show Proof.
  rewrite addn0.
  rewrite muln0.
  done.
Show Proof.
move=> n IH.
rewrite addSn.
rewrite addnS.
rewrite IH.
rewrite mulnS.
rewrite -addn2.
rewrite addnC.
done.
Show Proof.
Qed.

Print nat.

Print nat_rect.
Print nat_rect.

Definition mynat_ind_proof := fun (P : nat -> Prop) (f : P 0) (f0 : forall n : nat, P n -> P n.+1) =>
fix F (n : nat) : P n :=
  match n as n0 return (P n0) with
  | 0 => f
  | n0.+1 => f0 n0 (F n0)
  end.

Lemma mynat_ind : forall (P : nat -> Prop), P 0 ->
  (forall n : nat, P n -> P n.+1) ->
  forall n, P n.
exact mynat_ind_proof.
Qed.


Print le.
Print leq.

Goal forall n, 0 <= n.
done.
Show Proof.
Qed.

Print Le.le_0_n.

Goal forall n m, n.+1 <= m.+1 -> n <= m.
done.
Show Proof.
Qed.

Print le_S_n.
Print le_pred.

Goal forall n, n <= n.
done.
Qed.

Goal forall n, n <= n.+1.
done.
Qed.

Goal forall n, n < n = false.
by elim.
Qed.


Lemma exo24 n m : m + n = n + m.
Proof.
Abort.

Lemma exo25 (u : nat -> nat) (u0 : u 0 = 2) (u1 : u 1 = 3) (un : forall n, u n.+2 = 3 * u n.+1 - 2 * u n) n :
  u n = 1 + 2 ^ n.
Proof.
Fail elim/yet_another_ind.
Abort.

Lemma exo26 d (Hd : odd d) : d.-1./2 = d./2.
Proof.
Abort.

Lemma exo27 d (Hd : ~~ odd d) : (d.-1)./2 = d./2.-1.
Proof.
Abort.


Goal forall n : nat, (n <= 5 \/ 5 < n)%coq_nat.
move=> n.
destruct (Compare_dec.le_gt_dec n 5).
auto.
auto.
Show Proof.
Qed.

Goal forall n : nat, (n <= 5) || (5 < n).
move=> n.
case H : (n <= 5).
done.
move/negbT : H.
rewrite -ltnNge.
move=> ->.
done.
Qed.

Goal forall n : nat, (n <= 5) || (5 < n).
move=> n.
case: (leqP n 5).
done.
done.
Qed.

Definition rgb := sum unit bool.
Definition red : rgb := inl tt.
Definition green : rgb := inr false.
Definition blue : rgb := inr true.

Definition shift (c : rgb) : rgb :=
  match c with
  | inl _ => green
  | inr false => blue
  | inr true => red
  end.

Lemma exo28 c : shift (shift (shift c)) = c.
Proof.
Abort.

CoInductive rgb_spec : rgb -> bool -> bool -> bool -> Prop :=
| red_spec : rgb_spec red true false false
| green_spec : rgb_spec green false true false
| blue_spec : rgb_spec blue false false true.

Lemma exo29 c : rgb_spec c (c == red) (c == green) (c == blue).
Proof.
Admitted.

Lemma exo30 c : shift (shift (shift c)) = c.
Proof.
Abort.