fstar

Using the normalizer to reduce a recursive function

I want to prove a property parameterized over a finite number of cases. I would like to divide the problem to one instance per case and solve each instance separately. Here is an example to clear up things:

module Minimal
open FStar.List
open FStar.Tactics
open FStar.Reflection.Data

unfold let lst = [0;1]

unfold let prop i = 
  match i with
  | 0 -> i == 0
  | 1 -> i == 1
  | _ -> False

val propHolds (i:int) : Lemma (requires (List.mem i lst)) (ensures (prop i))

In this case the cases are defined by the list lst. I can easily prove propHolds:

let propHolds i =
  assert_by_tactic (prop 0) (fun () -> norm[delta;primops;iota;zeta]; dump "normalized"; trivial ());
  assert_by_tactic (prop 1) (fun () -> norm[delta;primops;iota;zeta]; dump "normalized"; trivial ())

but I obviously don't want to write a separate assert_by_tactic for each case (not when there may be thousands..). I somehow want to generate the proof above automatically for all elements in lst.

I tried various things, here is one of them:

  assert_by_tactic (let rec props i =
                       if i = 0 then prop 0
                       else (prop i) /\ (props (i-1))
                    in
                      props 1) (fun () -> norm[delta;primops;iota;zeta]; dump "normalized")

Unfortunately, this doesn't quite achieve what I would like, the assert_by_tactic fails (and is not reduced in the way I would expect). I think I am missing something obvious about normalization, but what is the canonical way to do this in F*? Bonus points if the solution points to the "case"/assertion that failed if there exists one.

Solution

  • F*'s type system only ensures weak normalization of terms. Well-typed open terms can diverge, e.g., when reduced in an inconsistent context. To guard against this, the F* normalizer employs various heuristics and, by default, conservatively refuses to reduce recursive calls in the bodies of unreduced matches. This is what prevents List.mem from reducing fully to a cascade of unreduced if/then/else's (if/then/else is just sugar for a match on a Boolean).

    List.memP, a related function from F*'s standard library is more reduction friendly in this case, since it does not block on unreduced matches internally. Note, List.memP need not always be more reduction friendly than List.mem---the latter is Boolean, so it can in some cases compute more (e.g., List.mem 3 [1;2;3] will reduce just fine to true);

    Try this program:

    module Minimal
open FStar.Tactics

let lst = [0;1;2;3;4;5;6;7;8;9;10]

let prop i =
  match i with
  | 0 -> i == 0
  | 1 -> i == 1
  | 2 -> i == 2
  | 3 -> i == 3
  | 4 -> i == 4
  | 5 -> i == 5
  | 6 -> i == 6
  | 7 -> i == 7
  | 8 -> i == 8
  | 9 -> i == 9
  | 10 -> i == 10
  | _ -> False

let propHolds (i:int) =
  assert (List.memP i lst ==> prop i) 
      by (dump "A";
          norm [delta_only [`%List.memP; `%lst]; iota; zeta; simplify];
          dump "B")

    At dump B, you'll see the hypothesis reduced to a nested disjunction. Z3 can prove the goal easily from there.

    Here's another way to do it, this time without tactics.

    let trigger_norm (a:Type) 
  : Lemma
    (requires a)
    (ensures (Pervasives.norm [delta_only [`%List.memP; `%lst]; iota; zeta; simplify] a))
  = ()


let propHolds (i:int) 
  : Lemma
    (requires List.memP i lst)
    (ensures prop i)
  = trigger_norm (List.memP i lst)

    Now, in response to jebus' comment below, you can go further and prove the postcondition using a tactic, although, the SMT solver is really pretty fast at doing this … so I wouldn't use a tactic for this unless you had some specific strong reason for doing so.

    Here's one more solution:

    module SO
open FStar.Tactics

let lst = [0;1;2;3;4;5;6;7;8;9;10]

let pred i =
  match i with
  | 0 -> i == 0
  | 1 -> i == 1
  | 2 -> i == 2
  | 3 -> i == 3
  | 4 -> i == 4
  | 5 -> i == 5
  | 6 -> i == 6
  | 7 -> i == 7
  | 8 -> i == 8
  | 9 -> i == 9
  | 10 -> i == 10
  | _ -> False

let case_impl (a b c:Type) 
  : Lemma
    (requires (a ==> c) /\ (b ==> c))
    (ensures (a \/ b) ==> c) 
  = ()

let solve_pred_impl () : Tac unit =
    let eq = implies_intro () in
    rewrite eq;
    norm [delta_only [`%pred]; iota];
    trivial()

let test i =  
  assert (List.memP i lst ==> pred i)
      by (norm [delta_only [`%List.memP; `%lst]; iota; zeta; simplify];
          let _ = repeat 
            (fun () ->
              mapply (`case_impl); 
              split();
              solve_pred_impl()) in
          solve_pred_impl())