What tactic is needed to rewrite a sub-expression in the goal state?

[klinvill]

I'm trying to use the rewrite tactic to replace a sub-expression in my goal, but it's not replacing it like I would expect it to be replaced if I was using the Coq rewrite tactic. What's the proper way to rewrite sub-expressions in F* using tactics?

Here's an example where I tried to replace bytes_to_seq b1 with Bytes.reveal b1 in the goal state. I'm able to pose lemma_bytes specifically for b1 and unsquash it so I have bytes_to_seq b1 == Bytes.reveal b1 in the context. But I can't use that equality to rewrite bytes_to_seq b1 in the goal state so it's replaced with Bytes.reveal b1. Instead it just tells me that the rewrite tactic failed.

module Test

open FStar.Seq
open FStar.Bytes

// Total function to convert a bytes type to a sequence of bytes
assume val bytes_to_seq (l: bytes) : (r: seq byte {r == Bytes.reveal l})

let lemma_bytes_to_seq (l: bytes) : Lemma
  (ensures bytes_to_seq l == Bytes.reveal l)
= ()

#push-options "--query_stats"
let try_rewrite_tactic (b1 b2: bytes) : Lemma
  // Require the appended bytes to still fit in the constraints of the bytes type
  (requires UInt.size (UInt32.v (Bytes.len b1) + UInt32.v (Bytes.len b2)) 32)
  (ensures bytes_to_seq (Bytes.append b1 b2) == Seq.append (bytes_to_seq b1) (bytes_to_seq b2))
  by (
    let open FStar.Tactics in
    // Split and send type obligations to smt solver
    split ();
    smt ();

    // Get rid of the extra cruft in the goal so the goal is just the squash of the ensures clause
    let post = forall_intro () in
    let h1 = implies_intro () in
    let h2, h3 = destruct_and h1 in
    let rt = forall_intro () in
    let h3' = instantiate h3 rt in
    mapply h3';

    // Try to rewrite (bytes_to_seq b1) to (Bytes.reveal b1) in the goal state
    let h4 = pose_lemma (`(lemma_bytes_to_seq (`@b1))) in
    let h5 = pose_as "h5" (unsquash h4) in
    // This rewrite fails, even though h5 in the context is: bytes_to_seq b1 == reveal b1
    rewrite' h5;

    // Dumps out goal since we haven't proven it yet
    qed ()
  )
= ()
#pop-options

[mtzguido]

Hi Kirby. The rewrite primitive only works for equalities with a variable on the LHS, and basically does substitution. To rewrite general term equalities, there is grewrite_eq, but it does not work in this example since the inferred equality type for your h5 binder is seq UInt8.t, but the bytes_to_seq b1 subterm is inferred at the refined type.

This variation works for me, maybe it can unblock you, but this is something to fix for sure.

module Test

open FStar.Seq
open FStar.Bytes

// Total function to convert a bytes type to a sequence of bytes
assume val bytes_to_seq (l: bytes) : seq byte

assume val __lemma_bytes_to_seq (l: bytes) : Lemma
  (ensures bytes_to_seq l == Bytes.reveal l)

let lemma_bytes_to_seq (l: bytes) : Lemma
  (ensures bytes_to_seq l == Bytes.reveal l)
= __lemma_bytes_to_seq l

#push-options "--query_stats --print_implicits" // --tactic_trace_d 2"
let try_rewrite_tactic (b1 b2: bytes) : Lemma
  // Require the appended bytes to still fit in the constraints of the bytes type
  (requires UInt.size (UInt32.v (Bytes.len b1) + UInt32.v (Bytes.len b2)) 32)
  (ensures bytes_to_seq (Bytes.append b1 b2) == Seq.append (bytes_to_seq b1) (bytes_to_seq b2))
  by (
    let open FStar.Tactics in
    // Split and send type obligations to smt solver
    split ();
    smt ();

    // Get rid of the extra cruft in the goal so the goal is just the squash of the ensures clause
    let post = forall_intro () in
    let h1 = implies_intro () in
    let h2, h3 = destruct_and h1 in
    let rt = forall_intro () in
    let h3' = instantiate h3 rt in
    mapply h3';

    // Try to rewrite (bytes_to_seq b1) to (Bytes.reveal b1) in the goal state
    let h4 = pose_lemma (`(lemma_bytes_to_seq (`@b1))) in
    let h5 = pose_as "h5" (unsquash h4) in
    dump "A";
    grewrite_eq h5;
    dump "B";

    // Dumps out goal since we haven't proven it yet
    qed ()
  )
= ()
#pop-options

[klinvill]

Awesome, thanks Guido! Does grewrite mean something like general rewrite?

[mtzguido]

Yup indeed :).

[klinvill]

Along similar lines, is there a tactic that allows adding a variable to represent a sub-expression? In particular I'm wondering if there's a way to put something like b3 == Bytes.append b1 b2 into the context? It seems that I can't write let h6 = (pose_lemma (`(lemma_bytes_to_seq (Bytes.append (`@b1) (`@b2))))) in. I presume this is because it sees Bytes.append (`@b1) (`@b2) as an expression rather than a term of bytes