Skip to content

Instantly share code, notes, and snippets.

@llelf
Last active May 16, 2020 21:21
Show Gist options
  • Save llelf/b4e74ce5074b4144db7f6cfa4cdce401 to your computer and use it in GitHub Desktop.
Save llelf/b4e74ce5074b4144db7f6cfa4cdce401 to your computer and use it in GitHub Desktop.
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) *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment