open import Definition.Typed.Restrictions
module Definition.Typed.Consequences.DerivedRules
{a} {M : Set a}
(R : Type-restrictions M)
where
open Type-restrictions R
open import Tools.Fin
open import Tools.Function
open import Tools.Product
import Tools.PropositionalEquality as PE
import Definition.Typed.Consequences.Stability R as S
open import Definition.Typed R
open import Definition.Typed.Consequences.DerivedRules.Sigma R public
open import Definition.Typed.Consequences.DerivedRules.Nat R public
open import Definition.Typed.Consequences.Injectivity R
open import Definition.Typed.Consequences.Inversion R
open import Definition.Typed.Consequences.Syntactic R
open import Definition.Typed.Properties R
open import Definition.Typed.Weakening R as W hiding (wk)
open import Definition.Untyped M hiding (_∷_)
open import Definition.Untyped.Properties M
private variable
Γ : Con Term _
A B C D t u : Term _
p p′ p″ q r : M
b : BinderMode
lam-cong :
Γ ∙ A ⊢ t ≡ u ∷ B →
Π-allowed p q →
Γ ⊢ lam p t ≡ lam p u ∷ Π p , q ▷ A ▹ B
lam-cong {B = B} t≡u ok = η-eq ⊢A (lamⱼ ⊢A ⊢t ok) (lamⱼ ⊢A ⊢u ok) $
_⊢_≡_∷_.trans
(PE.subst (_ ⊢ _ ≡ _ ∷_)
(wkSingleSubstId _)
(β-red A⊢A A∙A⊢B (wkTerm ρ ⊢∙A∙A ⊢t) (var ⊢∙A here)
PE.refl ok)) $
_⊢_≡_∷_.trans
(PE.subst₂ (_ ⊢_≡_∷ _)
(PE.sym (wkSingleSubstId _))
(PE.sym (wkSingleSubstId _))
t≡u) $
_⊢_≡_∷_.sym $
PE.subst (_ ⊢ _ ≡ _ ∷_)
(wkSingleSubstId _)
(β-red A⊢A A∙A⊢B (wkTerm ρ ⊢∙A∙A ⊢u) (var ⊢∙A here) PE.refl ok)
where
ρ = lift (step id)
⊢t = syntacticEqTerm t≡u .proj₂ .proj₁
⊢u = syntacticEqTerm t≡u .proj₂ .proj₂
⊢B = syntacticEqTerm t≡u .proj₁
⊢∙A = wf ⊢B
⊢A = case ⊢∙A of λ where
(_ ∙ ⊢A) → ⊢A
A⊢A = W.wk (step id) ⊢∙A ⊢A
⊢∙A∙A = ⊢∙A ∙ A⊢A
A∙A⊢B = W.wk (lift (step id)) ⊢∙A∙A ⊢B
inversion-lam′ :
Γ ⊢ lam p t ∷ Π q , r ▷ A ▹ B →
Γ ∙ A ⊢ t ∷ B × p PE.≡ q × Π-allowed q r
inversion-lam′ ⊢lam =
case inversion-lam ⊢lam of λ {
(_ , _ , _ , _ , ⊢t , ≡ΠΣ , ok) →
case ΠΣ-injectivity ≡ΠΣ of λ {
(A≡ , B≡ , PE.refl , PE.refl , _) →
conv (S.stabilityTerm (S.reflConEq (wfTerm ⊢lam) S.∙ sym A≡) ⊢t)
(sym B≡) ,
PE.refl ,
ok }}
wk1-lam∘0⇒ :
Γ ⊢ lam p t ∷ Π q , r ▷ A ▹ B →
Γ ∙ A ⊢ wk1 (lam p t) ∘⟨ p ⟩ var x0 ⇒ t ∷ B
wk1-lam∘0⇒ {p = p} {t = t} ⊢lam =
case inversion-lam′ ⊢lam of λ {
(⊢t , PE.refl , ok) →
let ⊢ΓA = wfTerm ⊢t
ΓA⊢A = case ⊢ΓA of λ {
(_ ∙ ⊢A) → W.wk (step id) ⊢ΓA ⊢A }
⊢ΓAA = ⊢ΓA ∙ ΓA⊢A
in PE.subst₂ (_ ⊢ wk1 (lam p t) ∘⟨ p ⟩ var x0 ⇒_∷_)
(wkSingleSubstId _)
(wkSingleSubstId _)
(β-red ΓA⊢A
(W.wk (lift (step id)) ⊢ΓAA (syntacticTerm ⊢t))
(wkTerm (lift (step id)) ⊢ΓAA ⊢t)
(var ⊢ΓA here) PE.refl ok) }
wk1-lam∘0≡ :
Γ ⊢ lam p t ∷ Π q , r ▷ A ▹ B →
Γ ∙ A ⊢ wk1 (lam p t) ∘⟨ p ⟩ var x0 ≡ t ∷ B
wk1-lam∘0≡ ⊢lam = subsetTerm (wk1-lam∘0⇒ ⊢lam)
lam-cong⁻¹ :
Γ ⊢ lam p t ≡ lam p u ∷ Π p , q ▷ A ▹ B →
Γ ∙ A ⊢ t ≡ u ∷ B × Π-allowed p q
lam-cong⁻¹
{Γ = Γ} {p = p} {t = t} {u = u} {q = q} {A = A} {B = B} lam-t≡lam-u = $⟨ lam-t≡lam-u ⟩
Γ ⊢ lam p t ≡ lam p u ∷ Π p , q ▷ A ▹ B →⟨ wkEqTerm (step id) ⊢ΓA ⟩
Γ ∙ A ⊢ wk1 (lam p t) ≡ wk1 (lam p u) ∷ wk1 (Π p , q ▷ A ▹ B) →⟨ flip app-cong (refl (var ⊢ΓA here)) ⟩
Γ ∙ A ⊢ wk1 (lam p t) ∘⟨ p ⟩ var x0 ≡ wk1 (lam p u) ∘⟨ p ⟩ var x0 ∷
wk (lift (step id)) B [ var x0 ]₀ →⟨ PE.subst (_ ⊢ _ ≡ _ ∷_) (wkSingleSubstId _) ⟩
Γ ∙ A ⊢ wk1 (lam p t) ∘⟨ p ⟩ var x0 ≡ wk1 (lam p u) ∘⟨ p ⟩ var x0 ∷ B →⟨ (λ hyp → trans
(sym (wk1-lam∘0≡ ⊢lam-t))
(trans hyp (wk1-lam∘0≡ ⊢lam-u))) ⟩
Γ ∙ A ⊢ t ≡ u ∷ B →⟨ _, ok ⟩
Γ ∙ A ⊢ t ≡ u ∷ B × Π-allowed p q □
where
⊢Γ = wfEqTerm lam-t≡lam-u
⊢A = inversion-ΠΣ (syntacticEqTerm lam-t≡lam-u .proj₁) .proj₁
⊢ΓA = ⊢Γ ∙ ⊢A
⊢lam-t = syntacticEqTerm lam-t≡lam-u .proj₂ .proj₁
⊢lam-u = syntacticEqTerm lam-t≡lam-u .proj₂ .proj₂
ok = inversion-lam′ ⊢lam-t .proj₂ .proj₂
lam-injective :
Γ ⊢ lam p t ≡ lam p′ u ∷ Π p″ , q ▷ A ▹ B →
p PE.≡ p′ × Γ ∙ A ⊢ t ≡ u ∷ B × Π-allowed p q × p′ PE.≡ p″
lam-injective
{Γ = Γ} {p = p} {t = t} {p′ = p′} {u = u} {p″ = p″} {q = q}
{A = A} {B = B} lam-t≡lam-u =
case syntacticEqTerm lam-t≡lam-u of λ {
(_ , ⊢lam₁ , ⊢lam₂) →
case inversion-lam′ ⊢lam₁ of λ {
(_ , PE.refl , _) →
case inversion-lam′ ⊢lam₂ of λ {
(_ , PE.refl , _) →
case lam-cong⁻¹ lam-t≡lam-u of λ {
(t≡u , ok) →
PE.refl , t≡u , ok , PE.refl }}}}
Π-η :
Γ ⊢ t ∷ Π p , q ▷ A ▹ B →
Γ ⊢ lam p (wk1 t ∘⟨ p ⟩ var x0) ≡ t ∷ Π p , q ▷ A ▹ B
Π-η {Γ = Γ} {t = t} {p = p} {q = q} {A = A} {B = B} ⊢t = η-eq
⊢A
⊢lam
⊢t
( $⟨ ⊢lam ⟩
Γ ⊢ lam p (wk1 t ∘⟨ p ⟩ var x0) ∷ Π p , q ▷ A ▹ B →⟨ wk1-lam∘0≡ ⟩
Γ ∙ A ⊢
wk1 (lam p (wk1 t ∘⟨ p ⟩ var x0)) ∘⟨ p ⟩ var x0 ≡
wk1 t ∘⟨ p ⟩ var x0 ∷
B □)
where
⊢A,ok = inversion-ΠΣ (syntacticTerm ⊢t)
⊢A = ⊢A,ok .proj₁
ok = ⊢A,ok .proj₂ .proj₂
⊢ΓA = wfTerm ⊢t ∙ ⊢A
⊢lam = $⟨ wkTerm (step id) ⊢ΓA ⊢t ∘ⱼ var ⊢ΓA here ⟩
Γ ∙ A ⊢ wk1 t ∘⟨ p ⟩ var x0 ∷ wk (lift (step id)) B [ var x0 ]₀ →⟨ PE.subst (_ ⊢ _ ∷_) (wkSingleSubstId _) ⟩
Γ ∙ A ⊢ wk1 t ∘⟨ p ⟩ var x0 ∷ B →⟨ flip (lamⱼ ⊢A) ok ⟩
Γ ⊢ lam p (wk1 t ∘⟨ p ⟩ var x0) ∷ Π p , q ▷ A ▹ B □
ΠΣ-cong′ : Γ ⊢ A ≡ C
→ Γ ∙ A ⊢ B ≡ D
→ ΠΣ-allowed b p q
→ Γ ⊢ ΠΣ⟨ b ⟩ p , q ▷ A ▹ B ≡ ΠΣ⟨ b ⟩ p , q ▷ C ▹ D
ΠΣ-cong′ A≡C B≡D ok =
ΠΣ-cong (proj₁ (syntacticEq A≡C)) A≡C B≡D ok
Unit-η :
Γ ⊢ t ∷ Unit →
Γ ⊢ star ≡ t ∷ Unit
Unit-η ⊢t = η-unit
(starⱼ (wfTerm ⊢t) (⊢∷Unit→Unit-allowed ⊢t))
⊢t