agda：如何证明Agda中涉及分支推理的`scanr`基本属性？

Question

我正在研究涉及 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

有人可以提供如何处理这个证明的指导，特别是如何处理推理中的分支吗？我对此很陌生，所以提前感谢您的指点！

Answer 1

确实是一个相当烦人的问题。以下是如何让它发挥作用：

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 | scanr-not-empty f e (x ∷ xs)
... | []     | () | ()
... | y ∷ ys | _  | _  = refl

基本上

scanr f e xs

出现在

scanr-not-empty f e xs

和

scanr-not-empty f e (x ∷ xs)

中，因此您必须将它们添加到

with

表达式中，以便

scanr f e xs

能够以与表达式其余部分一致的类型重写。如果这两个没有添加到

with

表达式中，则仅在一半位置用新变量

w

替换

scanr f e xs

，并且会出现类型错误。

您可以在这里了解更多关于这种皱纹的信息。