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
41
42
|
Require Import Setoid.
Require Import Coq.Classes.CRelationClasses.
Require Import Coq.Classes.CMorphisms.
Parameter B C : Type.
Parameter P : Type -> Type -> Type.
(* This is used for rewrites for lem_P and lem_P_iffT. *)
#[export] Instance P_Proper : Proper (iffT ==> iffT ==> iffT) (P).
Admitted.
Lemma lem_P : forall A, iffT A B -> P A C -> P B C.
Proof.
intros A H1 H2.
rewrite H1 in H2. (* Comment out iffT_P_Proper to see this fail. *)
Abort.
Lemma lem_P_iffT : forall A, iffT A B -> P A C -> iffT B C.
Proof.
intros A H1 H2.
setoid_rewrite H1 in H2. (* Comment out iffT_P_Proper to see this fail. *)
Abort.
(* Trying to do the same with iffT instead of P. *)
#[export] Instance iffT_Proper : Proper (iffT ==> iffT ==> iffT) iffT.
Admitted.
(* Just in case? *)
#[export] Instance arrow_Proper : Proper (iffT ==> iffT ==> iffT ) (arrow).
Admitted.
Lemma lem_iffT_P : forall A, iffT A B -> iffT A C -> P B C.
Proof.
intros A H1 H2.
rewrite H1 in H2.
Abort.
Lemma lem_iffT : forall A, iffT A B -> iffT A C -> iffT B C.
Proof.
intros A H1 H2.
setoid_rewrite H1 in H2.
Abort.
|
