如何在不使用assert_smaller的情况下证明Idris定理的终止性？

我正在使用Idris证明一条定理，证明过程中需要将定理自身应用于假设，但无法直接应用，必须执行重写操作。Idris无法自动证明该定理的终止性，我不得不使用assert_smaller，但assert_smaller类似Coq中的admit，我希望得到完全验证的证明。请问是否可以证明该定理的终止性（或证明相关断言）？相关代码如下，assert_smaller的使用位于定理的第二个分支：

data StType = StTop
            | StTApp StType StType

data StSubtype : StType -> StType -> Type where
    S_Refl : StSubtype t t
    S_Trans : (u: StType) -> StSubtype s u -> StSubtype u t -> StSubtype s t
    S_Top : StSubtype s StTop
    S_Arrow : StSubtype t1 s1 -> StSubtype s2 t2 -> StSubtype (StTApp s1 s2) (StTApp t1 t2)

-- Theorem 
%default total
%unbound_implicits off
theorem1 : (t1, t2, s:  StType) 
        -> StSubtype s (StTApp t1 t2) 
        -> (s1: StType **
                (s2 : StType ** 
                    (s = StTApp s1 s2, 
                     StSubtype t1 s1, 
                     StSubtype s2 t2)))
theorem1 t1 t2 (StTApp t1 t2) S_Refl = (t1 ** (t2 ** (Refl, S_Refl, S_Refl)))
theorem1 t1 t2 s (S_Trans u hyp1 hyp2) = let 
    (s1 ** (s2 ** (ueq, st1, st2))) = theorem1 t1 t2 u hyp2
    hyp1' : StSubtype s (StTApp s1 s2)
    hyp1' = replace {p = id} (cong (StSubtype s) ueq) hyp1
    in case theorem1 s1 s2 s (assert_smaller (S_Trans u hyp1 hyp2) hyp1') of
        (s1' ** (s2' ** (ueq', st1', st2'))) => (s1' ** (s2' ** (ueq', S_Trans s1 st1 st1', S_Trans s2 st2' st2)))
theorem1 t1 t2 (StTApp x1 x2) (S_Arrow hyp1 hyp2) = (x1 ** (x2 ** (Refl, hyp1, hyp2)))

解决方案 #

问题核心在于Idris无法自动识别S_Trans分支中递归调用的终止性，因为重写后的hyp1'与原推导的大小关系不明确。以下是两种完全验证的替代方案：

方案1：基于证明高度的良基递归 #

通过定义StSubtype推导的高度，显式证明递归调用的推导高度严格小于原推导，让Idris确认终止性：

%default total
%unbound_implicits off
import Data.Nat.LTE

data StType = StTop
            | StTApp StType StType

data StSubtype : StType -> StType -> Type where
    S_Refl : StSubtype t t
    S_Trans : (u: StType) -> StSubtype s u -> StSubtype u t -> StSubtype s t
    S_Top : StSubtype s StTop
    S_Arrow : StSubtype t1 s1 -> StSubtype s2 t2 -> StSubtype (StTApp s1 s2) (StTApp t1 t2)

-- 定义推导的高度
height : StSubtype s t -> Nat
height S_Refl = 1
height (S_Trans u h1 h2) = height h1 + height h2 + 1
height S_Top = 1
height (S_Arrow h1 h2) = height h1 + height h2 + 1

-- 辅助函数：显式接受推导高度的上界，证明递归调用的高度更小
theorem1Aux : (n : Nat) -> (t1, t2, s : StType) -> (p : StSubtype s (StTApp t1 t2)) -> 
              LTE (height p) n ->
              (s1 : StType ** (s2 : StType ** (s = StTApp s1 s2, StSubtype t1 s1, StSubtype s2 t2)))
theorem1Aux n t1 t2 (StTApp t1 t2) S_Refl _ = (t1 ** (t2 ** (Refl, S_Refl, S_Refl)))
theorem1Aux n t1 t2 s (S_Trans u hyp1 hyp2) prf = 
    let -- 证明hyp2的高度小于原推导高度
        hyp2_height_le : LTE (height hyp2) (n - height hyp1 - 1)
        hyp2_height_le = LTE.trans (LTE.refl (height hyp2)) (minusLTE n (height hyp1 + 1))
        -- 递归处理hyp2
        (s1 ** (s2 ** (ueq, st1, st2))) = theorem1Aux (n - height hyp1 - 1) t1 t2 u hyp2 hyp2_height_le
        -- 重写得到hyp1'
        hyp1' : StSubtype s (StTApp s1 s2)
        hyp1' = replace {p = \x => StSubtype s x} ueq hyp1
        -- 证明hyp1'的高度小于原推导高度
        hyp1_height_le : LTE (height hyp1') (n - height hyp2 - 1)
        hyp1_height_le = rewrite sym ueq in LTE.trans (LTE.refl (height hyp1)) (minusLTE n (height hyp2 + 1))
        -- 递归处理hyp1'
        (s1' ** (s2' ** (ueq', st1', st2'))) = theorem1Aux (n - height hyp2 - 1) s1 s2 s hyp1' hyp1_height_le
    in (s1' ** (s2' ** (ueq', S_Trans s1 st1 st1', S_Trans s2 st2' st2)))
theorem1Aux n t1 t2 (StTApp x1 x2) (S_Arrow hyp1 hyp2) _ = (x1 ** (x2 ** (Refl, hyp1, hyp2)))
-- 处理不可能的情况：StTop无法成为StTApp的子类型
theorem1Aux n t1 t2 StTop p _ = absurd p

-- 主定理：调用辅助函数，传入推导自身高度作为上界
theorem1 : (t1, t2, s:  StType) 
        -> StSubtype s (StTApp t1 t2) 
        -> (s1: StType **
                (s2 : StType ** 
                    (s = StTApp s1 s2, 
                     StSubtype t1 s1, 
                     StSubtype s2 t2)))
theorem1 t1 t2 s p = theorem1Aux (height p) t1 t2 s p (LTE.refl (height p))

方案2：先证明子类型的结构约束 #

先证明StSubtype s (StTApp t1 t2)时，s不可能是StTop，再通过模式匹配限定s为StTApp类型，让Idris自动识别递归结构：

%default total
%unbound_implicits off

data StType = StTop
            | StTApp StType StType

data StSubtype : StType -> StType -> Type where
    S_Refl : StSubtype t t
    S_Trans : (u: StType) -> StSubtype s u -> StSubtype u t -> StSubtype s t
    S_Top : StSubtype s StTop
    S_Arrow : StSubtype t1 s1 -> StSubtype s2 t2 -> StSubtype (StTApp s1 s2) (StTApp t1 t2)

-- 引理：StTop不可能是StTApp的子类型
subtypeAppNotTop : StSubtype s (StTApp t1 t2) -> s /= StTop
subtypeAppNotTop S_Refl = absurd Refl
subtypeAppNotTop (S_Trans u hyp1 hyp2) = \eq => subtypeAppNotTop hyp2 (trans eq Refl)
subtypeAppNotTop S_Top = absurd Refl
subtypeAppNotTop (S_Arrow hyp1 hyp2) = absurd Refl

-- 主定理：模式匹配s为StTApp，排除StTop的情况
theorem1 : (t1, t2, s:  StType) 
        -> StSubtype s (StTApp t1 t2) 
        -> (s1: StType **
                (s2 : StType ** 
                    (s = StTApp s1 s2, 
                     StSubtype t1 s1, 
                     StSubtype s2 t2)))
theorem1 t1 t2 (StTApp t1 t2) S_Refl = (t1 ** (t2 ** (Refl, S_Refl, S_Refl)))
theorem1 t1 t2 (StTApp s1 s2) (S_Trans u hyp1 hyp2) = 
    let (u1 ** (u2 ** (ueq, st1, st2))) = theorem1 t1 t2 u hyp2
        hyp1' : StSubtype (StTApp s1 s2) (StTApp u1 u2)
        hyp1' = replace {p = \x => StSubtype (StTApp s1 s2) x} ueq hyp1
        -- 此时递归调用的目标是StTApp u1 u2，s是StTApp s1 s2，结构递归明确
        (s1' ** (s2' ** (ueq', st1', st2'))) = theorem1 u1 u2 (StTApp s1 s2) hyp1'
    in (s1' ** (s2' ** (ueq', S_Trans u1 st1 st1', S_Trans u2 st2' st2)))
theorem1 t1 t2 (StTApp x1 x2) (S_Arrow hyp1 hyp2) = (x1 ** (x2 ** (Refl, hyp1, hyp2)))
-- 排除StTop的情况
theorem1 t1 t2 StTop p = absurd (subtypeAppNotTop p Refl)

内容的提问来源于stack exchange，提问作者Henrique Guerra