← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/lattice/SemiLattice.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/lattice/SemiLattice.agda
1
 
 
2
 
module SemiLattice where
3
 
 
4
 
open import Prelude
5
 
open import PartialOrder as PO
6
 
import Chain
7
 
 
8
 
private
9
 
 module IsSemiLat
10
 
   {A : Set}(po : PartialOrder A)(_⊓_ : A -> A -> A) where
11
 
  private open module PO = PartialOrder po
12
 
 
13
 
  record IsSemiLattice : Set where
14
 
    field
15
 
      ⊓-lbL : forall {x y}   -> (x ⊓ y) ≤ x
16
 
      ⊓-lbR : forall {x y}   -> (x ⊓ y) ≤ y
17
 
      ⊓-glb : forall {x y z} -> z ≤ x -> z ≤ y -> z ≤ (x ⊓ y)
18
 
 
19
 
open IsSemiLat public
20
 
 
21
 
record SemiLattice (A : Set) : Set1 where
22
 
  field
23
 
    po  : PartialOrder A
24
 
    _⊓_ : A -> A -> A
25
 
    prf : IsSemiLattice po _⊓_
26
 
 
27
 
module SemiLat {A : Set}(L : SemiLattice A) where
28
 
 
29
 
  private module SL   = SemiLattice L
30
 
  private module SLPO = POrder SL.po
31
 
  private module IsSL = IsSemiLattice SL.po SL._⊓_ SL.prf
32
 
 
33
 
  open SLPO public
34
 
  open SL   public hiding (prf)
35
 
  open IsSL public
36
 
 
37
 
  private open module C≤ = Chain _≤_ (\x -> ≤-refl) (\x y z -> ≤-trans)
38
 
                      renaming (_===_ to _-≤-_; chain>_ to trans>_)
39
 
 
40
 
  ⊓-commute : forall {x y} -> (x ⊓ y) == (y ⊓ x)
41
 
  ⊓-commute = ≤-antisym lem lem
42
 
    where
43
 
      lem : forall {x y} -> (x ⊓ y) ≤ (y ⊓ x)
44
 
      lem = ⊓-glb ⊓-lbR ⊓-lbL
45
 
 
46
 
  ⊓-assoc : forall {x y z} -> (x ⊓ (y ⊓ z)) == ((x ⊓ y) ⊓ z)
47
 
  ⊓-assoc = ≤-antisym lem₁ lem₂
48
 
    where
49
 
      lem₁ : forall {x y z} -> (x ⊓ (y ⊓ z)) ≤ ((x ⊓ y) ⊓ z)
50
 
      lem₁ = ⊓-glb (⊓-glb ⊓-lbL (≤-trans ⊓-lbR ⊓-lbL))
51
 
                   (≤-trans ⊓-lbR ⊓-lbR)
52
 
 
53
 
      lem₂ : forall {x y z} ->  ((x ⊓ y) ⊓ z) ≤ (x ⊓ (y ⊓ z))
54
 
      lem₂ = ⊓-glb (≤-trans ⊓-lbL ⊓-lbL)
55
 
                   (⊓-glb (≤-trans ⊓-lbL ⊓-lbR) ⊓-lbR)
56
 
 
57
 
  ⊓-idem : forall {x} -> (x ⊓ x) == x
58
 
  ⊓-idem = ≤-antisym ⊓-lbL (⊓-glb ≤-refl ≤-refl)
59
 
 
60
 
  ≤⊓-L : forall {x y} -> (x ≤ y) ⇐⇒ ((x ⊓ y) == x)
61
 
  ≤⊓-L = (fwd , bwd)
62
 
    where
63
 
      fwd = \x≤y -> ≤-antisym ⊓-lbL (⊓-glb ≤-refl x≤y)
64
 
      bwd = \x⊓y=x -> ≤-trans (==≤-R x⊓y=x) ⊓-lbR
65
 
 
66
 
  ≤⊓-R : forall {x y} -> (y ≤ x) ⇐⇒ ((x ⊓ y) == y)
67
 
  ≤⊓-R {x}{y} = (fwd , bwd)
68
 
    where
69
 
      lem : (y ≤ x) ⇐⇒ ((y ⊓ x) == y)
70
 
      lem = ≤⊓-L
71
 
 
72
 
      fwd = \y≤x -> ==-trans ⊓-commute (fst lem y≤x)
73
 
      bwd = \x⊓y=y -> snd lem (==-trans ⊓-commute x⊓y=y)
74
 
 
75
 
  ⊓-monotone-R : forall {a} -> Monotone (\x -> a ⊓ x)
76
 
  ⊓-monotone-R x≤y = ⊓-glb ⊓-lbL (≤-trans ⊓-lbR x≤y)
77
 
 
78
 
  ⊓-monotone-L : forall {a} -> Monotone (\x -> x ⊓ a)
79
 
  ⊓-monotone-L {a}{x}{y} x≤y = 
80
 
    trans> x ⊓ a
81
 
       -≤- a ⊓ x  by ==≤-L ⊓-commute
82
 
       -≤- a ⊓ y  by ⊓-monotone-R x≤y
83
 
       -≤- y ⊓ a  by ==≤-L ⊓-commute
84
 
 
85
 
  ≤⊓-compat : forall {w x y z} -> w ≤ y -> x ≤ z -> (w ⊓ x) ≤ (y ⊓ z)
86
 
  ≤⊓-compat {w}{x}{y}{z} w≤y x≤z =
87
 
    trans> w ⊓ x
88
 
       -≤- w ⊓ z  by ⊓-monotone-R x≤z
89
 
       -≤- y ⊓ z  by ⊓-monotone-L w≤y
90
 
 
91
 
  ⊓-cong : forall {w x y z} -> w == y -> x == z -> (w ⊓ x) == (y ⊓ z)
92
 
  ⊓-cong wy xz = ≤-antisym (≤⊓-compat (==≤-L wy) (==≤-L xz))
93
 
                           (≤⊓-compat (==≤-R wy) (==≤-R xz))
94
 
 
95
 
  ⊓-cong-L : forall {x y z} -> x == y -> (x ⊓ z) == (y ⊓ z)
96
 
  ⊓-cong-L xy = ⊓-cong xy ==-refl 
97
 
 
98
 
  ⊓-cong-R : forall {x y z} -> x == y -> (z ⊓ x) == (z ⊓ y)
99
 
  ⊓-cong-R xy = ⊓-cong ==-refl xy