{-# OPTIONS --allow-unsolved-metas #-}
module A201605.AltArtemov.Old.Common.Prov.VecWithReset where
open import A201605.AltArtemov.Old.Common.True.WithReset public
data Prov (Γ : Cx) : ∀ {k n} → Vec ᵍ⌊ Γ ⌋ k n → Ty k → Set where
var : ∀ {k n} {A : Ty k} (x : Var Γ A) →
Prov Γ (VARs {k = k} {n = n} ⁱ⌊ x ⌋) A
lam : ∀ {k n} {ts : Vec (suc ᵍ⌊ Γ ⌋) k n} {A B : Ty k} → Prov (Γ , A) ts B →
Prov Γ (LAMs ts) {!A ⊃ B!}
app : ∀ {k n} {ts₁ ts₂ : Vec ᵍ⌊ Γ ⌋ k n} {A B : Ty k} → Prov Γ ts₁ {!A ⊃ B!} → Prov Γ ts₂ A →
Prov Γ (APPs ts₁ ts₂) B
pair : ∀ {k n} {ts₁ ts₂ : Vec ᵍ⌊ Γ ⌋ k n} {A B : Ty k} → Prov Γ ts₁ A → Prov Γ ts₂ B →
Prov Γ (PAIRs ts₁ ts₂) {!A ∧ B!}
fst : ∀ {k n} {ts : Vec ᵍ⌊ Γ ⌋ k n} {A B : Ty k} → Prov Γ ts {!A ∧ B!} →
Prov Γ (FSTs ts) A
snd : ∀ {k n} {ts : Vec ᵍ⌊ Γ ⌋ k n} {A 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} {A : Ty k} {ts : Vec ᵍ⌊ Γ ⌋ k n} → Prov Γ ts A → Tm ᵍ⌊ Γ ⌋ (n + k)
ᵗ⌊ 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 ⌋
ᵗ⌊_⌋ {Γ} {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)
-- 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