Pattern matching and autocomplete

[JansthcirlU]

While reviewing the answer to exercise 8.4.1. (Reverse is injective), I rewrote the lemma like this because it felt more natural:

let rec snoc_injective (#a: Type) (l1 l2: list a) (h1 h2: a) : Lemma (requires snoc l1 h1 == snoc l2 h2) (ensures h1 == h2 /\ l1 == l2) =
    match l1, l2 with
    | [], [] -> ()
    | _ :: tl1, _ :: tl2 -> snoc_injective tl1 tl2 h1 h2

But then I realized that unlike the answer in the book, this lemma doesn't match on all the patterns (empty + non-empty list, for example). Why doesn't it give me an error here?

As a follow-up question, if I omit the second pattern, I do get a "Patterns are incomplete" error with the expected incomplete quantifiers Z3 errors, but will it ever be possible to autogenerate the missing cases like it's possible in F#?

[mtzguido]

Due to the precondition that snoc l1 h1 == snoc l2 h2, it's impossible for one of l1/l2 to be empty but not the other. F* + Z3 can prove this fact automatically, and therefore those branches need not be written as they are unreachable. You could even add the missing patterns like so:

let rec snoc_injective (#a: Type) (l1 l2: list a) (h1 h2: a) : Lemma (requires snoc l1 h1 == snoc l2 h2) (ensures h1 == h2 /\ l1 == l2) =
    match l1, l2 with
    | [], [] -> ()
    | _ :: tl1, _ :: tl2 -> snoc_injective tl1 tl2 h1 h2
    | _, _ -> assert False

We can prove false in that branch as it is unreachable.

I don't think there is a way to generate the missing branches automatically. There was an attempt to do this in #940 but I don't think it's been maintained.