/
big-step-prop.agda
128 lines (103 loc) · 5.6 KB
/
big-step-prop.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
{------------------------}
{- Big-step properties -}
{------------------------}
module big-step-prop where
open import Level as L using (Level ; _⊔_)
open import Function as F hiding (_∋_ ; _$_)
open import acmm
open import relations
open import sim-fusion-lemmas
lemma-2-1 : {τ : Ty} {M : Trm₀ τ} {U V : Val₀ τ} → M ⇓ U → M ⇓ V → U ≡ V
lemma-2-1 ⇓val ⇓val = PEq.refl
lemma-2-1 (⇓if-tt derU) (⇓if-tt derV) = lemma-2-1 derU derV
lemma-2-1 (⇓if-ff derU) (⇓if-ff derV) = lemma-2-1 derU derV
lemma-2-1 (⇓app derU) (⇓app derV) = lemma-2-1 derU derV
lemma-2-1 (⇓let derU derU') (⇓let derV derV')
rewrite lemma-2-1 derU derV | lemma-2-1 derU' derV' = PEq.refl
lemma-2-3i : {τ : Ty} {M N : Trm₀ τ} {V : Val₀ τ} →
(dev : M ⇓ V) → (red : M →₁ N) → N ⇓ V
lemma-2-3i (⇓if-tt dev) →₁if = dev
lemma-2-3i (⇓if-ff dev) →₁if = dev
lemma-2-3i (⇓app dev) →₁app = dev
→₁letTi : {σ τ : Ty} {N : (σ ⊢ Trm τ) _} {M M' : _} {V : Val₀ _} →
(der : `let M N ⇓ V) → (red : M →₁ M') → `let M' N ⇓ V
→₁letTi (⇓let derM derN) red = ⇓let (lemma-2-3i derM red) derN
lemma-2-3ii : {τ : Ty} {M N : Trm₀ τ} {V : Val₀ τ} →
(red : M →₁ N) → (dev : N ⇓ V) → M ⇓ V
lemma-2-3ii (→₁if {b = tt}) = ⇓if-tt
lemma-2-3ii (→₁if {b = ff}) = ⇓if-ff
lemma-2-3ii →₁app = ⇓app
→₁letTii : {σ τ : Ty} {N : (σ ⊢ Trm τ) _} {M M' : _} {V : Val₀ _} →
(red : M →₁ M') → (der : `let M' N ⇓ V) → `let M N ⇓ V
→₁letTii red (⇓let derM derN) = ⇓let (lemma-2-3ii red derM) derN
{----------------------------}
{-- Generic Lemmas on [_]^T -}
{----------------------------}
-- Lemmas regarding Val to Trm relation transformer
lemma-[_]^T-refl : {ℓ^V : Level} {τ : Ty} {R : GRel^V {ℓ^V} {τ}}
(r : (V : Val₀ τ) → R V V) → (M : Trm₀ τ) → M [ R ]^T M
lemma-[ r ]^T-refl M {U = U} der = U , der , r U
lemma-[_]^T-trans : {ℓ^V : Level} {τ : Ty} {R S T : GRel^V {ℓ^V} {τ}}
(t : {M N P : Val₀ τ} → R M N → S N P → T M P) →
{M N P : Trm₀ τ} → M [ R ]^T N → N [ S ]^T P → M [ T ]^T P
lemma-[ t ]^T-trans M[R]^TN N[S]^TP derM with M[R]^TN derM
... | _ , derN , rUV with N[S]^TP derN
... | _ , derP , sVW = _ , derP , t rUV sVW
lemma-[_]^T-mono : {ℓ^V : Level} {τ : Ty} {R S : GRel^V {ℓ^V} {τ}}
(m : {M N : Val₀ τ} → R M N → S M N) →
{M N : Trm₀ τ} → M [ R ]^T N → M [ S ]^T N
lemma-[ m ]^T-mono M[R]^TN {V} derM with M[R]^TN derM
... | _ , derN , rVW = _ , derN , m rVW
-- Trm relation transformer left/right respects primitive reduction.
lemma-2-10i : {ℓ^V : Level} {τ : Ty} {R : GRel^V {ℓ^V} {τ}}
{M N P : Trm₀ τ} → M →₁ P → (M [ R ]^T N) → P [ R ]^T N
lemma-2-10i red r = r ∘ (lemma-2-3ii red)
lemma-2-10i-exp : {ℓ^V : Level} {τ : Ty} {R : GRel^V {ℓ^V} {τ}}
{M N P : Trm₀ τ} → P →₁ M → (M [ R ]^T N) → P [ R ]^T N
lemma-2-10i-exp red r der = r (lemma-2-3i der red)
lemma-2-10ii : {ℓ^V : Level} {τ : Ty} {R : GRel^V {ℓ^V} {τ}}
{M N P : Trm₀ τ} → (M [ R ]^T N) → N →₁ P → M [ R ]^T P
lemma-2-10ii r red der with r der
... | V , derM , rUV = V , lemma-2-3i derM red , rUV
lemma-2-10ii-exp : {ℓ^V : Level} {τ : Ty} {R : GRel^V {ℓ^V} {τ}}
{M N P : Trm₀ τ} → (M [ R ]^T N) → P →₁ N → M [ R ]^T P
lemma-2-10ii-exp r red der with r der
... | V , derM , rUV = V , lemma-2-3ii red derM , rUV
lemma-[-]^T-βV : {ℓ^V : Level} {τ : Ty} {R : GRel^V {ℓ^V} {τ}} →
∀ {σ} {P Q : Trm₀ (σ `→ τ)} {M N} {V W} →
P ⇓ `λ M → appT P V [ R ]^T appT Q W → Q ⇓ `λ N →
(βV M V) [ R ]^T (βV N W)
lemma-[-]^T-βV {M = M} {V = V} {W = W} derM r derN {U} (⇓app derV)
with (λ der → r {U} (⇓let derM (⇓app der)))
... | hyp rewrite weak-sub (`λ M) V with hyp derV
... | _ , ⇓let derQ (⇓app {M = Q} derU) , simU
rewrite weak-sub (`λ Q) W | `λ-inj (lemma-2-1 derN derQ) =
_ , ⇓app derU , simU
-- congruence rules
lemma-[-]^T-app : {ℓ^V : Level} {R : {τ : Ty} → GRel^V {ℓ^V} {τ}} →
∀ {σ τ} →
(R-λ : ∀ {M N} {V W} → R {σ} V W → R {σ `→ τ} (`λ M) (`λ N) →
M ⟨ V /var₀⟩ [ R {τ} ]^T N ⟨ W /var₀⟩) →
∀ {f g} {a b} → R {σ `→ τ} f g → R {σ} a b → (f `$ a) [ R {τ} ]^T (g `$ b)
lemma-[-]^T-app R-λ {`var ()}
lemma-[-]^T-app R-λ {`λ M} {`var ()}
lemma-[-]^T-app R-λ {`λ M} {`λ N} {V} {W} rMN rVW =
lemma-2-10i-exp →₁app (lemma-2-10ii-exp (R-λ {M} {N} rVW rMN) →₁app)
lemma-[-]^T-if : {ℓ^V : Level} {R : {τ : Ty} → GRel^V {ℓ^V} {τ}} →
(R-B : ∀ {b b' : ⟦ `B ⟧B} → R (`b b) (`b b') → b ≡ b') →
∀ {σ} {B C M N P Q} → R {`b `B} B C → M [ R {σ} ]^T P → N [ R {σ} ]^T Q →
(`if B M N) [ R {σ} ]^T (`if C P Q)
lemma-[-]^T-if R-B {B = `var ()}
lemma-[-]^T-if R-B {B = `b b} {`var ()}
lemma-[-]^T-if R-B {B = `b b} {C = `b b'} rBC rMP rNQ with R-B rBC
lemma-[-]^T-if R-B {B = `b tt} {C = `b .tt} rBC rMP rNQ | PEq.refl =
lemma-2-10i-exp →₁if (lemma-2-10ii-exp rMP →₁if)
lemma-[-]^T-if R-B {B = `b ff} {C = `b .ff} rBC rMP rNQ | PEq.refl =
lemma-2-10i-exp →₁if (lemma-2-10ii-exp rNQ →₁if)
lemma-[-]^T-let : {ℓ^V : Level} {R : {τ : Ty} → GRel^V {ℓ^V} {τ}} →
∀ {σ τ} {M N P Q} → M [ R {σ} ]^T P →
(∀ {V W} → R {σ} V W → N ⟨ V /var₀⟩ [ R {τ} ]^T Q ⟨ W /var₀⟩) →
`let M N [ R ]^T `let P Q
lemma-[-]^T-let simM simN (⇓let derM derN) with simM derM
... | W , derW , rVW with simN rVW derN
... | U , derU , rU = U , ⇓let derW derU , rU