1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
Require Import TestSuite.admit.
Require Import Relations Program Setoid Morphisms.
Section S1.
Variable R: nat -> relation bool.
Instance HR1: forall n, Transitive (R n). Admitted.
Instance HR2: forall n, Symmetric (R n). Admitted.
Hypothesis H: forall n a, R n (andb a a) a.
Goal forall n a b, R n b a.
intros.
(* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *)
(* idem with setoid_rewrite *)
(* assert (HR2' := HR2 n). *)
rewrite <- H. (* ok *)
admit.
Qed.
End S1.
Section S2.
Variable R: nat -> relation bool.
Instance HR: forall n, Equivalence (R n). Admitted.
Hypothesis H: forall n a, R n (andb a a) a.
Goal forall n a b, R n a b.
intros. rewrite <- H. admit.
Qed.
End S2.
(* the parametrised relation is required to get the problem *)
Section S3.
Variable R: relation bool.
Instance HR1': Transitive R. Admitted.
Instance HR2': Symmetric R. Admitted.
Hypothesis H: forall a, R (andb a a) a.
Goal forall a b, R b a.
intros.
rewrite <- H. (* ok *)
admit.
Qed.
End S3.
|
