stuck on a proof (modeling IMP language)

Question

I've been trying 'port' some of the imperative language (IMP2) formalized in Isabelle here: https://www.isa-afp.org/sessions/imp2/#Semantics.html to Agda.

First, here are some initial translations I made for modeling the state and variable names + predicates for testing whether a variable is local or global:

vname : Set
vname = String

pname : Set -- procedure names 
pname = String 

is-global : vname -> Bool 
is-global name with (primStringToList name)
...    | []       = true
...    | (x ∷ xs) = primCharEquality x 'G' 

is-local : vname -> Bool 
is-local name = not (is-global name)

pval : Set 
pval = ℕ 

val : Set 
val = ℕ -> pval

-- *commands, boolean, and arith. expressions elided*

-- the state maps variable names to values 
State : Set 
State = vname -> val

I'm currently at the point in this part of the Imp2 document: https://www.isa-afp.org/sessions/imp2/#Semantics.html

(specifically the state combine definition -- my version shown in Agda below):

-- state combination
-- the state combination operator constructs a state by taking the local variables
-- from one state and the globals from another state

<_!_> : State -> State -> State
<_!_> s t = λ (n : vname) -> if (is-local n) then (s n) else (t n)

Having some trouble completing what I thought would be a pretty straightforward proof involving the combine <!> operator...:

combine-collapse : ∀ (s : State) -> < s ! s > ≡ s 
combine-collapse s = 
    begin
        < s ! s >
    ≡⟨⟩
       λ (n : vname) -> if is-local n then (s n) else (s n)  
    ≡⟨ ? ⟩
        ?    
    ∎

Using equational rewrites, I thought I would start with the left hand side of the ≡, then slowly derive s but when unfolding the definition of <!> in the second step, the typechecker is telling me:

s n ≡ _z_90 !=< (ℕ → pval)
when checking that the inferred type of an application
  s n ≡ _z_90
matches the expected type
  ℕ → pval

Figured that since the body for the ite application is the same, that would lead me to just s, but am getting stuck on the fact that states are functions.

Any guidance on how I should be proceeding with this proof? Or is there an oversight (or flaw) in the way State or other functions have been modeled that would keep this from proving?

Answer 1

You cannot prove propositional equality of functions. The closest you can get in your context is:

combine-collapse : ∀ {s n} -> < s ! s > n ≡ s n 
combine-collapse {s} {n} with is-local n
... | false = refl
... | true = refl

And then you would have to work with extensional equality (two functions are extensionally equal when they coincide for all inputs).

You can learn more about extensional equality in this article.