Working with Equivalent Definitions in Rocq

This summer, I’ve been interning at Sandia National Labs, working on extending CompCert for concurrent programs. We represent program states as a list of threads t :: ts and a memory state m. Much of my work relates to trying to formalize safety properties of the memory state as the program steps. This is my first time using Rocq outside of CSE 505, so I thought it would be interesting to write up some reflections on the experience.

Most importantly: the structure of definitions can drastically change how easy or hard it is to prove certain properties.

For example, consider these two definitions, which both capture the property of uniqueness of a list of nats:

Definition unique (m : list nat) :=
  forall i m1 m2,
  m = m1 ++ i :: m2
  -> ~ In i m1 /\ ~ In i m2.

Intuitively, this definition says a list of nats is unique if, for all i in the list, i does not appear before or after that single occurrence.

Fixpoint unique_rec (acc : list nat) (m : list nat) : Prop :=    
  match m with
  | [] => True
  | i :: m' => ~ In i acc /\ unique_rec (i :: acc) m'
  end.

Definition unique2 (m : list nat) := unique_rec [] m.

This definition uses a recursive helper function that traverses the list and checks whether each element has already appeared in the list (tracked via an accumulator).

Before we go any further, ponder the following for a moment:

1. Do you believe these definitions are equivalent?
2. Which definition do you think will be easier to work with?

By the end of this blog post, we will answer both questions, but let’s leave the question of equivalence aside for the moment and just start using the definitions to see whether there’s a difference in how easy they are to use.

Let’s start by trying to prove something really straightforward, like uniqueness of the empty list.

unique_empty

  Lemma unique_empty :
    unique [].
  Proof.
    unfold unique.

  (1/1)
  forall (i : nat) (m1 m2 : list nat),
  [] = m1 ++ i :: m2
  -> ~ In i m1 /\ ~ In i m2

Hmm, looks like the premise is false! Even if m1 and m2 are both empty, m1 ++ i :: m2 will have at least one element, so it can’t possibly equal the empty list. Destructing m1 and inverting the premise makes the rest of the proof go through easily:

  Lemma unique_empty :
    unique [].
  Proof.
    unfold unique. intros. destruct m1; inversion H.
  Qed.

Okay, now let’s try to do the same proof using our other definition:

  Lemma unique2_empty :
    unique2 [].
  Proof.
    unfold unique2.

  (1/1)
  unique_rec [] []

unique_rec is defined by cases on its second argument, so we know from the definition that unique_rec [] [] is True. We can finish the proof just by simplifying and letting auto take care of it:

  Lemma unique2_empty :
    unique2 [].
  Proof.
    unfold unique2. simpl; auto.
  Qed.

Okay, so maybe the proof for unique2 was a tiny bit easier, but both proofs fit on one line so it’s not a huge deal so far. It’s worth noting, though, that the proof for unique2 followed directly from the definition of unique_rec, while the proof for unique required doing case analysis on m2.

unique_single

Now that we’ve handled the empty list, let’s look at lists with a single element before we jump to the general inductive case.

  Lemma unique_single :
    forall x, unique [x].
  Proof.
    unfold unique. intros.

  x, i: nat
  m1, m2: list nat
  H: [x] = m1 ++ i :: m2
  
  ---
  
  (1/1)
  ~ In i m1 /\ ~ In i m2

It’s not immediately obvious how to prove that i is not in m1 or m2, which are just arbitrary lists. But if we stare at H a little bit, we can see that the only way for [x] to equal m1 ++ i :: m2 is if m1 and m2 are both [] (and therefore i is not in either list).

  Lemma unique_single :
    forall x, unique [x].
  Proof.
    unfold unique. intros.
    destruct m1, m2; split;
    auto; inversion H.

  x, i, n: nat
  m1: list nat
  H: [x] = (n :: m1) ++ [i]
  H1: x = n
  H2: [] = m1 ++ [i]
  
  ---
  
  (1/3)
  ~ In i (n :: m1)
  (2/3)
  ~ In i (n :: m1)
  (3/3)
  ~ In i (n0 :: m2)

For each of these cases, we just need to destruct m1 again to show Rocq that H is not possible, and we’re done:

  Lemma unique_single :
    forall x, unique [x].
  Proof.
    unfold unique. intros.
    destruct m1, m2; split; auto; inversion H;
    destruct m1; inversion H.
  Qed.

