Working with match expression

Stream: Program verification

[Sorawee Porncharoenwase]

Hi everyone,

In my work, I have an interpreter for a lambda calculus-like language. The function application case looks like this:

  | exp.app f a :=
    match interpC fuel f environ with
    | none := none
    | some (halt b) := some (halt b)
    | some (ans fval) :=
      match interpC fuel a environ with
      | none := none
      | some (halt b) := some (halt b)
      | some (ans aval) :=
        match fval with
        | val.clos x body staticEnviron :=
          interpC fuel body (staticEnviron.update_nth x aval)
        | _ := some err
        end
      end
    end

When I try to prove a theorem about this interpreter, after unfold the definition of the interpreter itself (and a couple of other case analysis), I have:

h :
  interpC._match_3
      (λ (aval : val) (x : ℕ) (body : exp) (staticEnviron : list val),
         interpC fuel_n body (staticEnviron.update_nth x aval))
      (some (result.ans v_a))
      (some (result.ans (val.clos the_var the_body the_env))) =
    some r

How do I partially reduce h further? It's clear from the high-level reasoning that I want to cases on interpC fuel_n the_body (the_env.update_nth the_var v_a) and then call injection h, but cases on interpC ... doesn't correctly rewrite h since the term doesn't occur in h.

I tried simp at h or even unfold interpC._match_3 at h, but none of them works.

Thanks!

[Mario Carneiro]

what does rw interpC at h do?

[Mario Carneiro]

Could you give a #mwe?

[Sorawee Porncharoenwase]

Yep, that works. I also just realized that unfold interpC._match_3 works too, but it introduced interpC._match_4 instead (which I mistook it as interpC._match_3). After a couple of unfold, I get exactly what I need.

Thanks!

[Mario Carneiro]

simp [interpC] will probably work from the start

[Mario Carneiro]

you don't usually need to mention these _match_n functions explicitly

[Sorawee Porncharoenwase]

Yep, you are totally right. Thanks for your help! :)