[agda] rewrite with some agdaisms, think it will work now

code/gcbpv.agda

@@ -13,7 +13,7 @@ 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 i (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
 
@@ -49,12 +49,13 @@ DCtx = StCtx ⊤
 onevar : StCtx ⊤
 onevar = hstoup tt
 
-infix 90 _⟨_⟩v
-infix 90 _⟨_⟩c
+infixl 90 _⟨_⟩v
+infixl 90 _⟨_⟩vsq
+infixl 90 _⟨_⟩c
 
-record VTC : Set
 data VType : DCtx -> Set
 _⟨_⟩v : VType onevar -> Dimension -> VType (cdot _)
+record VTC : Set
 data CType : DCtx -> Set
 _⟨_⟩c : CType onevar -> Dimension -> CType (cdot _)
 
@@ -67,6 +68,7 @@ record VTC where
     A⊥ : VType onevar
     eq : A⊤ ⟨ Bot ⟩v ≡ A⊥ ⟨ Top ⟩v
 
+
 data VType where
   VUnit  : forall I -> VType I
   _×_    : forall {I} -> VType I -> VType I -> VType I
@@ -76,8 +78,8 @@ data VType where
 VUnit _ ⟨ i ⟩v = VUnit _
 (A × A') ⟨ i ⟩v = (A ⟨ i ⟩v) × (A' ⟨ i ⟩v)
 U B ⟨ i ⟩v = U (B ⟨ i ⟩c)
-vtrans comp ⟨ Top ⟩v = VTC.A⊤ comp ⟨ Top ⟩v
-vtrans comp ⟨ Bot ⟩v = VTC.A⊥ comp ⟨ Bot ⟩v
+vtrans Vsq ⟨ Top ⟩v = VTC.A⊤ Vsq ⟨ Top ⟩v -- morally this: Vsq ⟨ Top ⟩vsq ⟨ Top ⟩v
+vtrans Vsq ⟨ Bot ⟩v = VTC.A⊥ Vsq ⟨ Bot ⟩v -- morally this: Vsq ⟨ Bot ⟩vsq ⟨ Bot ⟩v
 -- vtrans Atop Abot p ⟨ Top ⟩v = Atop ⟨ Top ⟩v
 -- vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩v
 
@@ -93,6 +95,10 @@ F A ⟨ i ⟩c = F (A ⟨ i ⟩v)
 ctrans Btop Bbot p ⟨ Top ⟩c = Btop ⟨ Top ⟩c
 ctrans Btop Bbot p ⟨ Bot ⟩c = Bbot ⟨ Bot ⟩c
 
+_⟨_⟩vsq : VTC -> Dimension -> VType onevar
+Vsq ⟨ Top ⟩vsq = VTC.A⊤ Vsq
+Vsq ⟨ Bot ⟩vsq = VTC.A⊥ Vsq
+
 vrefl : VType (cdot _) -> VType onevar
 crefl : CType (cdot _) -> CType onevar
 vrefl (VUnit _) = VUnit _
@@ -119,14 +125,14 @@ data CLt (B B' : CType (cdot _)) : Set where
   lt : forall (Bord : CType onevar) -> Bord ⟨ Top ⟩c ≡ B -> Bord ⟨ Bot ⟩c ≡ B' -> CLt B B'
 
 -- | Some sanity checking
-vltrefl : forall A -> VLt A A
-vltrefl A = lt (vrefl A) (vreflretract A Top) ((vreflretract A Bot))
+-- vltrefl : forall A -> VLt A A
+-- vltrefl A = lt (vrefl A) (vreflretract A Top) ((vreflretract A Bot))
 
 -- vlttrans : forall A1 A2 A3 -> VLt A1 A2 -> VLt A2 A3 -> VLt A1 A3
 -- vlttrans A1 A2 A3 (lt A12 x x₁) (lt A23 x₂ x₃) = lt (vtrans A12 A23 (trans x₁ (sym x₂))) x x₃
 
-cltrefl : forall B -> CLt B B
-cltrefl B = lt (crefl B) (creflretract B Top) ((creflretract B Bot))
+-- cltrefl : forall B -> CLt B B
+-- 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₃
@@ -148,44 +154,44 @@ open VCtx
 
 infixl 20 _,,_
 _,,_ : forall {I} -> VCtx I -> VType I -> VCtx I
-Γ ,, A = record { Vars = suc (VCtx.Vars Γ) ; vty = A ∷ VCtx.vty Γ }
+Vars (Γ ,, A) = suc (Vars Γ)
+vty  (Γ ,, A) = A ∷ vty Γ
 
-infix 90 _⟪_⟫v
-infix 90 _⟪_⟫c
+infixl 90 _⟪_⟫v
+infixl 90 _⟪_⟫vsq
+infixl 90 _⟪_⟫c
 
 _⟪_⟫v : VCtx onevar -> Dimension -> VCtx (cdot _)
-Γ ⟪ i ⟫v = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map (\A -> A ⟨ i ⟩v) (VCtx.vty Γ) }
+Vars (Γ ⟪ i ⟫v) = Vars Γ
+vty (Γ ⟪ i ⟫v)  = map (\A -> A ⟨ i ⟩v) (vty Γ)
 
 -- ctx-app-lem : ∀ Γ i -> Γ ⟪ i ⟫v
 
 vctxrefl : VCtx (cdot _) -> VCtx onevar
-vctxrefl Γ = record { Vars = VCtx.Vars Γ ; vty = Data.Vec.map vrefl (VCtx.vty Γ) }
+Vars (vctxrefl Γ) = Vars Γ
+vty  (vctxrefl Γ) = map vrefl (vty Γ)
 
 record VCtxTC : Set where
   field
     Vars : ℕ
     vty  : Vec VTC Vars
+open VCtxTC
 
-Γ⊤ : VCtxTC -> VCtx onevar
-Γ⊤ Γsq = vctx (VCtxTC.Vars Γsq) (map VTC.A⊤ (VCtxTC.vty Γsq))
-
-Γ⊥ : VCtxTC -> VCtx onevar
-Γ⊥ Γsq = vctx (VCtxTC.Vars Γsq) (map VTC.A⊥ (VCtxTC.vty Γsq))
+_⟪_⟫vsq : VCtxTC -> Dimension -> VCtx onevar
+Vars (Γsq ⟪ i ⟫vsq) = Vars Γsq
+vty  (Γsq ⟪ i ⟫vsq) = (map (λ Vsq → Vsq ⟨ i ⟩vsq) (vty Γsq))
 
 vctxtrans : VCtxTC -> VCtx onevar
-vctxtrans Γsq = vctx (VCtxTC.Vars Γsq) (map vtrans (VCtxTC.vty Γsq))
-
-lem' : ∀ Asq -> vtrans Asq ⟨ Top ⟩v ≡ VTC.A⊤ Asq ⟨ Top ⟩v
-lem' Asq = refl
+vctxtrans Γsq = vctx (Vars Γsq) (map vtrans (vty Γsq))
 
-lem : ∀ Γsq -> (vctxtrans Γsq ⟪ Top ⟫v) ≡ ((Γ⊤ Γsq) ⟪ Top ⟫v)
-lem Γsq =
+ctxttrans-dapp-lem : ∀ Γsq i -> vctxtrans Γsq ⟪ i ⟫v ≡ Γsq ⟪ i ⟫vsq ⟪ i ⟫v
+ctxttrans-dapp-lem Γsq i =
   begin
-    vctxtrans Γsq ⟪ Top ⟫v
+    vctxtrans Γsq ⟪ i ⟫v
     ≡⟨ {!!} ⟩
-    vctxtrans Γsq ⟪ Top ⟫v
+    vctxtrans Γsq ⟪ i ⟫v
     ≡⟨ {!!} ⟩
-    Γ⊤ Γsq ⟪ Top ⟫v
+    Γsq ⟪ i ⟫vsq ⟪ i ⟫v
   ∎
 
 CCtx : DCtx -> Set
@@ -216,11 +222,11 @@ record ValTC where
   field
     ΓΓ : VCtxTC
     AA : VTC
-    V⊤ : Value (Γ⊤ ΓΓ) (VTC.A⊤ AA)
-    V⊥ : Value (Γ⊥ ΓΓ) (VTC.A⊥ AA)
+    V⊤ : Value (ΓΓ ⟪ Top ⟫vsq) (AA ⟨ Top ⟩vsq)
+    V⊥ : Value (ΓΓ ⟪ Bot ⟫vsq) (AA ⟨ Bot ⟩vsq)
 
 data Value where
-  var : forall {I} (Γ : VCtx I) (x : Fin (VCtx.Vars Γ)) A -> A ≡ lookup x (VCtx.vty Γ) -> Value Γ A
+  var : forall {I} (Γ : VCtx I) (x : Fin (Vars Γ)) A -> A ≡ lookup x (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,17 +244,16 @@ 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))
+    (lookup x (vty Γ)) ⟨ i ⟩v
+    ≡⟨ sym (lookup-map x (\A -> A ⟨ i ⟩v) (vty Γ)) ⟩
+    lookup x (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 sq ⟨ Top ⟩vv with lem (ValTC.ΓΓ sq)
-... | q = {!!} -- subst (λ Γ⊤ → {!Value Γ⊤ ?!}) q ((ValTC.V⊤ sq) ⟨ Top ⟩vv)
-valtrans sq ⟨ Bot ⟩vv = {!!}
+valtrans sq ⟨ Top ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) Top = ValTC.V⊤ sq ⟨ Top ⟩vv
+valtrans sq ⟨ Bot ⟩vv rewrite ctxttrans-dapp-lem (ValTC.ΓΓ sq) Bot = ValTC.V⊥ sq ⟨ Bot ⟩vv
 
 data Term where
   hole : forall {I}{Γ : VCtx I}{B} -> Term Γ (hstoup B) B
