forked from vafeiadis/hahn
-
Notifications
You must be signed in to change notification settings - Fork 0
/
HahnFuneq.v
76 lines (55 loc) · 2.36 KB
/
HahnFuneq.v
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
74
75
76
Require Import HahnBase HahnRelationsBasic.
Require Import Setoid.
Set Implicit Arguments.
Section FunEq.
Variable A B : Type.
Variable f : A -> B.
Definition funeq (r : relation A) := forall a b (H: r a b), f a = f b.
Lemma funeq_union r t (H1: funeq r) (H2: funeq t) : funeq (r ∪ t).
Proof. firstorder. Qed.
Lemma funeq_inter_l r t (H1: funeq r) : funeq (r ∩ t).
Proof. firstorder. Qed.
Lemma funeq_inter_r r t (H1: funeq t) : funeq (r ∩ t).
Proof. firstorder. Qed.
Lemma funeq_seq r t (H1: funeq r) (H2: funeq t) : funeq (r ⨾ t).
Proof. eby red; ins; destruct H; desc; etransitivity; [apply H1 | apply H2]. Qed.
Lemma funeq_ct r (H: funeq r) : funeq r⁺.
Proof. eby red; ins; induction H0; eauto; etransitivity. Qed.
Lemma funeq_cr r (H: funeq r) : funeq r^?.
Proof. red; ins; red in H0; desf; subst; auto. Qed.
Lemma funeq_rt r (H: funeq r) : funeq r＊.
Proof. eby red; ins; induction H0; eauto; etransitivity. Qed.
Lemma funeq_restr r (H: funeq r) dom : funeq (restr_rel dom r).
Proof. firstorder. Qed.
Lemma funeq_restr_eq r (H: funeq r) C (dom : A -> C) : funeq (restr_eq_rel dom r).
Proof. firstorder. Qed.
Lemma funeq_restr_eq_rel r : funeq (restr_eq_rel f r).
Proof. firstorder. Qed.
Lemma funeq_eqv_rel dom : funeq ⦗dom⦘.
Proof. by red; ins; red in H; desc; subst. Qed.
Lemma funeq_transp r (H: funeq r) : funeq r⁻¹.
Proof. firstorder. Qed.
Lemma funeq_minus r t (H: funeq r) : funeq (r \ t).
Proof. firstorder. Qed.
Lemma funeq_irreflexive r t (H: funeq r)
(IRR: irreflexive (restr_eq_rel f t ⨾ r)) : irreflexive (t ⨾ r).
Proof.
unfold funeq, irreflexive, seq, restr_eq_rel in *.
ins; desf; eauto 8 using eq_sym.
Qed.
End FunEq.
Global Hint Unfold funeq : unfolderDb.
Global Hint Resolve funeq_union funeq_inter_l funeq_inter_r : hahn.
Global Hint Resolve funeq_seq funeq_ct funeq_cr funeq_rt : hahn.
Global Hint Resolve funeq_restr funeq_restr_eq funeq_restr_eq_rel : hahn.
Global Hint Resolve funeq_eqv_rel funeq_transp funeq_minus : hahn.
Add Parametric Morphism A B f : (@funeq A B f) with signature
inclusion --> Basics.impl as funeq_mori.
Proof.
unfold inclusion, funeq, Basics.impl; eauto.
Qed.
Add Parametric Morphism A B f : (@funeq A B f) with signature
same_relation ==> iff as funeq_more.
Proof.
unfold same_relation; split; desc; [rewrite H0|rewrite H]; eauto.
Qed.