`FStar.List.Tot.Properties.append_mem` is missing SMTPat

[shonfeder]

Hello!

I just found this very helpful property has its SMTPat commented out:

https://github.com/fstarlang/FStar/blob/master/ulib/FStar.List.Tot.Properties.fst#L191-L199

val append_mem: #t:eqtype ->  l1:list t
              -> l2:list t
              -> a:t
              -> Lemma (requires True)
                       (ensures (mem a (l1@l2) = (mem a l1 || mem a l2)))
                       (* [SMTPat (mem a (l1@l2))] *)
let rec append_mem #t l1 l2 a = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2 a

For want of this pattern, we don't enjoy automated proof for properties such as

let state_concat_has_both (vs vs': list vars) (s:state{state_has s (vs @ vs')})
    : Lemma (state_has s vs /\ state_has s vs')
    = ()

In general, it seems like a useful prop to have in the theory of lists. I assume this was commented out for a reason, but the git blame doesn't turn up anything obvious for me.

Would it be feasible to uncomment this? If not, perhaps a comment can be added explaining why it is omitted.

I'd be pleased to contribute either change, in case that is helpful.

Thanks for the amazing software!

[nikswamy]

Adding this pattern to append_mem is indeed fairly natural, but putting it in the standard library will make proofs much more expensive for many clients. Every mem a (l1 @ l2) in scope will introduce an SMT case split.

Instead, it may be better to introduce this lemma in scope when needed, rather than globally.

For example, one might write:

let append_mem_auto ()
  : squash
    (∀ (a:eqtype) (x:a) (l1 l2:list a).
       {:pattern mem x (l1 @ l2)}
       mem x (l1 @ l2) = (mem x l1 ‖ mem x l2))
  = introduce ∀ a x l1 l2. _
    with append_mem l1 l2 x

And in your particular proof, you can do something like this:

let test (l1 l2:list int) (x:int { mem x l1 }) =
  append_mem_auto ();
  assert (mem x (l1 @ l2))

[nikswamy]

We could add append_mem_auto to the list library and document this style of usage.

[shonfeder]

This makes sense and the pointer is very helpful! I would be pleased to open a PR with the improvement as advise, and will plan to do so this week if I don't hear otherwise.