From 3d3f3e6460b3474cf2711f7b4a1f12be0bac9ec4 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 25 Apr 2018 18:24:00 -0400
Subject: [PATCH] Add computation transitivity, some sanity checking
---
code/gcbpv.agda | 33 +++++++++++++++++++++++++++++++++
1 file changed, 33 insertions(+)
diff --git a/code/gcbpv.agda b/code/gcbpv.agda
index 92cf7c5..44280d0 100644
--- a/code/gcbpv.agda
+++ b/code/gcbpv.agda
@@ -59,9 +59,14 @@ vtrans Atop Abot p ⟨ Bot ⟩v = Abot ⟨ Bot ⟩v
data CType where
_⇀_ : forall {I} -> VType I -> CType I -> CType I
F : forall {I} -> VType I -> CType I
+ ctrans : forall (Btop : CType onevar) (Bbot : CType onevar) ->
+ Btop ⟨ Bot ⟩c ≡ Bbot ⟨ Top ⟩c ->
+ CType onevar
(A ⇀ B) ⟨ i ⟩c = (A ⟨ i ⟩v) ⇀ (B ⟨ i ⟩c)
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
vrefl : VType (cdot _) -> VType onevar
crefl : CType (cdot _) -> CType onevar
@@ -72,3 +77,31 @@ vrefl (U B) = U (crefl B)
crefl (A ⇀ B) = vrefl A ⇀ crefl B
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 (A × A₁) i = cong₂ _×_ (vreflretract A i) (vreflretract A₁ i)
+vreflretract (U B) i = cong U (creflretract B i)
+
+creflretract (A ⇀ B) i = cong₂ _⇀_ (vreflretract A i) (creflretract B i)
+creflretract (F A) i = cong F (vreflretract A i)
+
+-- | For a more traditional presentation of ordering
+data VLt (A A' : VType (cdot _)) : Set where
+ lt : forall (Aord : VType onevar) -> Aord ⟨ Top ⟩v ≡ A -> Aord ⟨ Bot ⟩v ≡ A' -> VLt A A'
+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))
+
+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))
+
+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₃
--
GitLab