Agda not eliminating clause in goal despite pattern matching on it

user_10420700 0
Viewed 78

I have a snippet of agda code of the following form:


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

I'm hoping that the details don't matter too much, basically evalExp e s has the form evalExp : Exp → S → Maybe Val i.e. it takes an expression, a state, and spits out the value unless a divide by zero error occurs for example. So it is a tedious but simple function.

All I'm interested in is: how can I pattern match on evalExp e s in example, and have agda correctly work out that the only possible case is just x but still if I look in the goal on the right hand side of the product I have that the goal is still waiting on the result of evalExp e s:

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
theorem-proving agda proof types
1 Answers

I believe the below snippet models your problem accurately:

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 , {!!}

Here, the type of the hole is Is-just (f x), and we would like to use the proof p to solve it. The problem is that we can't just write just tt into the hole:

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)

Because f x doesn't reduce to just _, since we know nothing about f or x. But wait, we do know something about it -- in p. So we need to arrange for p to make a difference here:

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)

Here, (after unification) we have just tt : Is-just (just y), and we rewrite its type with the equality sym p : just y ≡ f x, to subst _ _ (just tt) : Is-just (f x) which is exactly our goal.

user_4774760
Related