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 |              *)
(*******************************************************************)




(*******************************************************************)
(* 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)) *)
(*******************************************************************)






(********************************************************************)
(* 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.        *) 
(********************************************************************)




(********************************************************************)
(* Show that if a sequence has exactly two elements in particular   *)
(* it has at least two.                                             *)
(********************************************************************)


(********************************************************************)
(* Show that if one of a two sequences of a concatenation has at    *)
(* least two elements so is the concatenation                       *)
(********************************************************************)


(********************************************************************)
(* Show that the reverse of a sequence l has at least two elements  *)
(* if and only if l has also at least two elements                  *)
(********************************************************************)




(********************************************************************)
(* 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                                       *)
(********************************************************************)




(********************************************************************)
(* 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                                        *)
(********************************************************************)