Search code examples
coq

QuickChick context forwarding

I have a problem with QuickChick testing framework. Suppose I have a type like this:

Inductive f := f1 (x : Z) (range : x < 20 /\ 0 < x).

And two functions like this:

Definition boundaries' (t : bool) :=
  if t 
  then (1, 10)%Z 
  else (10, 19)%Z .

Program Definition binary_gen (t : G bool) : G (f) :=
  bindGen ((fmap boundaries') t) (fun '(m_min, m_max) =>
    bindGen (choose (m_min, m_max)) (fun (x : Z) =>
        returnGen (f1 x _))).

When I want to prove missing proof object I have this context:

t : G bool
z, z0, x : Z
============================
x < 20 /\ 0 < x

The problem is that when using bindGen I loose context from before that I need to prove current goal.

So the question is, how to forward context using bindGen or are there any workarounds around this problem?

Solution

  • There is a bindGen' combinator:

    Definition bindGen' : forall {A B : Type} (g : G A), 
                       (forall (a : A), (a \in semGen g) -> G B) -> G B.