Add handlers and evaluation strategy to theorems about translated properties
MajaRet opened this issue · 0 comments
Description
[WIP]
We should modify how Props are produced from Propertys in two ways:
- A handler is introduced as an additional argument. Handlers should be universally quantified in effect-generic proofs or can be given explicitly to conduct proofs about the semantics of a program in a specific setting (effect stack).
- An evaluation strategy is chosen explicitly. Because strategy-agnostic proofs do not make much sense, an evaluation strategy should always be chosen explicitly when one writes a theorem about a translated property.
Motivation
[WIP]
A QuickCheck property is translated into a function whose return value is a Free Property, where Property is a synonym for Coq's Prop type.
These properties can be transformed into Props by using the quickCheck function on them, which allows us to actually write proofs for them.
Currently, programs are not handled, meaning we prove properties directly about Free values. However, this becomes very limiting when sharing is introduced, as, for example, often two Free values that are not syntactically the same are still semantically equivalent (for some evaluation strategies).
So we should make it possible to reason about handled programs instead of Free values.