{-# OPTIONS --allow-unsolved-metas #-}
module A201605.AltArtemov.Try3.ProvVec where
open import A201605.AltArtemov.Try3.True public
-- TODO: unfinished
data Prov (Γ : Cx) : ∀ {k n m} → Vec ᵍ⌊ Γ ⌋ k n → Ty m → Set where
var : ∀ {k n} {A : Ty k} →
(x : Var Γ A) →
Prov Γ (VARs {k = k} {n = n} ⁱ⌊ x ⌋) A
lam : ∀ {k k′ n} {A : Ty k} {ts : Vec (suc ᵍ⌊ Γ ⌋) k′ n} {B : Ty k′} →
Prov (Γ , A) ts B →
Prov Γ (LAMs ts) (A ⊃ B)
app : ∀ {k k′ n} {ts₁ : Vec ᵍ⌊ Γ ⌋ 0 n} {ts₂ : Vec ᵍ⌊ Γ ⌋ k n} {A : Ty k} {B : Ty k′} →
Prov Γ ts₁ (A ⊃ B) → Prov Γ ts₂ A →
Prov Γ (APPs {!ts₁!} ts₂) B
pair : ∀ {k k′ n} {ts₁ : Vec ᵍ⌊ Γ ⌋ k n} {A : Ty k} {ts₂ : Vec ᵍ⌊ Γ ⌋ k′ n} {B : Ty k′} →
Prov Γ ts₁ A → Prov Γ ts₂ B →
Prov Γ (PAIRs {!ts₁!} ts₂) (A ∧ B)
fst : ∀ {k k′ n} {ts : Vec ᵍ⌊ Γ ⌋ 0 n} {A : Ty k} {B : Ty k′} →
Prov Γ ts (A ∧ B) →
Prov Γ (FSTs ts) A
snd : ∀ {k k′ n} {ts : Vec ᵍ⌊ Γ ⌋ 0 n} {A : Ty k} {B : Ty k′} →
Prov Γ ts (A ∧ B) →
Prov Γ (SNDs ts) B
up : ∀ {k n} {ts : Vec ᵍ⌊ Γ ⌋ (suc k) n} {u : Tm 0 k} {A : Ty k} →
Prov Γ ts (u ∶ A) →
Prov Γ (UPs ts) ((! u ∶ u ∶ A))
down : ∀ {k n} {ts : Vec ᵍ⌊ Γ ⌋ (suc k) n} {u : Tm 0 k} {A : Ty k} →
Prov Γ ts (u ∶ A) →
Prov Γ (DOWNs ts) A
--ᵗ⌊_⌋ : ∀ {Γ k n m} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k n} → Prov Γ ts A → Tm ᵍ⌊ Γ ⌋ m
--ᵗ⌊ var x ⌋ = VAR ⁱ⌊ x ⌋
--ᵗ⌊ lam j ⌋ = LAM ᵗ⌊ j ⌋
--ᵗ⌊ app j₁ j₂ ⌋ = APP {!ᵗ⌊ j₁ ⌋!} ᵗ⌊ j₂ ⌋
--ᵗ⌊ pair j₁ j₂ ⌋ = PAIR ᵗ⌊ j₁ ⌋ ᵗ⌊ j₂ ⌋
--ᵗ⌊ fst j ⌋ = FST {!ᵗ⌊ j ⌋!}
--ᵗ⌊ snd j ⌋ = SND {!ᵗ⌊ j ⌋!}
--ᵗ⌊ up j ⌋ = {!UP ᵗ⌊ j ⌋!}
--ᵗ⌊ down j ⌋ = DOWN ᵗ⌊ j ⌋
--ᵗ⌊_⌋ {Γ} {n = n} (up {k} j) = subst (Tm ᵍ⌊ Γ ⌋) (suc-plus (suc k) n) (UP ᵗ⌊ j ⌋)
--ᵗ⌊_⌋ {Γ} {n = n} (down {k} j) = DOWN (subst (Tm ᵍ⌊ Γ ⌋) (sym (suc-plus k n)) ᵗ⌊ j ⌋)
-- true⇒ : ∀ {Γ k} {A : Ty k} → True Γ A → Prov Γ [] A
-- true⇒ (var x) = var x
-- true⇒ (lam j) = {!!} -- lam (true⇒ j)
-- true⇒ (app j₁ j₂) = {!!} -- app (true⇒ j₁) (true⇒ j₂)
-- true⇒ (pair j₁ j₂) = {!!} -- pair (true⇒ j₁) (true⇒ j₂)
-- true⇒ (fst j) = {!!} -- fst (true⇒ j)
-- true⇒ (snd j) = snd {!true⇒ j!} -- snd (true⇒ j)
-- true⇒ (up j) = up (true⇒ j)
-- true⇒ (down j) = down (true⇒ j)
-- -- true⇐ : ∀ {Γ k} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k 0} → Prov Γ ts A → True Γ A
-- -- true⇐ (var x) = var x
-- -- true⇐ (lam j) = lam (true⇐ j)
-- -- true⇐ (app j₁ j₂) = app (true⇐ j₁) (true⇐ j₂)
-- -- true⇐ (pair j₁ j₂) = pair (true⇐ j₁) (true⇐ j₂)
-- -- true⇐ (fst j) = fst (true⇐ j)
-- -- true⇐ (snd j) = snd (true⇐ j)
-- -- true⇐ (up j) = up (true⇐ j)
-- -- true⇐ (down j) = down (true⇐ j)
-- -- true⇒⇐-id : ∀ {Γ k} {A : Ty k} (j : True Γ A) → true⇐ (true⇒ j) ≡ j
-- -- true⇒⇐-id (var x) = refl
-- -- true⇒⇐-id (lam j) = cong lam (true⇒⇐-id j)
-- -- true⇒⇐-id (app j₁ j₂) = cong₂ app (true⇒⇐-id j₁) (true⇒⇐-id j₂)
-- -- true⇒⇐-id (pair j₁ j₂) = cong₂ pair (true⇒⇐-id j₁) (true⇒⇐-id j₂)
-- -- true⇒⇐-id (fst j) = cong fst (true⇒⇐-id j)
-- -- true⇒⇐-id (snd j) = cong snd (true⇒⇐-id j)
-- -- true⇒⇐-id (up j) = cong up (true⇒⇐-id j)
-- -- true⇒⇐-id (down j) = cong down (true⇒⇐-id j)
-- -- true⇗ : ∀ {Γ k} {A : Ty k} (j : True Γ A) → Prov Γ [ ᵗ⌊ j ⌋ᵀ ] A
-- -- true⇗ (var x) = var x
-- -- true⇗ (lam j) = lam (true⇗ j)
-- -- true⇗ (app j₁ j₂) = app (true⇗ j₁) (true⇗ j₂)
-- -- true⇗ (pair j₁ j₂) = pair (true⇗ j₁) (true⇗ j₂)
-- -- true⇗ (fst j) = fst (true⇗ j)
-- -- true⇗ (snd j) = snd (true⇗ j)
-- -- true⇗ (up j) = up (true⇗ j)
-- -- true⇗ (down j) = down (true⇗ j)
-- -- true⇙ : ∀ {Γ k n} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k n} → Prov Γ ts A → True Γ A
-- -- true⇙ (var x) = var x
-- -- true⇙ (lam j) = lam (true⇙ j)
-- -- true⇙ (app j₁ j₂) = app (true⇙ j₁) (true⇙ j₂)
-- -- true⇙ (pair j₁ j₂) = pair (true⇙ j₁) (true⇙ j₂)
-- -- true⇙ (fst j) = fst (true⇙ j)
-- -- true⇙ (snd j) = snd (true⇙ j)
-- -- true⇙ (up j) = up (true⇙ j)
-- -- true⇙ (down j) = down (true⇙ j)
-- -- true⇗⇙-id : ∀ {Γ k} {A : Ty k} (j : True Γ A) → true⇙ (true⇗ j) ≡ j
-- -- true⇗⇙-id (var x) = refl
-- -- true⇗⇙-id (lam j) = cong lam (true⇗⇙-id j)
-- -- true⇗⇙-id (app j₁ j₂) = cong₂ app (true⇗⇙-id j₁) (true⇗⇙-id j₂)
-- -- true⇗⇙-id (pair j₁ j₂) = cong₂ pair (true⇗⇙-id j₁) (true⇗⇙-id j₂)
-- -- true⇗⇙-id (fst j) = cong fst (true⇗⇙-id j)
-- -- true⇗⇙-id (snd j) = cong snd (true⇗⇙-id j)
-- -- true⇗⇙-id (up j) = cong up (true⇗⇙-id j)
-- -- true⇗⇙-id (down j) = cong down (true⇗⇙-id j)
-- -- prov⇗ : ∀ {Γ k n} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k n} (j : Prov Γ ts A) →
-- -- Prov Γ (ᵗ⌊ j ⌋ ∷ ts) A
-- -- prov⇗ (var x) = var x
-- -- prov⇗ (lam j) = lam (prov⇗ j)
-- -- prov⇗ (app j₁ j₂) = app (prov⇗ j₁) (prov⇗ j₂)
-- -- prov⇗ (pair j₁ j₂) = pair (prov⇗ j₁) (prov⇗ j₂)
-- -- prov⇗ (fst j) = fst (prov⇗ j)
-- -- prov⇗ (snd j) = snd (prov⇗ j)
-- -- prov⇗ (up j) = up (prov⇗ j)
-- -- prov⇗ (down j) = down (prov⇗ j)
-- -- prov⇙ : ∀ {Γ k n} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k (suc n)} (j : Prov Γ ts A) →
-- -- Prov Γ (tail ts) A
-- -- prov⇙ (var x) = var x
-- -- prov⇙ (lam {ts = ts} j) rewrite tail-LAMs ts = lam (prov⇙ j)
-- -- prov⇙ (app {ts₁ = ts₁} {ts₂} j₁ j₂) rewrite tail-APPs ts₁ ts₂ = app (prov⇙ j₁) (prov⇙ j₂)
-- -- prov⇙ (pair {ts₁ = ts₁} {ts₂} j₁ j₂) rewrite tail-PAIRs ts₁ ts₂ = pair (prov⇙ j₁) (prov⇙ j₂)
-- -- prov⇙ (fst {ts = ts}j) rewrite tail-FSTs ts = fst (prov⇙ j)
-- -- prov⇙ (snd {ts = ts}j) rewrite tail-SNDs ts = snd (prov⇙ j)
-- -- prov⇙ (up {ts = ts}j) rewrite tail-UPs ts = up (prov⇙ j)
-- -- prov⇙ (down {ts = ts}j) rewrite tail-DOWNs ts = down (prov⇙ j)
-- -- prov⇗⇙-id : ∀ {Γ k n} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k n} (j : Prov Γ ts A) →
-- -- prov⇙ (prov⇗ j) ≡ j
-- -- prov⇗⇙-id (var x) = refl
-- -- prov⇗⇙-id (lam j) = cong lam (prov⇗⇙-id j)
-- -- prov⇗⇙-id (app j₁ j₂) = cong₂ app (prov⇗⇙-id j₁) (prov⇗⇙-id j₂)
-- -- prov⇗⇙-id (pair j₁ j₂) = cong₂ pair (prov⇗⇙-id j₁) (prov⇗⇙-id j₂)
-- -- prov⇗⇙-id (fst j) = cong fst (prov⇗⇙-id j)
-- -- prov⇗⇙-id (snd j) = cong snd (prov⇗⇙-id j)
-- -- prov⇗⇙-id (up j) = cong up (prov⇗⇙-id j)
-- -- prov⇗⇙-id (down j) = cong down (prov⇗⇙-id j)
-- -- --prov⋘ : ∀ {Γ k n} {A : Ty (suc k)} {ts : Vec ᵍ⌊ Γ ⌋ (suc k) n} (j : Prov Γ ts A) →
-- -- -- Prov Γ (ts ‘ init A)
-- -- --prov⋘ = ?
-- -- _∴_ : ∀ {Γ k n} (ts : Vec ᵍ⌊ Γ ⌋ k n) (A : Ty k) → Ty (n + k)
-- -- [] ∴ A = A
-- -- (t ∷ ts) ∴ A = t ∶ (ts ∴ A)
-- -- infixr 15 _∴_
-- -- --D : ∀
-- -- -- ren-prov : ∀ {Γ Γ′ k n} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k n} (η : Γ′ ⊇ Γ) → Prov Γ ts A →
-- -- -- Prov Γ′ (ren-vec ʰ⌊ η ⌋ ts) A
-- -- -- ren-prov η (var x) = ? --rewrite ren-VARs ʰ⌊ η ⌋ ⁱ⌊ x ⌋ |
-- -- -- -- °ren-fin-var η x =
-- -- -- --var (ren-var η x)
-- -- -- ren-prov η (lam {ts} j) rewrite ren-LAMs ʰ⌊ η ⌋ ts =
-- -- -- lam (ren-prov (lift η) j)
-- -- -- ren-prov η (app {ts} {us} j₁ j₂) rewrite ren-APPs ʰ⌊ η ⌋ ts us =
-- -- -- app (ren-prov η j₁) (ren-prov η j₂)
-- -- -- ren-prov η (pair {ts} {us} j₁ j₂) rewrite ren-PAIRs ʰ⌊ η ⌋ ts us =
-- -- -- pair (ren-prov η j₁) (ren-prov η j₂)
-- -- -- ren-prov η (fst {ts} j) rewrite ren-FSTs ʰ⌊ η ⌋ ts =
-- -- -- fst (ren-prov η j)
-- -- -- ren-prov η (snd {ts} j) rewrite ren-SNDs ʰ⌊ η ⌋ ts =
-- -- -- snd (ren-prov η j)
-- -- -- ren-prov η (up {ts} j) = ? --rewrite ren-UPs ʰ⌊ η ⌋ ts =
-- -- -- -- up (ren-prov η j)
-- -- -- ren-prov η (down {ts} j) = ? --rewrite ren-DOWNs ʰ⌊ η ⌋ ts =
-- -- -- -- down (ren-prov η j)
-- -- -- wk-prov : ∀ {Γ n A C} {ts : Vec ᵍ⌊ Γ ⌋ n} → Prov Γ ts C →
-- -- -- Prov (Γ , A) (wk-vec ts) C
-- -- -- wk-prov {Γ} rewrite sym (°id Γ) = ren-prov ⊇wk
-- -- -- wk*-prov : ∀ {Γ n C} {ts : Vec 0 n} → Prov ∅ ts C →
-- -- -- Prov Γ (wk*-vec ts) C
-- -- -- wk*-prov {Γ} rewrite sym (°to Γ) = ren-prov ⊇to
-- -- -- v₀ : ∀ {Γ k} {A : Ty k} → Prov (Γ , A) (VARs i₀) A
-- -- -- v₀ = var x₀
-- -- -- v₁ : ∀ {Γ k} {A B : Ty k} → Prov ((Γ , A) , B) (VARs i₁) A
-- -- -- v₁ = var x₁
-- -- -- v₂ : ∀ {Γ k} {A B C : Ty k} → Prov (((Γ , A) , B) , C) (VARs i₂) A
-- -- -- v₂ = var x₂
-- -- -- -- I[_] : ∀ {Γ} n {A} → Prov Γ (LAMs (VARs i₀)) (A ⊃ A)
-- -- -- -- I = lam v₀
-- -- -- -- K[_] : ∀ {Γ} n {A B} → Prov Γ (LAMs (LAMs (VARs i₁))) (A ⊃ B ⊃ A)
-- -- -- -- K = lam (lam v₁)
-- -- -- -- S[_] : ∀ {Γ} n {A B C} →
-- -- -- -- Prov Γ (LAMs (LAMs (LAMs
-- -- -- -- (APPs (APPs (VARs i₂) (VARs i₀))
-- -- -- -- (APPs (VARs i₁) (VARs i₀))))))
-- -- -- -- ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
-- -- -- -- S = lam (lam (lam
-- -- -- -- (app (app v₂ v₀)
-- -- -- -- (app v₁ v₀))))
-- -- -- -- I≡I[0] : ∀ {Γ A} → true⇒ (I {Γ} {A}) ≡ I[ 0 ]
-- -- -- -- I≡I[0] = refl
-- -- -- -- ⇗I≡I[1] : ∀ {Γ A} → true⇗ (I {Γ} {A}) ≡ I[ 1 ]
-- -- -- -- ⇗I≡I[1] = refl
-- -- -- -- ⇗⇗I≡I[2] : ∀ {Γ A} → prov⇗ (true⇗ (I {Γ} {A})) ≡ I[ 2 ]
-- -- -- -- ⇗⇗I≡I[2] = refl