[agda] change to de bruijn because of better judgmental equality

code/gcbpv.agda

@@ -4,27 +4,39 @@ open import Data.Empty
 open import Data.Unit
 open import Data.Sum
 open import Relation.Binary.PropositionalEquality
+open import Data.Nat
+open import Data.Fin
+open import Data.Vec
+import Data.Vec.Properties
 open ≡-Reasoning
 
+lookup-map : ∀ {a b n} {A : Set a} {B : Set b}
+             (i : Fin n) (f : A → B) (xs : Vec A n) →
+             lookup i (Data.Vec.map f xs) ≡ f (lookup i xs)
+lookup-map zero    f (x ∷ xs) = refl
+lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs
+
 data Stoup : Set where
   None : Stoup
   One  : Stoup
 
-⟦_⟧st : Stoup -> Set
-⟦ None ⟧st = ⊥
-⟦ One ⟧st = ⊤
+-- | Semantics
+-- | ⟦ S ⟧st X =~ ⟦ S ⟧ -> X
+⟦_⟧st : Stoup -> Set -> Set
+⟦ None ⟧st X = ⊤
+⟦ One ⟧st X = X
 
 record StCtx (X : Set) : Set where
   constructor stctx
   field
     S : Stoup
-    ty : ⟦ S ⟧st -> X
+    ty : ⟦ S ⟧st X
 
 cdot : forall (X : Set) -> StCtx X
-cdot X = record { S = None ; ty = ⊥-elim }
+cdot X = record { S = None ; ty = tt }
 
 hstoup : forall {Y : Set} -> Y -> StCtx Y
-hstoup B = record { S = One ; ty = \ x → B }
+hstoup B = record { S = One ; ty = B }
 
 data Dimension : Set where
   Top : Dimension
@@ -118,98 +130,102 @@ clttrans B1 B2 B3 (lt B12 x x₁) (lt B23 x₂ x₃) = lt (ctrans B12 B23 (trans
 
 record VCtx (I : DCtx) : Set₁ where
   field
-    Vars : Set
-    vty  : Vars -> VType I
+    Vars : ℕ
+    vty  : Vec (VType I) Vars
 
 
 infixl 20 _,,_
 _,,_ : forall {I} -> VCtx I -> VType I -> VCtx I
-Γ ,, A = record { Vars = VCtx.Vars Γ ⊎ ⊤ ; vty = \ { (inj₁ x) -> VCtx.vty Γ x; (inj₂ tt) -> A } }
+Γ ,, A = record { Vars = suc (VCtx.Vars Γ) ; vty = A ∷ VCtx.vty Γ }
 
 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 }
+Γ ⟪ i ⟫v = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map (\A -> A ⟨ i ⟩v) (VCtx.vty Γ) }
 
-vctxrefl : VCtx (cdot _) -> VCtx onevar
-vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = λ x → vrefl (VCtx.vty Γ x) }
+-- ctx-app-lem : ∀ Γ i -> Γ ⟪ i ⟫v
 
-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)
-  }
+vctxrefl : VCtx (cdot _) -> VCtx onevar
+vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map vrefl (VCtx.vty Γ) }
+
+-- 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
+stctx None ty ⟪ i ⟫c = stctx None tt
+stctx One ty ⟪ i ⟫c = stctx One (ty ⟨ i ⟩c)
 
 cctxrefl : CCtx (cdot _) -> CCtx onevar
-cctxrefl Δ = stctx (StCtx.S Δ) λ x → crefl (StCtx.ty Δ x)
+cctxrefl (stctx None ty) = stctx None tt
+cctxrefl (stctx One ty) = stctx One (crefl ty) 
 
 data Value : forall {I} -> VCtx I -> VType I -> Set₁
 _⟨_⟩vv : forall {Γ : VCtx onevar} {A} ->
@@ -228,7 +244,7 @@ _⟨_⟩cc : forall {Γ : VCtx onevar}{Δ}{B} ->
          Term (Γ ⟪ i ⟫v) (Δ ⟪ i ⟫c) (B ⟨ i ⟩c)
 
 data Value where
-  var : forall {I} (Γ : VCtx I) (x : VCtx.Vars Γ) -> Value Γ (VCtx.vty Γ x)
+  var : forall {I} (Γ : VCtx I) (x : Fin (VCtx.Vars Γ)) A -> A ≡ lookup x (VCtx.vty Γ) -> Value Γ A
   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} ->
@@ -238,23 +254,26 @@ data Value where
   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) ->
