Unexpected behavior when unfolding functions in two let match statements

[klinvill]

I'm seeing some unexpected behavior in what gets normalized in the below lemmas. The first lemma (add_equiv) normalizes like I expect it to, that is all occurrences of the reify and add are unfolded. However, normalization in the second lemma only unfolds the first occurrence of reify and add.

Does anyone know why this happens? I noticed that the unfolding works after mapply tm;, but doesn't do anything if applied to the premise (let h2 = norm_term [delta; iota] h1 in).

module Debugging

open FStar.Tactics
open FStar.Tactics.Arith

// These modules come from the examples/dm4free directory
// (https://github.com/FStarLang/FStar/tree/master/examples/dm4free)
open FStar.DM4F.Random
open FStar.DM4F.Heap.Random

(** A helper function from Nik to turn `hyp` into an arrow that can be applied *)
let as_lemma #a (#pre: a → Type)
		(#post: a → Type)
                (hyp:(∀ (x:a). pre x ⟹ post x))
                (x:a)
                (_:squash (pre x))
  : Tot (squash (post x))
  = ()

let add (x y: int) : Rand (int)
  = x + y

// Using norm in this lemma unfolds all reify and add functions as expected.
let add_equiv (x: int) : Lemma
  (ensures (
    let r1 h = reify (add x x) h in
    let r2 h = reify (add (x+1) (x-1)) h in
    forall (t: tape).
      let sum1 = match r1 ((to_id 0), t) with
        | Some z, _ -> z
        | _, _ -> 0
      in
      let sum2 = match r2 ((to_id 0), t) with
        | Some z, _ -> z
        | _, _ -> 0
      in
      sum1 == sum2
  ))
  by (
    split();
    smt();
 
    let post = forall_intro () in
    // Specifically this norm step unfolds the reify and add functions for both the first and second occurrences.
    norm [delta];
    let h1 = implies_intro () in
    let r = forall_intro () in
    let tm = `(as_lemma (`#(binder_to_term h1))) in
    mapply tm;
    let t = forall_intro () in
    dump "Simplified:";
    split_arith ();
    qed()
  )
= ()


// Yet using norm in this lemma unfolds only the first reify and add functions. The lemma is identical to the
// previous lemma except in introducing intermediate let statements within the forall statement.
let add_equiv_doesnt_norm (x: int) : Lemma
  (ensures (
    let r1 h = reify (add x x) h in
    let r2 h = reify (add (x+1) (x-1)) h in
    forall (t: tape).
      let s1, _ = r1 ((to_id 0), t) in
      let s2, _ = r2 ((to_id 0), t) in
      let sum1 = match s1 with
        | Some z -> z
        | _ -> 0
      in
      let sum2 = match s2 with
        | Some z -> z
        | _ -> 0
      in
      sum1 == sum2
  ))
  by (
    split();
    smt();
 
    let post = forall_intro () in
    // But this norm step only unfolds the reify and add functions for the first occurrence.
    norm [delta];
    let h1 = implies_intro () in
    let r = forall_intro () in
    let tm = `(as_lemma (`#(binder_to_term h1))) in
    mapply tm;
    let t = forall_intro () in
    dump "Not simplified:";
    split_arith ();
    qed()
  )
= ()

[klinvill]

I found that if I instead change the norm [delta]; step to norm [delta; iota]; (which additionally reduces match statements) then the second lemma ends up normalizing to the same thing as the first lemma (when just using norm [delta];). So it seems like the extra abstraction introduced by the let statements in the second lemma means that the normalizer needs to explicitly reduce the match statements? I'm still a little confused why only the first reify and add functions can be unfolded in the second lemma but it helps knowing the normalizer just needs to employ some additional tactics to fully reduce the expression.

[nikswamy]

This is surprising. Thanks for the investigations. It looks like a bug to me ... feel free to open an issue for it.

[klinvill]

For future reference, there is now an issue for this: #2568