Search code examples
typesproofagdatheorem-proving

Agda not eliminating clause in goal despite pattern matching on it

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
Solution

  • 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.