agda - 证明子类型、终止检查、`subst` 的反转引理

Question

我试图证明来自Types and Programming Languages的（第一部分）子类型引理。这是我到目前为止所拥有的：

data Type : Set where
  _=>_ : Type → Type → Type
  Top : Type

data _<:_ : Type → Type → Set where
  s-refl : {S : Type} → S <: S
  s-trans : {S T U : Type} → S <: U → U <: T → S <: T
  s-top : {S : Type} → S <: Top
  s-arrow : {S₁ S₂ T₁ T₂ : Type} → T₁ <: S₁ → S₂ <: T₂ → S₁ => S₂ <: T₁ => T₂

lemma-inversion₁ : {S T₁ T₂ : Type}                                                                                                                                 
  → S <: T₁ => T₂                                                                                                                                                   
  → ∃[ (S₁ × S₂) ∈ (Type & Type) ] ((S ≡ (S₁ => S₂)) & (T₁ <: S₁) & (S₂ <: T₂))                                                                                     
lemma-inversion₁ (s-refl {T₁ => T₂}) = (T₁ × T₂) , (refl × s-refl × s-refl)                                                                                         
lemma-inversion₁ (s-arrow {S₁} {S₂} T₁&lt;:S₁ S₂&lt;∶T₂) = (S₁ × S₂) , (refl × T₁&lt;:S₁ × S₂&lt;∶T₂)                                                                           
lemma-inversion₁ (s-trans {S} S<:U U<:T₁=>T₂) with lemma-inversion₁ U<:T₁=>T₂                                                                                       
... | (U₁ × U₂) , (U≡U₁=>U₂ × T₁&lt;:U₁ × U₂&lt;:T₂) with lemma-inversion₁ (subst (S <:_) U≡U₁=>U₂ S<:U)                                                                  
... | (S₁ × S₂) , (S≡S₁=>S₂ × U₂&lt;:S₁ × S₂&lt;:U₂) = (S₁ × S₂) , (S≡S₁=>S₂ × s-trans T₁&lt;:U₁ U₂&lt;:S₁ × s-trans S₂&lt;:U₂ U₂&lt;:T₂)                                             

这对我来说看起来是正确的，但我得到：

Termination checking failed for the following functions:                                                                                                            
  lemma-inversion₁                                                                                                                                                  
Problematic calls:                                                                                                                                                  
  lemma-inversion₁ (s-trans S<:U U<:T₁=>T₂)                                                                                                                         
  | lemma-inversion₁ U<:T₁=>T₂                                                                                                                                      
  lemma-inversion₁ U<:T₁=>T₂
  lemma-inversion₁ (subst (_<:_ S) U≡U₁=>U₂ S<:U)                                                                                                                   

看起来 Agda 无法推断终止，因为subst? 是对的吗？有解决方法吗？

标签： agda

Answer 1