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 Coq.Setoids.Setoid.
Set Implicit Arguments.
Record PartialOrder : Type :=
{ po_car :> Type
; le : po_car -> po_car -> Prop
; monotone : (po_car -> po_car) -> Prop
}.
Notation "x <= y" := (le _ x y).
Section PartialOrder.
Variable X : PartialOrder.
Lemma monotone_def : forall f, monotone X f <-> (forall x y, x <= y -> (f x) <= (f y)).
Admitted.
End PartialOrder.
Set Firstorder Depth 5.
Record SemiLattice : Type :=
{ po :> PartialOrder
; meet : po -> po -> po
}.
Arguments meet [s].
Axiom X : SemiLattice.
Lemma meet_monotone_l : forall a : X, monotone X (fun x => meet x a).
Admitted.
Lemma meet_le_compat : forall w x y z : X, w<=y -> meet w x <= meet y x.
Proof.
intros.
solve [firstorder using meet_monotone_l, monotone_def].
Qed.
|
