将布尔语句提升为命题。

Question

给定一个列表，一个 "属性"（一个函数，用于 Bools），以及证明 any f xs ≡ true，我想得到的值是 Any (λ x → T (f x)) ns即，我想把一个证明从 any 以证明 Any.

到目前为止，我已经能够画出证明的草图，但我卡在了一个看似简单的语句上（请看下面第二行到最后一行）。

open import Data.Bool
open import Data.Bool.Properties
open import Data.List
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Unit
open import Relation.Binary.PropositionalEquality 

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl = tt

any-val : ∀ {a} {A : Set a} (f) (ns : List A)
        → any f ns ≡ true
        → Any (λ x → T (f x)) ns
any-val f [] ()
any-val f (n ∷ ns) any-f-⟨n∷ns⟩≡true with f n
...                            | true  = here (≡→T ?)
...                            | false = there (any-val f ns any-f-⟨n∷ns⟩≡true)

显然，我需要证明 f n ≡ true这一点应该是不难证明的，因为我们是在 true 旗下 with 声明 f ≡ true.

那里面应该放什么？我有什么地方理解错了？

Answer 1

关键是要用 inspect 习惯用语，我在这里的另一个答案中已经详细描述了。

"with f x "匹配 "false"，但不能构造 "f x == false"。

这给出了下面的代码，我清理了一下，包括导入。

open import Data.Bool
open import Data.List
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.Unit
open import Relation.Binary.PropositionalEquality 
open import Function

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl = tt

any-val : ∀ {a} {A : Set a}
  f (ns : List A) → any f ns ≡ true → Any (T ∘ f) ns
any-val f (x ∷ l) p with f x | inspect f x
... | false | _ = there (any-val f l p)
... | true | [ fx≡true ] = here (≡→T fx≡true)

顺便说一句，请确保你的Agda更新到了最新版本，这样你就不用处理空箱了 any-val f [] ()，就像你的代码一样。