From 10178f616ab0bf6525ec5363f262b5c1528cee47 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 26 Apr 2018 10:15:32 -0400
Subject: [PATCH] most of the multiplicative term lang, val transitivity was
 hard

---
 code/gcbpv.agda | 186 ++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 181 insertions(+), 5 deletions(-)

diff --git a/code/gcbpv.agda b/code/gcbpv.agda
index 44280d0..ff801ee 100644
--- a/code/gcbpv.agda
+++ b/code/gcbpv.agda
@@ -2,7 +2,9 @@ module gcbpv where
 
 open import Data.Empty
 open import Data.Unit
+open import Data.Sum
 open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
 
 data Stoup : Set where
   None : Stoup
@@ -13,7 +15,7 @@ data Stoup : Set where
 ⟦ One ⟧st = ⊤
 
 record StCtx (X : Set) : Set where
-  constructor ctx
+  constructor stctx
   field
     S : Stoup
     ty : ⟦ S ⟧st -> X
@@ -21,8 +23,8 @@ record StCtx (X : Set) : Set where
 cdot : forall (X : Set) -> StCtx X
 cdot X = record { S = None ; ty = ⊥-elim }
 
-hstoup : forall (Y : Set) -> Y -> StCtx Y
-hstoup Y B = record { S = One ; ty = \ x → B }
+hstoup : forall {Y : Set} -> Y -> StCtx Y
+hstoup B = record { S = One ; ty = \ x → B }
 
 data Dimension : Set where
   Top : Dimension
@@ -32,7 +34,7 @@ DCtx : Set
 DCtx = StCtx ⊤
 
 onevar : StCtx ⊤
-onevar = hstoup ⊤ tt
+onevar = hstoup tt
 
 infix 90 _⟨_⟩v
 infix 90 _⟨_⟩c
@@ -80,7 +82,7 @@ crefl (F A) = F (vrefl A)
 vreflretract : forall A i -> vrefl A ⟨ i ⟩v ≡ A
 creflretract : forall B i -> crefl B ⟨ i ⟩c ≡ B
 
-vreflretract (VUnit .(ctx None ⊥-elim)) i = refl
+vreflretract (VUnit _) i = refl
 vreflretract (A × A₁) i = cong₂ _×_ (vreflretract A i) (vreflretract A₁ i)
 vreflretract (U B) i = cong U (creflretract B i)
 
@@ -105,3 +107,177 @@ cltrefl B = lt (crefl B) (creflretract B Top) ((creflretract B Bot))
 
 clttrans : forall B1 B2 B3 -> CLt B1 B2 -> CLt B2 B3 -> CLt B1 B3
 clttrans B1 B2 B3 (lt B12 x x₁) (lt B23 x₂ x₃) = lt (ctrans B12 B23 (trans x₁ (sym x₂))) x x₃
