我对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
转发上下文,或者是否有解决此问题的方法?
发布于 2019-06-11 03:01:17
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.
https://stackoverflow.com/questions/56531445
复制相似问题