Zulip Chat Archive

Stream: Program verification

Topic: Working with match expression


view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Oct 31 2020 at 23:58):

what does rw interpC at h do?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 23:59):

Could you give a #mwe?

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Nov 01 2020 at 00:02):

simp [interpC] will probably work from the start

view this post on Zulip Mario Carneiro (Nov 01 2020 at 00:02):

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

view this post on Zulip 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