blob: 0ac56b3676c30ca5c3753cc4a0dccc4c650de272 (
plain)
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
77
78
|
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps CSE2deps.
Require Import HashedSet.
Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
Definition t := PSet.t.
Definition eq (x : t) (y : t) := x = y.
Lemma eq_refl: forall x, eq x x.
Proof.
unfold eq. trivial.
Qed.
Lemma eq_sym: forall x y, eq x y -> eq y x.
Proof.
unfold eq. congruence.
Qed.
Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
Proof.
unfold eq. congruence.
Qed.
Definition beq (x y : t) := if PSet.eq x y then true else false.
Lemma beq_correct: forall x y, beq x y = true -> eq x y.
Proof.
unfold beq.
intros.
destruct PSet.eq; congruence.
Qed.
Definition ge (x y : t) := (PSet.is_subset x y) = true.
Lemma ge_refl: forall x y, eq x y -> ge x y.
Proof.
unfold eq, ge.
intros.
subst y.
apply PSet.is_subset_spec.
trivial.
Qed.
Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
Proof.
unfold ge.
intros.
rewrite PSet.is_subset_spec in *.
intuition.
Qed.
Definition lub := PSet.inter.
Lemma ge_lub_left: forall x y, ge (lub x y) x.
Proof.
unfold ge, lub.
intros.
apply PSet.is_subset_spec.
intro.
rewrite PSet.ginter.
rewrite andb_true_iff.
intuition.
Qed.
Lemma ge_lub_right: forall x y, ge (lub x y) y.
Proof.
unfold ge, lub.
intros.
apply PSet.is_subset_spec.
intro.
rewrite PSet.ginter.
rewrite andb_true_iff.
intuition.
Qed.
End RELATION.
Definition totoro := RELATION.lub.
|
