program+qc.v

From QuickChick Require Import QuickChick.
From Coq        Require Import Program.
From mathcomp   Require Import ssreflect ssrfun ssrnat ssrbool eqtype seq.

Program Fixpoint itakep {A} (n:nat) (s:seq A) {measure n} : seq A :=
  if s isn't [::] then
    (if n <= size s as r return (n <= size s = r -> _)
       then fun pf => take n s
       else fun pf => s ++ itakep (n - size s) s) erefl
  else [::].
Next Obligation.
apply/ltP. move:H pf. case:s=>//=a l _. rewrite ltn_subrL. by case:n itakep.
Defined.

Definition size_itakep {A} n (s:seq A) := size (itakep n s) == n.
Compute size_itakep 1 [::].  (* false *)
QuickChick size_itakep.      (* Passed 10000 tests (0 discards) *)