+
+-- | Now the term structure
+-- Values correspond to complex values in cbpv
+-- Terms correspond to both terms and complex stacks in cbpv
+-- Everything is also indexed by a dimension stoup, so that we simultaneously
+-- implement the term constructors and their monotonicity, meaning like the
+-- types we can implement reflexivity as weakening and only have to add in
+-- transitivity, beta and eta
+
+record VCtx (I : DCtx) : Set₁ where
+  field
+    Vars : Set
+    vty  : Vars -> VType I
+
+
+infixl 20 _,,_
+_,,_ : forall {I} -> VCtx I -> VType I -> VCtx I
+Γ ,, A = record { Vars = VCtx.Vars Γ ⊎ ⊤ ; vty = \ { (inj₁ x) -> VCtx.vty Γ x; (inj₂ tt) -> A } }
+
+infix 90 _⟪_⟫v
+infix 90 _⟪_⟫c
+
+_⟪_⟫v : VCtx onevar -> Dimension -> VCtx (cdot _)
+Γ ⟪ i ⟫v = record { Vars = VCtx.Vars Γ ; vty = λ x → ((VCtx.vty Γ) x) ⟨ i ⟩v }
+
+vctxrefl : VCtx (cdot _) -> VCtx onevar
+vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = λ x → vrefl (VCtx.vty Γ x) }
+
+record VctxComp (Γ⊤ Γ⊥ : VCtx onevar) : Set₁ where
+  field
+    SameVar : Set
+    eq⊤     : SameVar ≡ VCtx.Vars Γ⊤
+    eq⊥     : SameVar ≡ VCtx.Vars Γ⊥
+    eqδ     :
+      forall (x : SameVar) ->
+      (VCtx.vty Γ⊤ (subst _ eq⊤ x) ⟨ Bot ⟩v) ≡ VCtx.vty Γ⊥ (subst _ eq⊥ x) ⟨ Top ⟩v
+
+eq-to-compvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥
+eq-to-compvars Γ⊤ Γ⊥ eq =
+  begin VCtx.Vars Γ⊤
+    ≡⟨ refl ⟩
+    VCtx.Vars (Γ⊤ ⟪ Bot ⟫v)
+    ≡⟨ cong VCtx.Vars eq ⟩
+    VCtx.Vars (Γ⊥ ⟪ Top ⟫v)
+    ≡⟨ refl ⟩
+    VCtx.Vars Γ⊥
+  ∎
+
+lemlem : forall {I} Vars (vty1 : Vars -> VType I) vty2 -> record { Vars = Vars ; vty = vty1 } ≡ record { Vars = Vars; vty = vty2 } -> vty1 ≡ vty2
+lemlem Vars vty1 vty2 refl = refl
+
+lem : ∀ (Γ⊥ : VCtx onevar) ->
+        (Γ⊤ : VCtx onevar) ->
+      (p  : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) -> 
+      (x : VCtx.Vars Γ⊤) -> 
+      VCtx.vty (Γ⊤ ⟪ Bot ⟫v) x ≡ VCtx.vty (Γ⊥ ⟪ Top ⟫v) (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x)
+lem Γ⊥ Γ⊤ p x with (eq-to-compvars Γ⊤ Γ⊥ p)
+lem Γ⊥ record { Vars = .(VCtx.Vars Γ⊥) ; vty = vty⊤ } p Vars⊥ | refl =
+  begin
+    vty⊤ Vars⊥ ⟨ Bot ⟩v
+    ≡⟨ refl ⟩
+    VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = λ x → vty⊤ x ⟨ Bot ⟩v }) Vars⊥
+    ≡⟨ cong (λ x → VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = x }) Vars⊥) (lemlem (VCtx.Vars Γ⊥) (λ z → vty⊤ z ⟨ Bot ⟩v) ((λ x → VCtx.vty Γ⊥ x ⟨ Top ⟩v)) p) ⟩
+    VCtx.vty (record { Vars = VCtx.Vars Γ⊥ ; vty = λ x → VCtx.vty Γ⊥ x ⟨ Top ⟩v }) Vars⊥
+    ≡⟨ refl ⟩
+    VCtx.vty Γ⊥ Vars⊥ ⟨ Top ⟩v
+  ∎
+
+eq-to-comp : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VctxComp Γ⊤ Γ⊥
+eq-to-comp Γ⊤ Γ⊥ p =
+  record {
+  SameVar = VCtx.Vars Γ⊤ ;
+  eq⊤ = refl ;
+  eq⊥ = eq-to-compvars Γ⊤ Γ⊥ p ;
+  eqδ = λ x →
+    begin
+      VCtx.vty Γ⊤ x ⟨ Bot ⟩v
+      ≡⟨ refl ⟩
+      VCtx.vty (Γ⊤ ⟪ Bot ⟫v) x
+      ≡⟨ lem Γ⊥ Γ⊤ p x ⟩
+      VCtx.vty (Γ⊥ ⟪ Top ⟫v) (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x)
+      ≡⟨ refl ⟩
+      VCtx.vty Γ⊥ (subst (λ v → v) (eq-to-compvars Γ⊤ Γ⊥ p) x) ⟨ Top ⟩v
+    ∎
+  }
+
+vctxtrans : ∀ (Γ⊤ Γ⊥ : VCtx onevar) -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VCtx onevar
+vctxtrans Γ⊤ Γ⊥ p with eq-to-comp Γ⊤ Γ⊥ p
+vctxtrans Γ⊤ Γ⊥ p | record { SameVar = SameVar ; eq⊤ = eq⊤ ; eq⊥ = eq⊥ ; eqδ = eqδ } =
+  record { Vars = SameVar ; vty = λ x →
+    vtrans (VCtx.vty Γ⊤ (subst (λ z → z) eq⊤ x))
+           (VCtx.vty Γ⊥ (subst (λ z → z) eq⊥ x))
+           (eqδ x)
+  }
+
+CCtx : DCtx -> Set
+CCtx I = StCtx (CType I)
+
+_⟪_⟫c : CCtx onevar -> Dimension -> CCtx (cdot _)
+Δ ⟪ i ⟫c = stctx (StCtx.S Δ) λ x → StCtx.ty Δ x ⟨ i ⟩c
+
+cctxrefl : CCtx (cdot _) -> CCtx onevar
+cctxrefl Δ = stctx (StCtx.S Δ) λ x → crefl (StCtx.ty Δ x)
+
+data Value : forall {I} -> VCtx I -> VType I -> Set₁
+_⟨_⟩vv : forall {Γ : VCtx onevar} {A} ->
+         Value Γ A ->
+         (i : Dimension) ->
+         Value (Γ ⟪ i ⟫v) (A ⟨ i ⟩v)
+record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v) : Set₁
+data Term  : forall {I} -> VCtx I -> CCtx I -> CType I -> Set₁
+_⟨_⟩cc : forall {Γ : VCtx onevar}{Δ}{B} ->
+         Term Γ Δ B ->
+         (i : Dimension) ->
+         Term (Γ ⟪ i ⟫v) (Δ ⟪ i ⟫c) (B ⟨ i ⟩c)
+
+data Value where
+  var : forall {I} (Γ : VCtx I) (x : VCtx.Vars Γ) -> Value Γ (VCtx.vty Γ x)
+  vunit : forall {I} (Γ : VCtx I) -> Value Γ (VUnit _)
+  vpair : forall {I}{Γ : VCtx I}{A}{A'} -> Value Γ A -> Value Γ A' -> Value Γ (A × A')
+  vdestr : forall {I}{Γ : VCtx I}{A}{A'}{Am} ->
+           Value Γ (A × A') ->
+           Value (Γ ,, A ,, A') Am ->
+           Value Γ Am
+  vthunk : forall {I}{Γ : VCtx I}{B} ->
+           Term Γ (cdot _) B ->
+           Value Γ (U B)
+  valtrans : forall {Γ⊤}{Γ⊥}{A⊤}{A⊥} ->
+             (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) ->
+             (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v) ->
+             ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty ->
+             Value (vctxtrans Γ⊤ Γ⊥ pctx) (vtrans A⊤ A⊥ pty)
+             -- VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥ ->
+             -- {!!}
+
+_⟨_⟩vv = {!!}
+
+record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty where
+  inductive
+  field
+    v⊤ : Value Γ⊤ A⊤
+    v⊥ : Value Γ⊥ A⊥
+    compat :
+      subst (λ Γm → Value Γm (A⊥ ⟨ Top ⟩v)) pctx (subst (λ Am → Value (Γ⊤ ⟪ Bot ⟫v) Am) pty
+      (v⊤ ⟨ Bot ⟩vv))
+      ≡ v⊥ ⟨ Top ⟩vv
+
+data Term where
+  hole : forall {I}{Γ : VCtx I}{B} -> Term Γ (hstoup B) B
+  lambda : forall {I}{Γ : VCtx I}{Δ}{A}{B} ->
+           Term (Γ ,, A) Δ B ->
+           Term Γ Δ (A ⇀ B)
+  app : forall {I}{Γ : VCtx I}{Δ}{A}{B} ->
+           Term Γ Δ (A ⇀ B) ->
+           Value Γ A ->
+           Term Γ Δ B
+  force : forall {I}{Γ : VCtx I}{B} ->
+          Value Γ (U B) ->
+          Term Γ (cdot _) B
+  ret : forall {I}{Γ : VCtx I}{A} ->
+        Value Γ A ->
+        Term Γ (cdot _) (F A)
+  lett : forall {I}{Γ : VCtx I}{Δ}{A}{B} ->
+         Term Γ Δ (F A) ->
+         Term Γ (cdot _) B ->
+         Term Γ Δ B
+
+_⟨_⟩cc = {!!}
+
+valrefl : forall {Γ}{A} -> Value Γ A -> Value (vctxrefl Γ) (vrefl A)
+valrefl = {!!}
+
+termrefl : forall {Γ}{Δ}{B} -> Term Γ Δ B -> Term (vctxrefl Γ) (cctxrefl Δ) (crefl B)
+termrefl = {!!}
-- 
GitLab