## Stream: Program verification

### Topic: Working with match expression

#### Sorawee Porncharoenwase (Oct 31 2020 at 23:52):

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 (Oct 31 2020 at 23:58):

what does rw interpC at h do?

#### Mario Carneiro (Oct 31 2020 at 23:59):

Could you give a #mwe?

#### Sorawee Porncharoenwase (Nov 01 2020 at 00:01):

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 (Nov 01 2020 at 00:02):

simp [interpC] will probably work from the start

#### Mario Carneiro (Nov 01 2020 at 00:02):

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

#### Sorawee Porncharoenwase (Nov 01 2020 at 00:04):

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

Last updated: May 08 2021 at 22:13 UTC