Testing Delay.v

Tests

Reflexivity

Setoid rewriting

There is an issue with the following.

Monotonicity tactics

Basic sanity check. This has actually failed in the past due to context_candidate being too liberal and selecting the RB property instead of RA, then going nowhere with that with no backtracking implemented yet.

Check that we can use relational hypotheses from the context as well as Monotonic/Related instances.

Bug with relational parametricity: you can't RElim a relation you don't know yet.

Pattern matching

rel_curry

If we can deduce some terms are equal, we should be able to rewrite them under any context. However right now this can only be done by declaring the f_equal_relim hint. Maybe a good solution for this might even go further: abstract the common context and use eq_rect if it's possible to prove equality between the variant parts.

Hypotheses from the context

This used to fail because the flipped hypothesis would not be identified as a candidate. This is important because the constraints generated by the setoid rewriting system often have this form.

Then *this* used to fail because the flip was hidden until after we exploit the subrel property. This is important in particular when using the equivalences for a given partial order, as in eqrel vs. subrel, where we want to be able to use equivalences in both directions.

As an example where proper handling of flip is important, this is a goal generated by setoid_rewrite when we try to rewrite using eqrel under option_le. Here, both R1 and R2 have to be instantiated as flip eq (so that the associated hypotheses can be used to solve goals of the form yi = xi), and similarly we need to use the super-relation flip subrel of eqrel.

impl vs. subrel

This checks that a relational property written in terms of subrel can be used to solve a goal stated in terms of impl. This is made possible by subrel_impl_relim.

Generic rules

The coreflexivity of rel_prod and eq makes it possible for pair_rel to behave in the same way as f_equal below, since they allow us to deduce that eq × eq is a subrel of eq.

Using foo_subrel instances

Still broken because of the interaction between subrel and - ==> - ==> impl (or lack thereof)

The rgraph tactic

General issues

Assumptions can be used by Monotonicity to solve the goal. However, consider the goal ?R f g |- (- ==> S) f g. Monotonicity can solve this by instantiating R and using the hypothesis, however RIntro will take precedence in this case. This means we will end up with a goal ?R f g, x |- S (f x) (g x) that cannot be solved anymore. When ?R is already - ==> S or some equivalent relation, this is not a problem, because the work done by RIntro can essentially be undone later by Monotonicity. However when ?R is an existential variable this is not true and we would prefer an earlier instantiation. This is a possible workaround: < Lemma assumption_rstep {P : Prop} : P -> RStep True P. Proof. firstorder. Qed. Global Hint Extern 1 (RStep _ (_ ?x ?y)) => lazymatch goal with H : ?R x y |- _ => is_evar R; eexact (assumption_rstep H) end : typeclass_instances. >>>

The transport tactic

Tests for specific relators

list_rel

list_subrel use to not work because of a missing Params declaration.

rel_pull

The RIntro instance for rel_pull used to be less general.

We don't want the introduction rule for rel_pull to shadow relational properties.

rel_all

rel_ex

rel_top

We used to only have an RIntro instance for ⊤%rel, which is enough for proving all goals of the form ⊤%rel x y but not enough to derive properties of relations in which ⊤%rel is a component.