The final proof isn’t that bad, especially using semi-colon chaining to make it more concise. But it’s annoying that we keep having to do case analysis on m1 and m2. This is the first sign that our definition isn’t going to be well-suited to induction on xs.

Now let’s take a look at proving the same property using the other definition:

  Lemma unique2_single :
    forall x, unique2 [x].
  Proof.
    intros. unfold unique2. simpl. split; auto.
  Qed.

Here, the proof goes through super smoothly. It falls out pretty directly from the definition of unique2 and unique_rec.

unique_tl

  Lemma unique_tl :
    forall xs x,
    unique (x :: xs)
    -> unique xs.
  Proof.
    unfold unique. intros.

  xs: list nat
  x: nat
  H: forall (i : nat)
        (m1 m2 : list nat),
      x :: xs = m1 ++ i :: m2
      -> ~ In i m1 /\ ~ In i m2
  i: nat
  m1, m2: list nat
  H0: xs = m1 ++ i :: m2
  
  ---
  
  (1/1)
  ~ In i m1 /\ ~ In i m2

First, we need to decide how to approach this proof. Should we do induction? On what? The most natural thing to do induction on would probably be xs.

And we certainly can set up the proof that way. It ends up looking something like this:

  Lemma unique_tl :
    forall xs x, unique (x :: xs) -> unique xs.
  Proof.
    unfold unique. induction xs; intros.
    - destruct m1; inversion H0. 
    - destruct (H i (x :: m1) m2).
      + rewrite H0. auto.
      + split; auto.
        unfold not in *. intros; simpl in *.
        apply H1. auto.
  Qed.

Notice, though, that we never ended up using the induction hypothesis. That should tell us that we could have done the proof without induction. Recall that after unfolding the definition of unique and introducing variables, our proof goal is ~ In i m1 /\ ~ In i m2. Notice that the hypothesis H, which says forall (i : nat) (m1 m2 : list nat) if x :: xs = m1 ++ i :: m2 then ~ In i m1 /\ ~ In i m2, matches our proof goal exactly. Let’s see if we can use it!

In order to use H, we need to show x :: xs = m1 ++ i :: m2 for some m1, i, m2. From H0, we know xs = m1 ++ i :: m2. It’s important to note that the m1, i, and m2 in H0 are different than the m1, i, and m2 in H. In H0 they are set, while in H they are universally quantified, so we can choose any values to use in H. Specifically, we want to choose m1 = x :: m1, i = i, and m2 = m2. That way, we have x :: xs = x :: m1 ++ i :: m2, as desired.

Now we get to use the conclusion of H, which tells us ~ In i (x :: m1) /\ ~ In i m2. Remember, we’re still trying to prove ~ In i m1 /\ ~ In i m2. The right clause follows directly from H, and the left clause isn’t too hard to prove just by unfolding not and simplifying things. The final proof looks like this:

  Lemma unique_tl :
    forall xs x, unique (x :: xs) -> unique xs.
  Proof.
    unfold unique. intros.
    destruct (H i (x :: m1) m2). subst; auto.
    split; auto. unfold not in *; simpl in *.
    intros; apply H1; auto.
  Qed.

Now let’s prove the same thing for unique2. As before, we probably won’t need induction. Let’s try case analysis on xs. The first case, unique2 [], is exactly what we already proved with the unique2_empty lemma. Unfolding and simplifying in the second case, we get to a proof state that looks like this:

  Lemma unique2_tl :
    forall xs x,
      unique2 (x :: xs)
      -> unique2 xs.
  Proof.
    destruct xs; intros.
    - apply unique2_empty.
    - unfold unique2 in *.
      simpl in *. split; auto.
      destruct H. destruct H0.

  n: nat
  xs: list nat
  x: nat
  H: ~ False
  H0: ~ (x = n \/ False)
  H1: unique_rec [n; x] xs
  
  ---
  
  (1/1)
  unique_rec [n] xs

