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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
Require Import Setoid CMorphisms.
Parameter A : Type.
Parameter R : A -> A -> Type.
Definition B := Type.
Definition Ri := fun x y => x -> y.
Definition Ra := arrow.
Definition Rb := Basics.arrow.
Definition RBi : B -> B -> Type := fun x y => x -> y.
Definition RBa : B -> B -> Type := arrow.
Definition RBb : B -> B -> Type := Basics.arrow.
Definition RTi : Type -> Type -> Type := fun x y => x -> y.
Definition RTa : Type -> Type -> Type := arrow.
Definition RTb : Type -> Type -> Type := Basics.arrow.
Definition RRBi : crelation B := fun x y => x -> y.
Definition RRBa : crelation B := arrow.
Definition RRBb : crelation B := Basics.arrow.
Definition RRTi : crelation Type := fun x y => x -> y.
Definition RRTa : crelation Type := arrow.
Definition RRTb : crelation Type := Basics.arrow.
Parameter f: A -> B.
#[local] Instance f_Ri: Proper (R ==> Ri) f. Admitted.
#[local] Instance f_Ra: Proper (R ==> Ra) f. Admitted.
#[local] Instance f_Rb: Proper (R ==> Rb) f. Admitted.
#[local] Instance f_RBi: Proper (R ==> RBi) f. Admitted.
#[local] Instance f_RBa: Proper (R ==> RBa) f. Admitted.
#[local] Instance f_RBb: Proper (R ==> RBb) f. Admitted.
#[local] Instance f_RTi: Proper (R ==> RTi) f. Admitted.
#[local] Instance f_RTa: Proper (R ==> RTa) f. Admitted.
#[local] Instance f_RTb: Proper (R ==> RTb) f. Admitted.
#[local] Instance f_RRBi: Proper (R ==> RRBi) f. Admitted.
#[local] Instance f_RRBa: Proper (R ==> RRBa) f. Admitted.
#[local] Instance f_RRBb: Proper (R ==> RRBb) f. Admitted.
#[local] Instance f_RRTi: Proper (R ==> RRTi) f. Admitted.
#[local] Instance f_RRTa: Proper (R ==> RRTa) f. Admitted.
#[local] Instance f_RRTb: Proper (R ==> RRTb) f. Admitted.
Ltac asserts b t :=
match b with
| true => assert_succeeds t
| false => assert_fails t
end.
Ltac test S b1 b2 b3 b4 :=
let Ht := fresh in
assert (forall a b, R a b -> S (f a) (f b)) as Ht;
[ intros a b HR;
asserts b1 ltac:(rewrite HR);
asserts b2 ltac:(rewrite <- HR);
unfold S;
asserts b3 ltac:(rewrite HR);
asserts b4 ltac:(rewrite <- HR);
unfold arrow, Basics.arrow; now rewrite <- HR | clear Ht ].
Goal True.
Proof.
test Ra true true true true.
test Rb false false false false.
test RBa true true true true.
test RBb false false false false.
test RTa true true true true.
test RTb false false false false.
test RRBa true true true true.
test RRBb false false false false.
test RRTa true true true true.
test RRTb false false false false.
apply I.
Qed.
|
