QuickChick переадресация контекста - PullRequest
Новая
       11

QuickChick переадресация контекста

0 голосов
/ 10 июня 2019

У меня проблема с платформой тестирования QuickChick.Предположим, у меня есть такой тип: 

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

и две такие функции: 

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 _))).

Когда я хочу доказать отсутствие объекта доказательства, у меня есть этот контекст: 

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

Проблема в том, что при использовании bindGen я теряю контекст из-за того, что мне нужно доказать текущую цель.

Итак, вопрос в том, как переадресовать контекст, используя bindGen, или есть ли обходные пути для решения этой проблемы?

1 Ответ

3 голосов
/ 10 июня 2019

Существует bindGen' комбинатор : 

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