We know that xs is unique with respect to [n; x] so it should follow that xs is unique with respect to just [n]. We need a way to “forget” things out of the accumulator. But this doesn’t follow directly from any of the definitions, so we’ll need to prove a helper lemma:

  Lemma unique2_acc :
    forall xs acc acc',
      unique_rec acc xs
      -> (forall x, In x acc' -> In x acc)
      -> unique_rec acc' xs.
  Proof.
    induction xs; intros; simpl in *; auto.
    destruct H. split; auto.
    eapply IHxs; eauto.
    intros; simpl in *. destruct H2; auto.
  Qed.

This is our first induction proof. Our induction hypothesis tells us that the property holds for xs and we need to show that it holds for a :: xs. And since unique_rec is defined recursively on its second argument, we can use the definition of unique_rec to simplify unique_rec acc' (a :: xs) to unique_rec (a :: acc') xs, allowing us to use the induction hypothesis.

Okay, great, so with helper lemma in hand, we can finish the proof for unique2_tl:

  Lemma unique2_tl :
    forall xs x, unique2 (x :: xs) -> unique2 xs.
  Proof.
    destruct xs; intros.
    - apply unique2_empty.
    - unfold unique2 in *; simpl in *. split; auto.
      destruct H, H0. eapply unique2_acc; eauto.
      intros; simpl in *. destruct H2; auto.
  Qed.

That time, it seems like the proof for unique2 was actually a little harder. We needed to prove a helper lemma by induction that we could use in the second case of the proof. But, along the way, we proved a helper lemma that will likely be useful in other contexts as well. We also saw that induction proofs on the second argument to unique_rec can work out smoothly because the definition of unique_rec is also recursive on that argument.

unique_cons

We just saw that we can peel off an item from the list and the rest is still unique. Let’s now try to show that we can add something to the list and maintain uniqueness. Of course, we also need to know that the thing we’re adding isn’t already in the list (otherwise the resulting list won’t be unique).

This time let’s do it first for unique2:

  Lemma unique2_cons :
    forall xs x,
      unique2 xs
      -> ~ In x xs
      -> unique2 (x :: xs).
  Proof.
    induction xs; intros.
    - apply unique2_single.
    - unfold unique2 in *.
      simpl. split; auto. split.
      + unfold not. intros.
        destruct H1; auto. subst.
        simpl in H0. apply H0.
        left; auto.
      + simpl in *.
        destruct H.
        specialize (IHxs x).

  a: nat
  xs: list nat
  x: nat
  IHxs: unique_rec [] xs
        -> ~ In x xs
        -> (~ False /\
        unique_rec [x] xs)
  H: ~ False
  H1: unique_rec [a] xs
  H0: ~ (a = x \/ In x xs)
  
  ---
  
  (1/1)
  unique_rec [a; x] xs

So far we’ve handled the base case and we’ve started working our way through the inductive case. We’ve unfolded all of the definitions, simplifying and substituting as we go, to get to a place where we can use the induction hypothesis. Now we’re at a point where we know unique_rec [x] xs (from the IH) and we know unique_rec [a] xs (from H1). But we need a way to put them together. Let’s try a helper lemma:

  Lemma unique2_acc_append :
    forall xs acc1 acc2,
      unique_rec acc1 xs
      -> unique_rec acc2 xs
      -> unique_rec (acc1 ++ acc2) xs.
  Proof.
    induction xs; intros; simpl in *; auto.
    split; destruct H, H0.
    - unfold not in *; intros.
      edestruct Coq.Lists.List.in_app_or; eauto.
    - apply (IHxs (a :: acc1) acc2); auto.
      eapply unique2_acc; eauto.
      intros; simpl; right; auto.
  Qed.

There’s nothing super interesting going on in this helper lemma, but it’s just another example of how the definition of unique_rec is well-suited to proofs by induction on xs. And with this lemma we can finish the proof for unique2_cons:

  Lemma unique2_cons :
    forall xs x,
      unique2 xs
      -> ~ In x xs
      -> unique2 (x :: xs).
  Proof.
    induction xs.
    - intros. apply unique2_single.
    - intros. unfold unique2 in *. simpl.
      split; auto. split.
      + unfold not. intros. destruct H1; auto.
        subst. simpl in H0. apply H0. left; auto.
      + simpl in *. destruct H.
        apply (unique2_acc_append xs [a] [x]); auto.
        apply IHxs; auto.
        eapply unique2_acc; eauto. intros; inversion H2.
  Qed.

