blob: e71dcb9ee24ca1fb9dac4ac125598d4e8b39a0db (
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
{-# OPTIONS --safe #-}
module Problem18 (Symbol : Set) where
open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Data.Product
open ≡-Reasoning
variable n m a b c d : ℕ
data Patch : ℕ → ℕ → Set where
end : Patch 0 0
skp : Patch n m → Patch (suc n) (suc m)
del : Patch n m → Patch (suc n) m
ins : Symbol → Patch n m → Patch n (suc m)
apply : Patch n m → Vec Symbol n → Vec Symbol m
apply end [] = []
apply (ins x p) xs = x ∷ apply p xs
apply (skp p) (x ∷ xs) = x ∷ apply p xs
apply (del p) (x ∷ xs) = apply p xs
infixl 50 _·_
_·_ : Patch a b → Patch b c → Patch a c
end · p₂ = p₂
skp p₁ · skp p₂ = skp (p₁ · p₂)
skp p₁ · del p₂ = del (p₁ · p₂)
skp p₁ · ins x p₂ = ins x (skp p₁ · p₂)
ins x p₁ · ins x₂ p₂ = ins x₂ (ins x p₁ · p₂)
del p₁ · ins x₂ p₂ = ins x₂ (del p₁ · p₂)
del p₁ · p₂ = del (p₁ · p₂)
ins x p₁ · skp p₂ = ins x (p₁ · p₂)
ins x p₁ · del p₂ = p₁ · p₂
_≈_ : (x y : Patch a b) → Set
x ≈ y = ∀ d → apply x d ≡ apply y d
compose-correct : ∀ (p₁ : Patch a b) (p₂ : Patch b c) (d : Vec Symbol a)
→ apply (p₁ · p₂) d ≡ apply p₂ (apply p₁ d)
compose-correct end p₂ [] = refl
compose-correct (skp p₁) (skp p₂) (x ∷ d) = cong (x ∷_) (compose-correct p₁ p₂ d)
compose-correct (skp p₁) (del p₂) (x ∷ d) = compose-correct p₁ p₂ d
compose-correct (skp p₁) (ins y p₂) (x ∷ d) = cong (y ∷_) (compose-correct (skp p₁) p₂ (x ∷ d))
compose-correct (del p₁) end (x ∷ d) = compose-correct p₁ end d
compose-correct (del p₁) (skp p₂) (x ∷ d) = compose-correct p₁ (skp p₂) d
compose-correct (del p₁) (del p₂) (x ∷ d) = compose-correct p₁ (del p₂) d
compose-correct (del p₁) (ins y p₂) (x ∷ d) = cong (y ∷_) (compose-correct (del p₁) p₂ (x ∷ d))
compose-correct (ins y p₁) (skp p₂) d = cong (y ∷_) (compose-correct p₁ p₂ d)
compose-correct (ins y p₁) (del p₂) d = compose-correct p₁ p₂ d
compose-correct (ins y p₁) (ins z p₂) d = cong (z ∷_) (compose-correct (ins y p₁) p₂ d)
compose-assoc : ∀ (p₁ : Patch a b) (p₂ : Patch b c) (p₃ : Patch c d)
→ (p₁ · p₂) · p₃ ≈ p₁ · (p₂ · p₃)
compose-assoc p₁ p₂ p₃ d = begin
apply (p₁ · p₂ · p₃) d ≡⟨ compose-correct (p₁ · p₂) p₃ d ⟩
apply p₃ (apply (p₁ · p₂) d) ≡⟨ cong (apply p₃) (compose-correct p₁ p₂ d) ⟩
apply p₃ (apply p₂ (apply p₁ d)) ≡˘⟨ compose-correct p₂ p₃ (apply p₁ d) ⟩
apply (p₂ · p₃) (apply p₁ d) ≡˘⟨ compose-correct p₁ (p₂ · p₃) d ⟩
apply (p₁ · (p₂ · p₃)) d ∎
record Merge (p₁ : Patch a b)(p₂ : Patch a c) : Set where
constructor M
field size : ℕ
field p₁′ : Patch b size
field p₂′ : Patch c size
merge : ∀(p₁ : Patch a b)(p₂ : Patch a c) → Merge p₁ p₂
merge end end = M 0 end end
merge p₁ (ins x p₂) = let m = merge p₁ p₂ in M (suc (Merge.size m)) (ins x (Merge.p₁′ m)) (skp (Merge.p₂′ m))
merge (ins x p₁) p₂ = let m = merge p₁ p₂ in M (suc (Merge.size m)) (skp (Merge.p₁′ m)) (ins x (Merge.p₂′ m))
merge (del p₁) (skp p₂) = let m = merge p₁ p₂ in M (Merge.size m) (Merge.p₁′ m) (del (Merge.p₂′ m))
merge (skp p₁) (del p₂) = let m = merge p₁ p₂ in M (Merge.size m) (del (Merge.p₁′ m)) (Merge.p₂′ m)
merge (del p₁) (del p₂) = let m = merge p₁ p₂ in M (Merge.size m) (Merge.p₁′ m) (Merge.p₂′ m)
merge (skp p₁) (skp p₂) = let m = merge p₁ p₂ in M (suc (Merge.size m)) (skp (Merge.p₁′ m)) (skp (Merge.p₂′ m))
merge-pushout :
(p₁ : Patch a b) (p₂ : Patch a c) →
p₁ · Merge.p₁′ (merge p₁ p₂) ≈ p₂ · Merge.p₂′ (merge p₁ p₂)
merge-pushout end end d = refl
merge-pushout end (ins z p₂) d = cong (z ∷_) (merge-pushout end p₂ d)
merge-pushout (skp p₁) (skp p₂) (x ∷ d) = cong (x ∷_) (merge-pushout p₁ p₂ d)
merge-pushout (skp p₁) (del p₂) (x ∷ d) = begin
apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d ≡⟨ merge-pushout p₁ p₂ d ⟩
apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d ≡⟨ compose-correct p₂ (Merge.p₂′ (merge p₁ p₂)) d ⟩
apply (Merge.p₂′ (merge p₁ p₂)) (apply p₂ d) ≡⟨⟩
apply (Merge.p₂′ (merge p₁ p₂)) (apply (del p₂) (x ∷ d)) ≡˘⟨ compose-correct (del p₂) (Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ⟩
apply (del p₂ · Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ∎
merge-pushout (skp p₁) (ins z p₂) d = cong (z ∷_) (merge-pushout (skp p₁) p₂ d )
merge-pushout (del p₁) (skp p₂) (x ∷ d) = begin
apply (del p₁ · Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ≡⟨ compose-correct (del p₁) (Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ⟩
apply (Merge.p₁′ (merge p₁ p₂)) (apply (del p₁) (x ∷ d)) ≡⟨⟩
apply (Merge.p₁′ (merge p₁ p₂)) (apply p₁ d) ≡˘⟨ compose-correct p₁ (Merge.p₁′ (merge p₁ p₂)) d ⟩
apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d ≡⟨ merge-pushout p₁ p₂ d ⟩
apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d ∎
merge-pushout (del p₁) (del p₂) (x ∷ d) = begin
apply (del p₁ · Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ≡⟨ compose-correct (del p₁) (Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ⟩
apply (Merge.p₁′ (merge p₁ p₂)) (apply (del p₁) (x ∷ d)) ≡⟨⟩
apply (Merge.p₁′ (merge p₁ p₂)) (apply p₁ d) ≡˘⟨ compose-correct p₁ (Merge.p₁′ (merge p₁ p₂)) d ⟩
apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d ≡⟨ merge-pushout p₁ p₂ d ⟩
apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d ≡⟨ compose-correct p₂ (Merge.p₂′ (merge p₁ p₂)) d ⟩
apply (Merge.p₂′ (merge p₁ p₂)) (apply p₂ d) ≡⟨⟩
apply (Merge.p₂′ (merge p₁ p₂)) (apply (del p₂) (x ∷ d)) ≡˘⟨ compose-correct (del p₂) (Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ⟩
apply (del p₂ · Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ∎
merge-pushout (del p₁) (ins z p₂) d = cong (z ∷_) (merge-pushout (del p₁) p₂ d)
merge-pushout (ins y p₁) end d = cong (y ∷_) (merge-pushout p₁ end d)
merge-pushout (ins y p₁) (skp p₂) d = cong (y ∷_) (merge-pushout p₁ (skp p₂) d)
merge-pushout (ins y p₁) (del p₂) d = cong (y ∷_) (merge-pushout p₁ (del p₂) d)
merge-pushout (ins y p₁) (ins z p₂) d = cong (z ∷_) (merge-pushout (ins y p₁) p₂ d)
|
