Использование нормализатора для уменьшения рекурсивной функции

Question

Я хочу доказать свойство, параметризованное для конечного числа случаев. Я хотел бы разделить проблему на один экземпляр для каждого случая и решить каждый экземпляр отдельно. Вот пример, чтобы прояснить ситуацию:

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))

В этом случае случаи определяются списком lst. Я могу легко доказать 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 ())

но я, очевидно, не хочу писать отдельный assert_by_tactic для каждого случая (не тогда, когда их может быть несколько тысяч...). Я как-то хочу автоматически сгенерировать приведенное выше доказательство для всех элементов в lst.

Я пробовал разные вещи, вот одна из них:

  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")

К сожалению, это не совсем то, что я хотел бы, assert_by_tactic не удается (и не уменьшается, как я ожидал). Я думаю, что упускаю что-то очевидное в нормализации, но какой канонический способ сделать это в F*? Бонусные баллы, если решение указывает на "дело" / утверждение, которое провалилось, если оно существует.

Answer 1

Система типов F* обеспечивает слабую нормализацию терминов. Правильно типизированные открытые термины могут расходиться, например, при сокращении в противоречивом контексте. Чтобы защититься от этого, нормализатор F* использует различные эвристические методы и по умолчанию консервативно отказывается сокращать рекурсивные вызовы в теле невосстановленных совпадений. Это то, что препятствует тому, чтобы List.mem полностью превратился в каскад невосстановленных if/then/else (если / then / else - просто сахар для совпадения с логическим значением).

List.memPСвязанная функция из стандартной библиотеки F* в этом случае более удобна для сокращения, так как она не блокирует внутренние преобразования. Обратите внимание, что List.memP не всегда должен быть более дружественным по отношению к сокращению, чем List.mem- последний является логическим, поэтому в некоторых случаях он может вычислять больше (например, List.mem 3 [1;2;3] уменьшит просто отлично до true);

Попробуйте эту программу:

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")

В dump Bвы увидите, что гипотеза сводится к вложенной дизъюнкции. Z3 может доказать цель легко оттуда.

Вот еще один способ сделать это, на этот раз без тактики.

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)

Теперь, в ответ на комментарий Jebus ниже, вы можете пойти дальше и доказать постусловие, используя тактику, хотя решатель SMT действительно довольно быстро это делает... поэтому я бы не стал использовать тактику для этого, если у вас нет какой-то конкретной веская причина для этого.

Вот еще одно решение:

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())