-             (v⊤ : Value Γ⊤ A⊤) ->
-             (v⊥ : Value Γ⊥ A⊥) -> 
-             ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ ->
-             Value (vctxtrans Γ⊤ Γ⊥ pctx) (vtrans A⊤ A⊥ pty)
-             -- VCtx.Vars Γ⊤ ≡ VCtx.Vars Γ⊥ ->
-             -- {!!}
-
-var Γ x ⟨ i ⟩vv = var (Γ ⟪ i ⟫v) x 
+  -- valtrans : forall {Γ⊤}{Γ⊥}{A⊤}{A⊥} ->
+  --            (pctx : Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v) ->
+  --            (pty  : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v) ->
+  --            (v⊤ : Value Γ⊤ A⊤) ->
+  --            (v⊥ : Value Γ⊥ A⊥) -> 
+  --            ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ ->
+  --            Value (vctxtrans Γ⊤ Γ⊥ pctx) (vtrans A⊤ A⊥ pty)
+
+var Γ x A p ⟨ i ⟩vv = var (Γ ⟪ i ⟫v) x (A ⟨ i ⟩v)
+  (begin
+    A ⟨ i ⟩v
+    ≡⟨ cong (λ A → A ⟨ i ⟩v) p ⟩
+    (lookup x (VCtx.vty Γ)) ⟨ i ⟩v
+    ≡⟨ sym (lookup-map x (\A -> A ⟨ i ⟩v) (VCtx.vty Γ)) ⟩
+    lookup x (VCtx.vty (Γ ⟪ i ⟫v))
+  ∎)
 vunit Γ ⟨ i ⟩vv = vunit (Γ ⟪ i ⟫v)
 vpair V V' ⟨ i ⟩vv = vpair (V ⟨ i ⟩vv) (V' ⟨ i ⟩vv)
-vdestr V Vk ⟨ i ⟩vv = vdestr (V ⟨ i ⟩vv) {!Vk ⟨ i ⟩vv!}
-vthunk M ⟨ i ⟩vv = vthunk {!M ⟨ i ⟩cc!}
-(valtrans pctx pty v⊤ v⊥ compat) ⟨ Top ⟩vv  = v⊤ ⟨ Top ⟩vv
-(valtrans pctx pty v⊤ v⊥ compat) ⟨ Bot ⟩vv  = {!v⊥ ⟨ Bot ⟩vv!}
+vdestr V Vk ⟨ i ⟩vv = vdestr (V ⟨ i ⟩vv) (Vk ⟨ i ⟩vv)
+vthunk M ⟨ i ⟩vv = vthunk (M ⟨ i ⟩cc)
 
 record ValCompat Γ⊤ Γ⊥ A⊤ A⊥ pctx pty v⊤ v⊥ where
   inductive
@@ -285,25 +304,32 @@ data Term where
          Term Γ Δ B
 
 hole ⟨ i ⟩cc = hole
-lambda M ⟨ i ⟩cc = {!lambda (M ⟨ i ⟩cc)!}
+lambda M ⟨ i ⟩cc = lambda (M ⟨ i ⟩cc)
 app M V ⟨ i ⟩cc = app (M ⟨ i ⟩cc) (V ⟨ i ⟩vv)
-force V ⟨ i ⟩cc = {!force (V ⟨ i ⟩vv)!}
-ret V ⟨ i ⟩cc = {!ret (V ⟨ i ⟩vv)!}
-lett M Mk ⟨ i ⟩cc = lett (M ⟨ i ⟩cc) {!Mk ⟨ i ⟩cc!}
+force V ⟨ i ⟩cc = force (V ⟨ i ⟩vv)
+ret V ⟨ i ⟩cc = ret (V ⟨ i ⟩vv)
+lett M Mk ⟨ i ⟩cc = lett (M ⟨ i ⟩cc) (Mk ⟨ i ⟩cc)
 
 valrefl : forall {Γ}{A} -> Value Γ A -> Value (vctxrefl Γ) (vrefl A)
 termrefl : forall {Γ}{Δ}{B} -> Term Γ Δ B -> Term (vctxrefl Γ) (cctxrefl Δ) (crefl B)
 
-valrefl (var Γ x) = var _ x
+valrefl (var Γ x A p) = var (vctxrefl Γ) x (vrefl A) (
+  begin
+    vrefl A
+    ≡⟨ cong vrefl p ⟩
+    vrefl (lookup x (VCtx.vty Γ))
+    ≡⟨ sym (lookup-map x vrefl (VCtx.vty Γ)) ⟩
+    lookup x (VCtx.vty (vctxrefl Γ))
+  ∎)
 valrefl (vunit Γ) = vunit _
 valrefl (vpair V V') = vpair (valrefl V) (valrefl V')
-valrefl (vdestr V Vk) = vdestr (valrefl V) {!valrefl Vk!}
-valrefl (vthunk M) = vthunk {!termrefl M!}
+valrefl (vdestr V Vk) = vdestr (valrefl V) (valrefl Vk)
+valrefl (vthunk M) = vthunk (termrefl M)
 
 termrefl hole = hole
-termrefl (lambda M) = {!lambda (termrefl M)!}
+termrefl (lambda M) = lambda (termrefl M)
 termrefl (app M V) = app (termrefl M) (valrefl V)
-termrefl (force V) = {!force (valrefl V)!}
-termrefl (ret V) = {!ret (valrefl V)!}
-termrefl (lett M Mk) = lett (termrefl M) {!(termrefl Mk)!}
+termrefl (force V) = force (valrefl V)
+termrefl (ret V) = ret (valrefl V)
+termrefl (lett M Mk) = lett (termrefl M) ((termrefl Mk))