如何在Agda中证明scanr基本性质？分支推理问题求助

我在Agda中证明scanr函数的首元素性质时，卡在了分支推理环节。虽然逻辑上看似简单，但实际实现有难度。以下是我当前的代码：

open import Data.List using (List; []; _∷_; [_]; _++_; foldl; foldr; map; scanl; scanr)
open import Data.Bool using (Bool; true; false)
𝔹-contra : false ≡ true → ∀{ℓ} {P : Set ℓ} → P
𝔹-contra ()

is-empty : ∀{A : Set} → (xs : List A) → Bool
is-empty [] = true
is-empty (x ∷ xs) = false

scanr-not-empty : {A B : Set} (f : A → B → B) (e : B) (xs : List A) → is-empty (scanr f e xs) ≡ false
scanr-not-empty f e [] = refl
scanr-not-empty f e (x ∷ xs) with scanr f e xs in p'
... | []     = 𝔹-contra (trans (sym (scanr-not-empty f e xs)) (cong is-empty p'))
... | y ∷ ys = refl

listFir : {A : Set} (xs : List A) → is-empty xs ≡ false → A
listFir (x ∷ xs) p = x
scanFir : {A B : Set} (f : A → B → B) (e : B) (xs : List A) → B 
scanFir f e xs = listFir (scanr f e xs) (scanr-not-empty f e xs)

scanFi : {A B : Set} (f : A → B → B) (e : B) (x : A) (xs : List A) → 
  scanFir f e (x ∷ xs) ≡ f x (scanFir f e xs)
scanFi f e x xs = {!!}

标准库中scanr的定义如下：

scanr : (A → B → B) → B → List A → List B
scanr f e []       = e ∷ []
scanr f e (x ∷ xs) with scanr f e xs
... | []     = []                -- dead branch
... | y ∷ ys = f x y ∷ y ∷ ys

恳请指导该证明的实现思路，尤其是分支推理的处理方法。我是Agda新手，感谢帮助！

解决思路 #

要证明scanFi，核心是利用你已经证明的scanr-not-empty引理排除scanr定义中的死分支（即scanr f e xs等于[]的情况），具体步骤如下：

1. 拆分scanr f e xs的结构：在scanFi的证明中，用with语句对scanr f e xs进行模式匹配，结合scanr-not-empty引理可直接排除[]分支——因为该引理已证明scanr f e xs不可能是空列表，此分支可通过𝔹-contra直接消去。
2. 展开scanFir定义：当scanr f e xs匹配到y ∷ ys时，分别展开等式两边的scanFir：
   • 左边scanFir f e (x ∷ xs)对应的scanr结果是f x y ∷ y ∷ ys，listFir取首元素即为f x y；
   • 右边f x (scanFir f e xs)中的scanFir f e xs就是listFir (y ∷ ys) _，也就是y，代入后结果为f x y；
   • 两边值完全相等，用refl即可完成证明。

最终的scanFi实现代码如下：

scanFi : {A B : Set} (f : A → B → B) (e : B) (x : A) (xs : List A) → 
  scanFir f e (x ∷ xs) ≡ f x (scanFir f e xs)
scanFi f e x xs with scanr f e xs | scanr-not-empty f e xs
... | []     = 𝔹-contra -- 利用引理排除死分支
... | y ∷ ys = refl

补充说明 #

• 用with同时携带scanr f e xs和scanr-not-empty f e xs，能让Agda自动利用引理排除空列表情况，无需额外等式推导；
• 匹配到y ∷ ys时，scanFir的展开结果直接对应scanr定义中的首元素逻辑，refl即可完成证明。

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