Note that we got to use unique2_acc again – I knew that helper lemma would come in handy :)

Okay, so this proof was not trivial, but we were able to break it down into smaller pieces using helper lemmas, prove all of them by induction on xs, and build it back together to prove the property we wanted.

Let’s see what happens when we try to prove unique_cons for the other definition of uniqueness.

  Lemma unique_cons :
    forall xs x,
      unique xs
      -> ~ In x xs
      -> unique (x :: xs).
  Proof.
    induction xs.
    - intros.
      apply unique_single.
    - unfold unique. intros.
      split;
      destruct m1, m2; auto.

  a: nat
  xs: list nat
  IHxs: forall x : nat,
        (forall (i : nat)
          (m1 m2 : list nat),
          xs = m1 ++ i :: m2
          -> (~ In i m1 /\
          ~ In i m2)) ->
        ~ In x xs ->
        forall (i : nat)
          (m1 m2 : list nat),
        x :: xs = m1 ++ i :: m2
        -> ~ In i m1 /\
        ~ In i m2
  x: nat
  H: forall (i : nat)
      (m1 m2 : list nat),
      a :: xs = m1 ++ i :: m2
      -> ~ In i m1 /\
         ~ In i m2
  H0: ~ In x (a :: xs)
  i, n: nat
  m1: list nat
  H1: x :: a :: xs =
      (n :: m1) ++ [i]
  
  ---
  
  (1/4)
  ~ In i (n :: m1)
  (2/4)
  ~ In i (n :: m1)
  (3/4)
  ~ In i (n :: m2)
  (4/4)
  ~ In i (n0 :: m2)

Okay, so far, we were able to handle the base case using unique_single, which we proved earlier. In the inductive case, we will again need to massage a :: xs into having the right shape to be able to use either IHxs, which requires xs = m1 ++ i :: m2, or H, which requires a :: xs = m1 ++ i :: m2. Let’s try destructing m1 and m2, that was helpful in previous proofs.

Honestly, this is the part of the blog post where I wish I could show you the gnarly, complicated proof for unique_cons that would nicely illustrate how much easier unique2 is to work with. Unfortunately though, I really haven’t been able to get the proof to go through. I think there’s got to be a way to do it by case analysis on m1 and m2, but I eventually gave up.

If anything, though, maybe my ability to solve one proof but not the other counts as evidence that unique2 is easier to work with :)

Yeah, but are they equivalent?

Suppose we’re working in a system that uses the unique definition everywhere. We’d like to switch the definition to unique2 since it’s so much easier to prove properties about. But is it safe? We wouldn’t want to change the definition to make our proofs easier if it doesn’t actually capture the same meaning we had originally intended…

Let’s try to prove the equivalence between our two definitions. There are two directions to prove: forall xs, unique xs -> unique2 xs and forall xs, unique2 xs -> unique xs.

If we’re right that unique2 is easier to work with than unique, we should expect unique xs -> unique2 xs to be easier to prove, so let’s start there.

Again, we’ll set up the proof by induction on xs. The first case is taken care of by unique2_empty, which we proved earlier. In the inductive case, we can use the definition of unique_rec and the structure of the argument to simplify to unique_rec [a] xs. Then it only takes a few more steps to be able to use our induction hypothesis, which tells us unique xs -> unique2 xs. The whole proof looks like this:

Lemma unique_is_unique2 :
  forall xs, unique xs -> unique2 xs.
Proof.
  induction xs; intros.
  - apply unique2_empty.
  - unfold unique2. simpl. split; auto.
    eapply unique2_cons.
    + apply IHxs. eapply unique_fst; eauto.
    + unfold unique in H. apply (H a [] xs); auto.
Qed.

Okay, great! Did we prove that it’s safe to replace unique with unique2 everywhere in our codebase? We’ve shown that if a list is unique, then it is unique2. But, that’s not really what we care about, right? If we’re switching from unique to unique2, we really care about the other direction: that is, if a list is unique2 then it is unique. Then we’ll know that it’s safe to show unique2 instead of unique. So let’s tackle that direction:

We’re going to need a few more helper lemmas. The proofs aren’t very interesting, so in the interest of space, I’ll leave them as an exercise to the reader

