forked from hazelgrove/hazelnut-dynamics-agda
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlemmas-meet.agda
105 lines (92 loc) · 6.13 KB
/
lemmas-meet.agda
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
open import Nat
open import Prelude
open import core-type
open import lemmas-prec
module lemmas-meet where
⊓-ability : ∀{τ1 τ2} → τ1 ~ τ2 → Σ[ τ3 ∈ htyp ] (τ1 ⊓ τ2 == τ3)
⊓-ability ConsistBase = b , MeetBase
⊓-ability ConsistVar = T _ , MeetVar
⊓-ability ConsistHole1 = _ , MeetHoleR
⊓-ability ConsistHole2 = _ , MeetHoleL
⊓-ability (ConsistArr con con₁) with ⊓-ability con | ⊓-ability con₁
... | τ1 , meet1 | τ2 , meet2 = τ1 ==> τ2 , MeetArr meet1 meet2
⊓-ability (ConsistForall con) with ⊓-ability con
... | τ , meet = ·∀ τ , MeetForall meet
⊓-consist : ∀{τ1 τ2 τ3} → τ1 ⊓ τ2 == τ3 → τ1 ~ τ2
⊓-consist MeetHoleL = ConsistHole2
⊓-consist MeetHoleR = ConsistHole1
⊓-consist MeetBase = ConsistBase
⊓-consist MeetVar = ConsistVar
⊓-consist (MeetArr meet meet₁) = ConsistArr (⊓-consist meet) (⊓-consist meet₁)
⊓-consist (MeetForall meet) = ConsistForall (⊓-consist meet)
⊓-unicity : ∀{τ1 τ2 τ3 τ3'} → τ1 ⊓ τ2 == τ3 → τ1 ⊓ τ2 == τ3' → τ3 == τ3'
⊓-unicity MeetHoleL MeetHoleL = refl
⊓-unicity MeetHoleL MeetHoleR = refl
⊓-unicity MeetHoleR MeetHoleL = refl
⊓-unicity MeetHoleR MeetHoleR = refl
⊓-unicity MeetBase MeetBase = refl
⊓-unicity MeetVar MeetVar = refl
⊓-unicity (MeetArr meet1 meet2) (MeetArr meet3 meet4) rewrite ⊓-unicity meet1 meet3 rewrite ⊓-unicity meet2 meet4 = refl
⊓-unicity (MeetForall meet1) (MeetForall meet2) rewrite ⊓-unicity meet1 meet2 = refl
⊓-lb : ∀{τ1 τ2 τ3} → τ1 ⊓ τ2 == τ3 → (τ3 ⊑t τ1 × τ3 ⊑t τ2)
⊓-lb MeetHoleL = PTHole , ⊑t-refl _
⊓-lb MeetHoleR = ⊑t-refl _ , PTHole
⊓-lb MeetBase = PTBase , PTBase
⊓-lb MeetVar = PTTVar , PTTVar
⊓-lb (MeetArr meet meet₁) = (PTArr (π1 (⊓-lb meet)) (π1 (⊓-lb meet₁))) , (PTArr (π2 (⊓-lb meet)) (π2 (⊓-lb meet₁)))
⊓-lb (MeetForall meet) = (PTForall (π1 (⊓-lb meet))) , (PTForall (π2 (⊓-lb meet)))
⊑t-⊓ : ∀{τ1 τ2 τ3 τ1' τ2'} → τ1 ⊑t τ1' → τ2 ⊑t τ2' → τ1 ⊓ τ2 == τ3 → Σ[ τ3' ∈ htyp ] ((τ1' ⊓ τ2' == τ3') × (τ3 ⊑t τ3'))
⊑t-⊓ PTHole prec2 MeetHoleL = _ , MeetHoleL , prec2
⊑t-⊓ prec1 PTHole MeetHoleR = _ , MeetHoleR , prec1
⊑t-⊓ PTHole PTHole _ = ⦇-⦈ , MeetHoleL , PTHole
⊑t-⊓ PTBase PTBase MeetBase = _ , MeetBase , PTBase
⊑t-⊓ PTBase PTHole MeetBase = _ , MeetHoleR , PTBase
⊑t-⊓ PTHole PTBase MeetBase = _ , MeetHoleL , PTBase
⊑t-⊓ PTHole PTTVar MeetVar = _ , MeetHoleL , PTTVar
⊑t-⊓ PTTVar PTHole MeetVar = _ , MeetHoleR , PTTVar
⊑t-⊓ PTTVar PTTVar MeetVar = _ , MeetVar , PTTVar
⊑t-⊓ PTHole (PTArr prec2 prec3) (MeetArr meet1 meet2) = _ , MeetHoleL , PTArr (⊑t-trans (π2 (⊓-lb meet1)) prec2) ((⊑t-trans (π2 (⊓-lb meet2)) prec3))
⊑t-⊓ (PTArr prec1 prec2) PTHole (MeetArr meet1 meet2) = _ , MeetHoleR , PTArr (⊑t-trans (π1 (⊓-lb meet1)) prec1) (⊑t-trans (π1 (⊓-lb meet2)) prec2)
⊑t-⊓ (PTArr prec1 prec2) (PTArr prec3 prec4) (MeetArr meet1 meet2) with ⊑t-⊓ prec1 prec3 meet1 | ⊑t-⊓ prec2 prec4 meet2
... | _ , meet1' , prec1' | _ , meet2' , prec2' = _ , MeetArr meet1' meet2' , PTArr prec1' prec2'
⊑t-⊓ PTHole (PTForall prec2) (MeetForall meet) = _ , MeetHoleL , PTForall (⊑t-trans (π2 (⊓-lb meet)) prec2)
⊑t-⊓ (PTForall prec1) PTHole (MeetForall meet) = _ , MeetHoleR , PTForall (⊑t-trans (π1 (⊓-lb meet)) prec1)
⊑t-⊓ (PTForall prec1) (PTForall prec2) (MeetForall meet) with ⊑t-⊓ prec1 prec2 meet
... | _ , meet' , prec' = _ , MeetForall meet' , PTForall prec'
⊑t-⊓-fun : ∀{τ1 τ2 τ3 τ1' τ2' τ3'} → τ1 ⊑t τ1' → τ2 ⊑t τ2' → τ1 ⊓ τ2 == τ3 → τ1' ⊓ τ2' == τ3' → τ3 ⊑t τ3'
⊑t-⊓-fun PTHole prec2 MeetHoleL MeetHoleL = prec2
⊑t-⊓-fun PTHole prec2 MeetHoleL MeetHoleR = prec2
⊑t-⊓-fun prec1 PTHole MeetHoleR MeetHoleL = prec1
⊑t-⊓-fun prec1 PTHole MeetHoleR MeetHoleR = prec1
⊑t-⊓-fun prec1 prec2 MeetBase MeetHoleL = prec2
⊑t-⊓-fun prec1 prec2 MeetBase MeetHoleR = prec1
⊑t-⊓-fun prec1 prec2 MeetBase MeetBase = prec2
⊑t-⊓-fun prec1 prec2 MeetVar MeetHoleL = prec2
⊑t-⊓-fun prec1 prec2 MeetVar MeetHoleR = prec1
⊑t-⊓-fun prec1 prec2 MeetVar MeetVar = prec2
⊑t-⊓-fun PTHole prec2 (MeetArr meet1 meet2) MeetHoleL = ⊑t-trans (PTArr (π2 (⊓-lb meet1)) (π2 (⊓-lb meet2))) prec2
⊑t-⊓-fun prec1 prec2 (MeetArr meet1 meet2) MeetHoleR = ⊑t-trans (PTArr (π1 (⊓-lb meet1)) (π1 (⊓-lb meet2))) prec1
⊑t-⊓-fun (PTArr prec1 prec2) (PTArr prec3 prec4) (MeetArr meet1 meet2) (MeetArr meet3 meet4) =
PTArr (⊑t-⊓-fun prec1 prec3 meet1 meet3) (⊑t-⊓-fun prec2 prec4 meet2 meet4)
⊑t-⊓-fun PTHole prec2 (MeetForall meet) MeetHoleL = ⊑t-trans (PTForall (π2 (⊓-lb meet))) prec2
⊑t-⊓-fun prec1 prec2 (MeetForall meet) MeetHoleR = ⊑t-trans (PTForall (π1 (⊓-lb meet))) prec1
⊑t-⊓-fun (PTForall prec1) (PTForall prec2) (MeetForall meet) (MeetForall meet2) = PTForall (⊑t-⊓-fun prec1 prec2 meet meet2)
module meet-match where
--- direct matching for arrows
data _▸arr_ : htyp → htyp → Set where
MAHole : ⦇-⦈ ▸arr ⦇-⦈ ==> ⦇-⦈
MAArr : {τ1 τ2 : htyp} → τ1 ==> τ2 ▸arr τ1 ==> τ2
--- direct matching for foralls
data _▸forall_ : htyp → htyp → Set where
MFHole : ⦇-⦈ ▸forall (·∀ ⦇-⦈)
MFForall : ∀{τ} → (·∀ τ) ▸forall (·∀ τ)
⊓-▸arr : ∀{τ1 τ2 τ3} → τ1 ⊓ (⦇-⦈ ==> ⦇-⦈) == τ2 → τ1 ▸arr τ3 → τ2 == τ3
⊓-▸arr MeetHoleL MAHole = refl
⊓-▸arr (MeetArr MeetHoleL MeetHoleL) MAArr = refl
⊓-▸arr (MeetArr MeetHoleL MeetHoleR) MAArr = refl
⊓-▸arr (MeetArr MeetHoleR MeetHoleL) MAArr = refl
⊓-▸arr (MeetArr MeetHoleR MeetHoleR) MAArr = refl
⊓-▸forall : ∀{τ1 τ2 τ3} → τ1 ⊓ ·∀ ⦇-⦈ == τ2 → τ1 ▸forall τ3 → τ2 == τ3
⊓-▸forall MeetHoleL MFHole = refl
⊓-▸forall (MeetForall MeetHoleL) MFForall = refl
⊓-▸forall (MeetForall MeetHoleR) MFForall = refl