向Agda證明我們正在談論同樣的事

Question

我試圖證明一個矛盾，但我遇到了一個問題，試圖向Agda證明由<>-wt-inv返回的西格瑪域類型與所看到的相同西格瑪在證明之前。 我希望uniq型證明能夠幫助我，但我無法將它們放在一起。

我希望下面的代碼中的註釋給出足夠的上下文。

-- given a type for (f ⟨⟩), we can derive that f is a function type 
-- and we can prove that the context yields σ 
⟨⟩-wt-inv : ∀ {n m f τ} {K : Ktx n m} → K ⊢ (f ⟨⟩) ∶ τ → 
      ∃ λ σ → K Δ↝ σ × K ⊢ f ∶ (σ ⇒ τ) 
⟨⟩-wt-inv (_⟨_⟩ {τ = σ} K⊢f∶σ⇒τ KΔ↝σ) = σ , (KΔ↝σ , K⊢f∶σ⇒τ) 

uniq-type : ∀ {n m} {K : Ktx n m} {t τ τ'} → K ⊢ t ∶ τ → K ⊢ t ∶ τ' → τ ≡ τ' 

-- excerpt from the typeof decision procedure 
typeof : ∀ {n m} (K : Ktx n m) t → Dec (HasType K t) 
typeof (Γ , Δ) (f ⟨⟩) with typeof (Γ , Δ) f 
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , _)  with (Δ-resolve (Γ , Δ) σ) 
typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , f∶φ) | no KΔ↝̸σ = 
    -- I'm trying to derive a contraction based on the fact that we've proven that 
    -- K Δ↝̸ σ, but assuming a type for (f ⟨⟩) will yield an instance of K Δ↝ σ' (see ⟨⟩-wt-inv) 
    -- the problem is that I don't know how to make agda see that σ' ≡ σ 
    -- such that the following typechecks. 
    -- (while agda will now complain that the σ in the wt-inv is not the 
    same one as used in the KΔ↝̸σ instance, which is sensible) 
    -- I think I have to use the uniq-type prove on f somewhere... 
    no $ KΔ↝̸σ ∘ proj₁ ∘ proj₂ ⟨⟩-wt-inv ∘ proj₂ 

任何幫助表示讚賞

Answer 1

Saizan在#agda通道還跟點我在正確的方向：使用功能subst在使用一個平等的證明「替身」爲σσ」證明我必須從KΔ↝σ'獲得KΔ↝σ的實例：

typeof (Γ , Δ) (f ⟨⟩) | yes (σ ⇒ τ , f∶φ) | no KΔ↝̸σ = 
    no $ KΔ↝̸σ ∘ helper 
    where 
     helper : (HasType (Γ , Δ) (f ⟨⟩)) → (Γ , Δ) Δ↝ σ 
     helper p with (⟨⟩-wt-inv ∘ proj₂) p 
     helper p | (σ' , KΔ↝σ' , f∶φ') = subst (λ s → (Γ , Δ) Δ↝ s) σ'≡σ KΔ↝σ' 
     where 
      σ'≡σ : σ' ≡ σ 
      σ'≡σ = ≡⇒dom $ uniq-type f∶φ' f∶φ