algebra.v 863 Bytes
Newer Older
1
2
From iris.base_logic.lib Require Import invariants.

Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
3
4
Instance test_cofe: Cofe (iPreProp Σ) := _.

5
Section tests.
6
  Context `{!invG Σ}.
7
8
9
10
11
12

  Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
    λne P v, ( (P v))%I.
  Solve Obligations with solve_proper.

End tests.
13
14
15
16
17
18
19
20
21
22

(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
    Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
    we cannot [1].  So at least we try to make sure the first solution found
    is the right one, to not pay performance in the success case [2].

    [1] https://github.com/coq/coq/issues/7916
    [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
Robbert Krebbers's avatar
Robbert Krebbers committed
23
   R, @Reflexive Prop R  R = iff.
24
25
26
27
28
Proof.
  eexists. split.
  - apply _.
  - reflexivity.
Qed.