@@ -284,9 +289,9 @@ 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 Γ))
+    vrefl (lookup x (vty Γ))
+    ≡⟨ sym (lookup-map x vrefl (vty Γ)) ⟩
+    lookup x (vty (vctxrefl Γ))
   ∎)
 valrefl (vunit Γ) = vunit _
 valrefl (vpair V V') = vpair (valrefl V) (valrefl V')
@@ -299,83 +304,3 @@ 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))
-
--- 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
---   ∎
-
--- mkeqvars : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> Vars Γ⊤ ≡ Vars Γ⊥
--- mkeqvars Γ⊤ Γ⊥ p = 
---     begin
---       Vars Γ⊤
---       ≡⟨ refl ⟩
---       Vars (Γ⊤ ⟪ Bot ⟫v)
---       ≡⟨ cong Vars p ⟩
---       Vars (Γ⊥ ⟪ Top ⟫v)
---       ≡⟨ refl ⟩
---       Vars Γ⊥
---     ∎
-
-
--- eq-to-comp : ∀ Γ⊤ Γ⊥ -> Γ⊤ ⟪ Bot ⟫v ≡ Γ⊥ ⟪ Top ⟫v -> VctxTransComp Γ⊤ Γ⊥
--- eq-to-comp Γ⊤ Γ⊥ p = record {
---   eqvars = mkeqvars Γ⊤ Γ⊥ p;
---   eqδ = tabulate λ x⊤ → record {
---     A⊤ = lookup x⊤ (vty Γ⊤) ;
---     A⊥ = lookup (subst Fin (mkeqvars Γ⊤ Γ⊥ p)  x⊤) (vty Γ⊥) ;
---     compat =
---       begin
---         lookup x⊤ (vty Γ⊤) ⟨ Bot ⟩v
---         ≡⟨ sym (lookup-map x⊤ (λ z → z ⟨ Bot ⟩v) (vty Γ⊤)) ⟩
---         lookup x⊤ (vty (Γ⊤ ⟪ Bot ⟫v))
---         ≡⟨ cong (lookup x⊤) {!p!} ⟩
---         lookup x⊤ (subst (Vec (VType _)) _ (vty (Γ⊥ ⟪ Top ⟫v)))
---         ≡⟨ {!!} ⟩
---         lookup (subst Fin _ x⊤) (vty (Γ⊥ ⟪ Top ⟫v))
---         ≡⟨ lookup-map _ (\z -> z ⟨ Top ⟩v) (vty Γ⊥) ⟩
---         lookup (subst Fin _ x⊤) (vty Γ⊥) ⟨ Top ⟩v
---       ∎
---     }
---   }
---   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
---     ∎
---   }