From elpi Require Import elpi.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

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

(** # This is the <a href="https://math-comp.github.io/htmldoc_2_0_alpha1/mathcomp.ssreflect.seq.html">doc of seq</a>, use it! #*)

(**

----
Exercise 1: 
    - look up the documentation of [take] and [drop]
    - prove this by induction (mind the recursive argument)
*)
Lemma cat_take_drop T n (s : seq T) : take n s ++ drop n s = s.
Proof.
(*D*)by elim: s n => [|x s IHs] [|n] //=; rewrite IHs.
(*A*)Qed.

(** Exercise 2:
   - look at the definition of [take] and [size] and prove the following lemma
   - the proof goes by cases (recall the spec lemma [leqP])
*)
Lemma size_take T n (s : seq T) :
  size (take n s) = if n < size s then n else size s.
Proof.
(*D*)have [le_sn | lt_ns] := leqP (size s) n; first by rewrite take_oversize.
(*D*)by rewrite size_takel // ltnW.
(*A*)Qed.

(** Exercise 3:
    - another proof by cases 
    - remark that also [eqP] is a spec lemma
*)
Lemma takel_cat T n (s1 s2 : seq T) :
  n <= size s1 -> take n (s1 ++ s2) = take n s1.
Proof.
(*D*)move=> Hn; rewrite take_cat ltn_neqAle Hn andbT.
(*D*)by case: eqP => //= ->; rewrite subnn take0 cats0 take_size.
(*A*)Qed.

(** Exercise 4:
    - Look up the definition of [rot]
    - Look back in this file the lemma [cat_take_drop] 
    - can you rewrite with it right-to-left in the right-hand-side of the goal? 
*)
Lemma size_rot T n (s : seq T) : size (rot n s) = size s.
Proof.
(*D*)by rewrite -[s in RHS](cat_take_drop n) /rot !size_cat addnC.
(*A*)Qed.

(** Exercise 5:
    - which is the size of an empty sequence?
    - Use lemmas about [size] and [filter] 
*)
Lemma has_filter (T : eqType) a (s : seq T)  : has a s = (filter a s != [::]).
Proof.
(*D*)by rewrite -size_eq0 size_filter has_count lt0n.
(*A*)Qed.

(** Exercise 6:
    - prove that by induction 
*)
Lemma filter_all T a (s : seq T) : all a (filter a s).
Proof. 
(*D*)by elim: s => //= x s IHs; case: ifP => //= ->. 
(*A*)Qed.

(** Exercise 7:
  - prove that view (one branch is by induction) 
*)
Lemma all_filterP T a (s : seq T) :
  reflect (filter a s = s) (all a s).
Proof.
(*D*)apply: (iffP idP) => [| <-]; last exact: filter_all.
(*D*)by elim: s => //= x s IHs /andP[-> Hs]; rewrite IHs.
(*A*)Qed.

(** Exercise 9:
    - prove this by induction on [s] 
*)
Lemma allP (T : eqType) (a : pred T) (s : seq T) :
  reflect (forall x, x \in s -> a x) (all a s).
Proof.
(*D*)elim: s => [|x s IHs] /=; first by exact: ReflectT.
(*D*)rewrite andbC; case: IHs => IHs /=.
(*D*)  apply: (iffP idP) => [Hx y|].
(*D*)    by rewrite inE => /orP[ /eqP-> // | /IHs ].
(*D*)  by move=> /(_ x); apply; rewrite inE eqxx.
(*D*)by apply: ReflectF=> H; apply: IHs => y Hy; apply H; rewrite inE orbC Hy.
(*A*)Qed.

(** *** Exercise 10:
  - check out the definitions and theory of [leq] and [maxn]
  - use only [rewrite] and [apply]
  - proof sketch:
<<
   n <= m = n - m == 0
          = m + n - m == m + 0
          = maxn m n == m
>> *)
Lemma maxn_idPl m n : reflect (maxn m n = m) (m >= n).
(*D*)Proof. by rewrite -subn_eq0 -(eqn_add2l m) addn0 -maxnE; apply: eqP. Qed.