Require Import ssreflect ssrbool ssrfun ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(*******************************************************************)
(* Redefine your own version of boolean connectives trying to      *)
(* minimise the number of if then else expressions.                *)
(*   x      y    negb    andb   orb    implb  xorb                 *)
(* true | true | false | true | true | true | false |              *)
(* true | false| false | false| true | false| true  |              *)
(* false| true | true  | false| true | true | true  |              *)
(* false| false| true  | false| false| true | false |              *)
(*******************************************************************)

Definition negb x := if x then false else true.
Definition andb x y := if x then y else false.
Definition orb x y := if x then true else y.
Definition implb x y := if x then y else true.
Definition xorb x y := if x then negb y else y.

(*******************************************************************)
(* Prove the following equalities trying to minimise the number of *)
(* applications of case:                                           *)
(* andbA : forall x y z, andb x (andb y z) = andb (andb x y) z     *)
(* andb_orr :                                                      *)
(*    forall x y z, andb x (orb y z) = orb (andb x y) (andb x z)   *)
(* impbE : forall x y, implb x y = orb (negb x) y                  *)
(* xorbE : forall x y, xorb x y = andb (orb x y) (negb (andb x y)) *)
(*******************************************************************)
Lemma andbA : forall x y z, andb x (andb y z) = andb (andb x y) z.
Proof. by move=> x y z; case: x; case: y. Qed.

Lemma andb_orr : forall x y z, andb x (orb y z) = orb (andb x y) (andb x z).
Proof. by move=> x y z; case: x; case: y. Qed.

Lemma impbE : forall x y, implb x y = orb (negb x) y.
Proof. by move=> x y; case: x. Qed.

Lemma xorbE : forall x y, xorb x y = andb (orb x y) (negb (andb x y)).
Proof. by move=> x y; case: x; case: y. Qed.


(********************************************************************)
(* Define the two predicates at_least_two and exactly_two that      *)
(* check that a sequence has at least two and exactly two elements. *)
(* Test on some examples that these definitions are correct.        *) 
(********************************************************************)
Definition at_least_two (A : Type) (l : seq A) :=
  if l is _ :: _ :: _ then true else false.

Definition exactly_two (A : Type) (l : seq A) :=
  if l is [:: _; _] then true else false.

Lemma ex1 : exactly_two [:: 1] = false.
Proof. by apply: erefl. Qed.

Lemma at1 : at_least_two [:: 1] = false.
Proof. by apply: erefl. Qed.

Lemma ex2 : exactly_two [:: 1; 2] = true.
Proof. by apply: erefl. Qed.

Lemma at2 : at_least_two [:: 1; 2] = true.
Proof. by apply: erefl. Qed.

Lemma ex3 : exactly_two [:: 1; 2; 3] = false.
Proof. by apply: erefl. Qed.

(********************************************************************)
(* Show that if a sequence has exactly two elements in particular   *)
(* it has at least two.                                             *)
(********************************************************************)
Lemma exactly_two_at_least_two (A : Type) (l : seq A) : 
  exactly_two l -> at_least_two l.
Proof. by move: l; case; rewrite //=; move=> a; case. Qed.

(********************************************************************)
(* Show that if one of a two sequences of a concatenation has at    *)
(* least two elements so is the concatenation                       *)
(********************************************************************)
Lemma at_least_two_appl (A : Type) (l1 l2 : seq A) : 
  at_least_two l1 -> at_least_two (l1 ++ l2).
Proof. by move: l1; case; rewrite //=; move=> a; case. Qed.

Lemma at_least_two_appr (A : Type) (l1 l2 : seq A) : 
  at_least_two l2 -> at_least_two (l1 ++ l2).
Proof.
move: l1; case; rewrite //=; move=> a; case; rewrite //=.
move: l2; case; rewrite //=.
Qed.

(********************************************************************)
(* Show that the reverse of a sequence l has at least two elements  *)
(* if and only if l has also at least two elements                  *)
(********************************************************************)
Lemma at_least_two_rcons (A : Type) a b (l : seq A) : 
  at_least_two (rcons (rcons l a) b).
Proof. by move: l; case => // a1; case. Qed.

Lemma at_least_two_rev (A : Type) (l : seq A) : 
  at_least_two l = at_least_two (rev l).
Proof.  
move: l; case; rewrite //=; move=> a; case; rewrite //=.
by move=> b l; rewrite !rev_cons at_least_two_rcons.
Qed.

(********************************************************************)
(* Using a fixpoint generalize the predicate at_least_two to a      *)
(* at_least, such that at_least n l indicates that l has at least n *)
(* elements and prove the corresponding properties about            *)
(* concatenation  and reverse                                       *)
(********************************************************************)
Fixpoint at_least n (A : Type) (l : seq A) :=
  if n is n1.+1 then
     if l is _ :: l1 then at_least n1 l1 else false
  else true.

Lemma at_least_appl n (A : Type) (l1 l2 : seq A) : 
  at_least n l1 -> at_least n (l1 ++ l2).
Proof. 
by move: n l1; elim; rewrite //; move=> n IH; case.
Qed.

Lemma at_least_cons n (A : Type) (a : A) l : 
  at_least n l -> at_least n (a :: l).
Proof.
by move: n a l; elim; rewrite //= ; move=> n IH a; case.
Qed.

Lemma at_least_appr n (A : Type) (l1 l2 : seq A) : 
  at_least n l2 -> at_least n (l1 ++ l2).
Proof.
move: n l1 l2; elim; rewrite //; move=> n IH; case; rewrite //.
move=> a l1; case; rewrite //; move=> b l2.
rewrite /=; move=> HH.
by apply: IH (at_least_cons _ _).
Qed.

(********************************************************************)
(* Propose a more direct definition of at_least (at_leastn) that    *)
(* uses the comparison between integers and the size of a sequence  *)
(* prove the equivalence and give alternatives proofs for the       *)
(* concatenation and reverse                                        *)
(********************************************************************)
Definition at_leastn n (A : Type) (l : seq A) := n <= size l.

Lemma at_least_at_leastn n A (l : seq A) :
  at_least n l = at_leastn n l.
Proof.
move: n l; elim.
case; rewrite //=.
move=> a IH; case; rewrite //=.
Qed.

Lemma at_leastn_appl n (A : Type) (l1 l2 : seq A) : 
  at_leastn n l1 -> at_leastn n (l1 ++ l2).
Proof.
rewrite /at_leastn size_cat => /leq_trans; apply.
exact: leq_addr.
Qed.

Lemma at_leastn_appr n (A : Type) (l1 l2 : seq A) : 
  at_leastn n l2 -> at_leastn n (l1 ++ l2).
Proof.
rewrite /at_leastn size_cat => /leq_trans; apply.
exact: leq_addl.
Qed.

Lemma at_leastn_rev n (A : Type) (l : seq A) : 
  at_leastn n l = at_leastn n (rev l).
Proof.  by rewrite /at_leastn size_rev. Qed.