Lemma unique_acc_not_in :
  forall xs acc x, unique_rec acc xs -> In x acc -> ~ In x xs.
Proof.
Admitted.

Lemma in_end :
  forall (A : Type) (xs xs' : list A) x, In x (xs ++ x :: xs').
Proof.
Admitted.

And the whole proof looks like this:

Lemma unique2_is_unique :
    forall xs, unique2 xs -> unique xs.
Proof.
    induction xs.
    - intros. apply unique_empty.
    - unfold unique. intros. unfold unique2 in H.
      simpl in H. destruct H.
      assert (unique2 xs). eapply unique2_acc; eauto.
      intros; inversion H2.
      unfold unique in IHxs. destruct m1, m2; auto.
      + split; auto. inversion H0.
        unfold not; simpl; intros. subst.
        destruct H3; subst.
        * inversion H1. simpl in *. auto.
        * simpl in *. destruct H1.
          edestruct unique_acc_not_in; eauto.
          simpl; right; auto.
      + split; auto. inversion H0.
        unfold not; simpl. intros. destruct H3. subst.
        apply (unique_acc_not_in (m1 ++ [i]) [i] i); auto.
        simpl; auto. eapply in_end.
        edestruct IHxs; eauto.
      + split; inversion H0.
        * unfold not; simpl. intros. destruct H3. subst.
          apply (unique_acc_not_in
            (m1 ++ i :: n0 :: m2) [i] i); auto.
          simpl; auto. eapply in_end.
          edestruct IHxs; eauto.
        * eapply IHxs; eauto.
Qed.

In the base case, we just use unique_empty. In the inductive case, after unfolding and simplifying things, we have H1: unique_rec [a] xs. We can use this to show unique2 xs, which will allow us to use our induction hypothesis (unique2 xs -> unique xs). Recall that unique xs says forall (i : nat) (m1 m2 : list nat), xs = m1 ++ i :: m2 -> ~ In i m1 /\ ~ In i m2, and we’re trying to show ~ In i m1 /\ ~ In i m2. Let’s do case analysis on m1 and m2.

1. When both are empty, auto takes care of ~ In i m1 /\ ~ In i m2.
2. When m1 = [] and m2 = n :: m2, we need to show ~ In i (n :: m2), which results in two cases: ~ n = i and ~ In i m2. In both cases, we can use H1 : unique_rec [i] (n :: m2) to show the contradiction.
3. When m1 = n :: m2 and m2 = [], we again end up with two cases: n = i \/ In i m1 -> False. In the first case, we use unique_rec [n] (m1 ++ [i]) to show the contradiction. In the second case, we can use the induction hypothesis since m1 ++ [i] = m1 ++ [i] :: []
4. The last case, when m1 = n :: m1 and m2 = n0 :: m2, is similar to the the third case, just with a different instantiation of the induction hypothesis.

Phew, that was a lot. But taking a step back, we can see that we’ve proven the answer to Question 1 that I posed at the beginning of this post. YES, unique and unique2 are equivalent, and we proved it.

Bonus: unique_cons again

With the equivalence between unique and unique2 in hand, we can finally show forall xs x, unique xs -> ~ In x xs -> unique (x :: xs)., which I was unable to prove directly. The proof looks like this:

Lemma unique_cons :
  forall xs x, unique xs -> ~ In x xs -> unique (x :: xs).
Proof.
  intros.
  (* convert to using the recursive definition *)
  eapply unique2_is_unique.

  (* apply the lemma *)
  eapply unique2_cons; auto. 
  
  (* convert back *)
  eapply unique_is_unique2; auto. 
Qed.

Basically, we show that since we know unique xs, then we know unique2 xs. And since we know unique2 xs and ~ In x xs, then we know unique2 (x :: xs). And finally, since we know unique2 (x :: xs), then we can conclude unique (x :: xs), as desired.

Conclusion

So what’s the point of all this? I think the main takeaway is that the structure of the definition has a huge impact on how easy or hard it is to prove properties. As a result, when you’re stuck on a proof, it’s worth considering if there’s a way to rephrase the property to facilitate the proof. These uniqueness lemmas are pretty similar to lemmas that we have in our extension to CompCert. And we did, in fact, end up changing the definition to more closely resemble unique2 in order to make the lemmas easier to work with.