blob: aaf35bc210963850ad4430930a8219726f8d87f0 (
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
|
{-# OPTIONS --safe #-}
module Problem2 (T : Set) where
open import Data.List
open import Data.Nat
open import Data.Product
Relation = T → T → Set
Commutes : Relation → Relation → Set
Commutes R1 R2 = ∀{x y z} → R1 x y → R2 x z → ∃[ t ] (R2 y t × R1 z t)
Diamond : Relation → Set
Diamond R = Commutes R R
data Star (R : Relation) : Relation where
rule : ∀{x y} → R x y → Star R x y
refl : ∀{x} → Star R x x
trans : ∀{x y z} → Star R x y → Star R y z → Star R x z
-- We prove by induction on the transitive closure proof rs. The three cases
-- are given diagrammatically:
--
-- rs = rule r′
-- We have the following diagram by assumption.
-- x - r′ → y
-- | |
-- r s
-- ↓ ↓
-- z - s′ → t
--
-- rs = refl
-- The diagram commutes.
-- x == x
-- | |
-- r r
-- ↓ ↓
-- z == z
--
-- rs = trans rs₁ rs₂
-- The diagram commutes, with each square derived by induction.
-- x - rs₁ → y₁ - rs₂ → y₂
-- | | |
-- r s₁ s₂
-- ↓ ↓ ↓
-- z - ss₁ → t₁ - ss₂ → t₂
strip : ∀{R} → Diamond R → Commutes (Star R) R
strip commutes (rule r′) r =
let (t , s , s′) = commutes r′ r in
t , s , rule s′
strip commutes refl r = -, r , refl
strip commutes (trans rs₁ rs₂) r =
let (t₁ , s₁ , ss₁) = strip commutes rs₁ r in
let (t₂ , s₂ , ss₂) = strip commutes rs₂ s₁ in
t₂ , s₂ , trans ss₁ ss₂
|
