{-# OPTIONS --copatterns --sized-types #-}
module SAT3 where
open import Library
open import SizedInfiniteTypes
open import Terms
open import Substitution
open import Reduction
open import SN
open import SN.AntiRename
TmSet : (a : Ty) → Set₁
TmSet a = {Γ : Cxt} (t : Tm Γ a) → Set
_⊆_ : ∀{a} (𝑨 𝑨′ : TmSet a) → Set
𝑨 ⊆ 𝑨′ = ∀{Γ}{t : Tm Γ _} → 𝑨 t → 𝑨′ t
Closed : ∀ (n : ℕ) {a} (𝑨 : TmSet a) → Set
Closed n 𝑨 = ∀{Γ}{t t' : Tm Γ _} → t ⟨ n ⟩⇒ t' → 𝑨 t' → 𝑨 t
data Cl (n : ℕ) {a} (𝑨 : TmSet a) {Γ} (t : Tm Γ a) : Set where
emb : 𝑨 t → Cl n 𝑨 t
exp : ∀{t'} → t ⟨ n ⟩⇒ t' → Cl n 𝑨 t' → Cl n 𝑨 t
_[→]_ : ∀{a b} → TmSet a → TmSet b → TmSet (a →̂ b)
(𝓐 [→] 𝓑) {Γ} t = ∀{Δ} (ρ : Δ ≤ Γ) → {u : Tm Δ _} → 𝓐 u → 𝓑 (app (rename ρ t) u)
_[×]_ : ∀{a b} → TmSet a → TmSet b → TmSet (a ×̂ b)
(𝓐 [×] 𝓑) t = 𝓐 (fst t) × 𝓑 (snd t)
data [▸] {a∞} (𝑨 : TmSet (force a∞)) {Γ} : (n : ℕ) → Tm Γ (▸̂ a∞) → Set where
▹0 : ∀ {t : Tm Γ (force a∞)} → [▸] 𝑨 zero (▹ t)
▹_ : ∀{n}{t : Tm Γ (force a∞)} (𝒕 : 𝑨 t) → [▸] 𝑨 (suc n) (▹ t)
ne : ∀{n}{t : Tm Γ (▸̂ a∞)} (𝒏 : SNe n t) → [▸] 𝑨 n t
exp : ∀{n}{t t' : Tm Γ (▸̂ a∞)} (t⇒ : t ⟨ n ⟩⇒ t') (𝒕 : [▸] 𝑨 n t') → [▸] 𝑨 n t
record IsSAT (n : ℕ) {a} (𝑨 : TmSet a) : Set where
field
satSNe : SNe n ⊆ 𝑨
satSN : 𝑨 ⊆ SN n
satExp : Closed n 𝑨
satRename : ∀ {Γ Δ} → (ρ : Ren Γ Δ) → ∀ {t} → 𝑨 t → 𝑨 (subst ρ t)
record SAT (a : Ty) (n : ℕ) : Set₁ where
field
satSet : TmSet a
satProp : IsSAT n satSet
open IsSAT satProp public
open SAT
SAT≤ : (a : Ty) (n : ℕ) → Set₁
SAT≤ a n = ∀ {m} → (m ≤ℕ n) → SAT a m
module SAT≤ {a : Ty} {n : ℕ} (𝓐 : SAT≤ a n) {m} (m≤n : m ≤ℕ _) where
open SAT (𝓐 m≤n) public
record _∈_ {a n Γ} (t : Tm Γ a) (𝓐 : SAT a n) : Set where
constructor ↿_
field ⇃_ : satSet 𝓐 t
open _∈_ public
_∈⟨_⟩_ : ∀ {a n Γ} (t : Tm Γ a) {m} (m≤n : m ≤ℕ n) (𝓐 : SAT≤ a n) → Set
t ∈⟨ m≤n ⟩ 𝓐 = t ∈ (𝓐 m≤n)
_⟦→⟧_ : ∀ {n a b} (𝓐 : SAT≤ a n) (𝓑 : SAT≤ b n) → SAT (a →̂ b) n
𝓐 ⟦→⟧ 𝓑 = record
{ satSet = 𝑪
; satProp = record
{ satSNe = CSNe
; satSN = CSN
; satExp = CExp
; satRename = λ ρ {t} 𝒕 m m≤n ρ₁ {u} 𝒖 → ≡.subst (λ t₁ → 𝑩 {m} m≤n (app t₁ u)) (subst-∙ ρ₁ ρ t) (𝒕 m m≤n (λ x₂ → ρ₁ (ρ x₂)) 𝒖)
}
}
where
module 𝓐 = SAT≤ 𝓐
module 𝓑 = SAT≤ 𝓑
𝑨 = 𝓐.satSet
𝑩 = 𝓑.satSet
𝑪 : TmSet (_ →̂ _)
𝑪 t = ∀ m (m≤n : m ≤ℕ _) → (𝑨 m≤n [→] 𝑩 m≤n) t
CSNe : SNe _ ⊆ 𝑪
CSNe 𝒏 m m≤n ρ 𝒖 = 𝓑.satSNe m≤n (sneApp (mapSNe m≤n (renameSNe ρ 𝒏)) (𝓐.satSN m≤n 𝒖))
CSN : 𝑪 ⊆ SN _
CSN 𝒕 = unRenameSN (prop→Ind suc ≡.refl) (absVarSN (𝓑.satSN ≤ℕ.refl (𝒕 _ ≤ℕ.refl suc (𝓐.satSNe ≤ℕ.refl (var v₀)))))
CExp : ∀{Γ}{t t' : Tm Γ _} → t ⟨ _ ⟩⇒ t' → 𝑪 t' → 𝑪 t
CExp t⇒ 𝒕 m m≤n ρ 𝒖 = 𝓑.satExp m≤n ((cong (appl _) (appl _) (map⇒ m≤n (subst⇒ (renSN ρ) t⇒)))) (𝒕 m m≤n ρ 𝒖)
⟦abs⟧ : ∀{n a b}{𝓐 : SAT≤ a n}{𝓑 : SAT≤ b n}{Γ}{t : Tm (a ∷ Γ) b} →
(∀ {m} (m≤n : m ≤ℕ n) {Δ} (ρ : Δ ≤ Γ) {u : Tm Δ a} →
u ∈⟨ m≤n ⟩ 𝓐 → (subst0 u (subst (lifts ρ) t)) ∈⟨ m≤n ⟩ 𝓑 ) → abs t ∈ (𝓐 ⟦→⟧ 𝓑)
(⇃ ⟦abs⟧ {𝓐 = 𝓐}{𝓑 = 𝓑} 𝒕) m m≤n ρ 𝒖 =
SAT≤.satExp 𝓑 m≤n (β (SAT≤.satSN 𝓐 m≤n 𝒖)) (⇃ 𝒕 m≤n ρ (↿ 𝒖))
⟦app⟧ : ∀ {n a b}{𝓐 : SAT≤ a n}{𝓑 : SAT≤ b n}{Γ}{t : Tm Γ (a →̂ b)}{u : Tm Γ a} →
∀ {m} (m≤n : m ≤ℕ n) → t ∈ (𝓐 ⟦→⟧ 𝓑) → u ∈⟨ m≤n ⟩ 𝓐 → app t u ∈⟨ m≤n ⟩ 𝓑
⟦app⟧ {𝓑 = 𝓑} {u = u} m≤n (↿ 𝒕) (↿ 𝒖) = ≡.subst (λ t → app t u ∈⟨ m≤n ⟩ 𝓑) renId (↿ 𝒕 _ m≤n id 𝒖)
_⟦×⟧_ : ∀ {n a b} (𝓐 : SAT a n) (𝓑 : SAT b n) → SAT (a ×̂ b) n
𝓐 ⟦×⟧ 𝓑 = record
{ satSet = 𝑪
; satProp = record
{ satSNe = CSNe
; satSN = CSN
; satExp = CExp
; satRename = λ ρ x → satRename 𝓐 ρ (proj₁ x) , satRename 𝓑 ρ (proj₂ x)
}
}
where
𝑨 = satSet 𝓐
𝑩 = satSet 𝓑
𝑪 : TmSet _
𝑪 = 𝑨 [×] 𝑩
CSNe : SNe _ ⊆ 𝑪
CSNe 𝒏 = SAT.satSNe 𝓐 (elim 𝒏 fst)
, SAT.satSNe 𝓑 (elim 𝒏 snd)
CSN : 𝑪 ⊆ SN _
CSN (𝒕₁ , 𝒕₂) = bothProjSN (SAT.satSN 𝓐 𝒕₁) (SAT.satSN 𝓑 𝒕₂)
CExp : ∀{Γ}{t t' : Tm Γ _} → t ⟨ _ ⟩⇒ t' → 𝑪 t' → 𝑪 t
CExp t⇒ (𝒕₁ , 𝒕₂) = SAT.satExp 𝓐 (cong fst fst t⇒) 𝒕₁
, SAT.satExp 𝓑 (cong snd snd t⇒) 𝒕₂
⟦pair⟧ : ∀ {n a b} {𝓐 : SAT a n} {𝓑 : SAT b n} {Γ} {t₁ : Tm Γ a} {t₂ : Tm Γ b}
→ t₁ ∈ 𝓐 → t₂ ∈ 𝓑 → pair t₁ t₂ ∈ (𝓐 ⟦×⟧ 𝓑)
⇃ ⟦pair⟧ {𝓐 = 𝓐} {𝓑 = 𝓑} (↿ 𝒕₁) (↿ 𝒕₂) = satExp 𝓐 (βfst (satSN 𝓑 𝒕₂)) 𝒕₁ , satExp 𝓑 (βsnd (satSN 𝓐 𝒕₁)) 𝒕₂
⟦fst⟧ : ∀ {n a b} {𝓐 : SAT a n} {𝓑 : SAT b n} {Γ} {t : Tm Γ (a ×̂ b)}
→ t ∈ (𝓐 ⟦×⟧ 𝓑) → fst t ∈ 𝓐
⟦fst⟧ 𝒕 = ↿ (proj₁ (⇃ 𝒕))
⟦snd⟧ : ∀ {n a b} {𝓐 : SAT a n} {𝓑 : SAT b n} {Γ} {t : Tm Γ (a ×̂ b)}
→ t ∈ (𝓐 ⟦×⟧ 𝓑) → snd t ∈ 𝓑
⟦snd⟧ 𝒕 = ↿ (proj₂ (⇃ 𝒕))
SATpred : (a : Ty) (n : ℕ) → Set₁
SATpred a zero = ⊤
SATpred a (suc n) = SAT a n
SATpredSet : {n : ℕ}{a : Ty} → SATpred a n → TmSet a
SATpredSet {zero} 𝓐 _ = ⊤
SATpredSet {suc n} 𝓐 = satSet 𝓐
module _ {a∞ : ∞Ty} where
private
a = force a∞
𝑪 : ∀{n} (𝓐 : SATpred a n) → TmSet (▸̂ a∞)
𝑪 {n} 𝓐 = [▸] (SATpredSet 𝓐) n
CSN : ∀ {n} (𝓐 : SATpred a n) → 𝑪 {n} 𝓐 ⊆ SN n
CSN 𝓐 ▹0 = ▹0
CSN 𝓐 (▹ 𝒕) = ▹ satSN 𝓐 𝒕
CSN 𝓐 (ne 𝒏) = ne 𝒏
CSN 𝓐 (exp t⇒ 𝒕) = exp t⇒ (CSN 𝓐 𝒕)
CRen : ∀ {n} (𝓐 : SATpred a n) → ∀ {Γ Δ} (ρ : Γ ≤ Δ) → ∀ {t} → 𝑪 {n} 𝓐 t → 𝑪 {n} 𝓐 (subst ρ t)
CRen 𝓐 ρ ▹0 = ▹0
CRen 𝓐 ρ (▹ 𝒕) = ▹ satRename 𝓐 ρ 𝒕
CRen 𝓐 ρ (ne 𝒏) = ne (substSNe (ρ , (λ x → var (ρ x))) 𝒏)
CRen 𝓐 ρ (exp t⇒ 𝒕) = exp (subst⇒ (ρ , (λ x → var (ρ x))) t⇒) (CRen 𝓐 ρ 𝒕)
⟦▸⟧_ : ∀{n} (𝓐 : SATpred a n) → SAT (▸̂ a∞) n
⟦▸⟧_ {n} 𝓐 = record
{ satSet = 𝑪 𝓐
; satProp = record
{ satSNe = ne
; satSN = CSN 𝓐
; satExp = exp
; satRename = CRen 𝓐
}
}