我正在研究涉及 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
有人可以提供如何处理这个证明的指导,特别是如何处理推理中的分支吗?我对此很陌生,所以提前感谢您的指点!
确实是一个相当烦人的问题。以下是如何让它发挥作用:
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
,并且会出现类型错误。
您可以在这里了解更多关于这种皱纹的信息。