尽管对其进行了模式匹配，但 Agda 并未消除目标中的子句

Question

我有以下形式的 agda 代码片段：


Terminates :  → S → Set
Terminates c s = Σ[ n ∈ ℕ ] ( Is-just (proj₂ (smallStepEvalwithFuel n ( c , just s ))))

evalAssiProg : ∀ {i e} → S → (p : i := e) → Maybe S
evalAssiProg s (id ꞉= exp) with evalExp exp s
... | nothing = nothing -- Comp failed. i.e. ÷ by 0 error
... | just v = just (updateState id v s) -- Comp success

example : ∀ i v exp s → ( a : i := exp ) → evalExp exp s ≡ just v → Terminates ( ꞉ a ) s
example i v e s (.i ꞉= .e) p with evalExp e s
... | just x = 1 , {!!} --<----------------------! Problem here

我希望细节不要太重要，基本上 evalExp e s 具有 evalExp : Exp → S → Maybe Val 的形式，即它接受一个表达式、一个状态，并吐出值，除非除法例如，零错误发生。所以这是一个繁琐但简单的功能。

我感兴趣的是：如何在 example 中对 evalExp e s 进行模式匹配，并使 agda 正确计算出唯一可能的情况是 just x 但如果我查看产品右侧的目标，我仍然认为目标仍在等待 [=12= 的结果]:

Goal: Any (λ _ → ⊤)
      (Mini-C.Evaluation.evalAssiProg dRep sRep s (i Mini-C.Lang._:=_.꞉= e)
       | evalExp e s)
————————————————————————————————————————————————————————————
i    : Id
s    : S
e    : Exp
sRep : S-Representation dRep
p    : just x ≡ just v
v    : Val
x    : Val
dRep : D-Representation

Answer 1

我相信下面的代码片段可以准确模拟您的问题：

module _ where

open import Data.Maybe
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Maybe.Relation.Unary.Any

variable
  A B : Set

Terminates : ∀ {A B : Set} → (A → Maybe B) → Set
Terminates f = Σ _ λ x → Is-just (f x)

example : ∀ (f : A → Maybe B) x y → f x ≡ just y → Terminates f
example f x y p = x , {!!}

这里，洞的类型是Is-just (f x)，我们想用证明p来解决它。问题是我们不能只把 just tt 写进洞里：

just _x_26 != f x of type Maybe B
when checking that the inferred type of an application
  Any (λ _ → ⊤) (just _x_26)
matches the expected type
  Is-just (f x)

因为 f x 不会减少到 just _，因为我们对 f 或 x 一无所知。但是等等，我们知道一些关于它的信息 -- 在 p。所以这里需要安排p来做个差：

example : ∀ (f : A → Maybe B) x y → f x ≡ just y → Terminates f
example f x y p = x , subst Is-just (sym p) (just tt)

在这里，（统一后）我们有 just tt : Is-just (just y)，我们用等式 sym p : just y ≡ f x 重写它的类型为 subst _ _ (just tt) : Is-just (f x)，这正是我们的目标。

尽管对其进行了模式匹配，但 Agda 并未消除目标中的子句

Agda not eliminating clause in goal despite pattern matching on it

types

proof

agda

theorem-proving