Написание обоснованных программ в Coq с использованием Fix или Program Fixpoint

Question

Следуя примеру, приведенному в главе GeneralRec книги Chlipala, я пытаюсь написать алгоритм слияния.

Вот мой код

Require Import Nat. 

Fixpoint insert (x:nat) (l: list nat) : list nat := 
    match l with 
    | nil => x::nil 
    | y::l' => if leb x y then 
       x::l 
      else 
       y::(insert x l') 
    end. 

Fixpoint merge (l1 l2 : list nat) : list nat := 
    match l1 with 
    | nil => l2 
    | x::l1' => insert x (merge l1' l2) 
    end. 

Fixpoint split (l : list nat) : list nat * list nat := 
    match l with 
    | nil => (nil,nil) 
    | x::nil => (x::nil,nil) 
    | x::y::l' => 
    let (ll,lr) := split l' in 
    (x::ll,y::lr) 
    end. 

Definition lengthOrder (l1 l2 : list nat) := 
    length l1 < length l2. 

Theorem lengthOrder_wf : well_founded lengthOrder. 
Admitted. 

Проблема заключается в том, что это не возможно, чтобы написать функцию сортировки слиянием с командой Fixpoint, так как функция структурно не уменьшается:

Fixpoint mergeSort (l: list nat) : list nat := 
    if leb (length l) 1 then l 
    else 
    let (ll,lr) := split l in 
    merge (mergeSort ll) (mergeSort lr). 

Вместо этого один может использовать команду Program Fixpoint или Definition с термином Fix (как в книге Chlipala).

Однако, если я пишу этот

Definition mergeSort : list nat -> list nat. 
refine (Fix lengthOrder_wf (fun (l: list nat) => list nat) 
     (fun (l : list nat) => (fun mergeSort : (forall ls : list nat, lengthOrder ls l -> list nat)=> 
          if leb (length l) 1 then 
          let (ll,lr) := split l in 
          merge (mergeSort ll _) (mergeSort lr _) 
          else 
          l))). 

я получаю невозможные цели:

2 subgoals, subgoal 1 (ID 65) 

    l : list nat 
    mergeSort : forall ls : list nat, lengthOrder ls l -> list nat 
    ll, lr : list nat 
    ============================ 
    lengthOrder ll l 

subgoal 2 (ID 66) is: 
lengthOrder lr l 

Поэтому Chlipala предлагает изменить определение слиянием таким образом:

Definition mergeSort : list nat -> list nat. 
    refine (Fix lengthOrder_wf (fun _ => list nat) 
       (fun (ls : list nat) 
       (mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat) => 
       if Compare_dec.le_lt_dec 2 (length ls) 
       then let lss := split ls in 
         merge (mergeSort (fst lss) _) (mergeSort (snd lss) _) 
       else ls)). 

, который преследует следующие цели:

2 subgoals, subgoal 1 (ID 68) 

    ls : list nat 
    mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat 
    l : 2 <= length ls 
    lss := split ls : list nat * list nat 
    ============================ 
    lengthOrder (fst lss) ls 

subgoal 2 (ID 69) is: 
lengthOrder (snd lss) ls 

Это новое определение звучит как волшебство для меня. Поэтому я задаюсь вопросом:

• Fom первое определение, можно ли еще доказать доказательство правильности функции?
• Иначе почему первое определение не может работать?
• Как простой пользователь может перейти от первого определения ко второму легко?

Answer 1

Легко видеть, что вам нужно сделать два изменения, чтобы добраться до решения А. Хлипалы.

1) При выполнении split вы как-то нужно помнить, что ll и lr пришли из раскола, в противном случае они были бы некоторые произвольные списки, которые не может быть короче первоначального списка l.

Следующий фрагмент кода не удается сохранить такую ​​информацию:

let (ll,lr) := split l in 
    merge (mergeSort ll _) (mergeSort lr _) 

и, таким образом, должен быть заменен

let lss := split ls in 
    merge (mergeSort (fst lss) _) (mergeSort (snd lss) _) 

который держит то, что нам нужно.

Неудача происходит из-за неспособности Coq, чтобы помнить, что ll и lr приходят из split l и что происходит, потому что let (ll,lr) просто match в маскировке (смотрите руководство, §2.2.3).

Напомним, что цели сопоставления с образцом является (грубо говоря)

• распаковывать компоненты некоторого значения индуктивного типа данных и связывания их с некоторыми именами (мы будем нуждаться в этом в Вторая часть моего ответа) и
• замените исходное определение специальными случаями в соответствующих ветвях совпадения шаблонов.

Теперь заметим, что split lне происходят в любой точке цели или контекста, прежде чем мы сопоставления с образцом на нем. Мы просто произвольно вводим его в определение. Вот почему совпадение шаблонов не дает нам ничего - мы не можем заменить split l своим «специальным случаем» ((ll,lr)) в цели или контексте, потому что нет split l в любом месте.

Существует альтернативный способ сделать это с помощью логического равенства (=):

(let (ll, lr) as s return (s = split l -> list nat) := split l in 
    fun split_eq => merge (mergeSort ll _) (mergeSort lr _)) eq_refl 

Это аналогично использования remember тактики. Мы избавились от fst и snd, но это огромный перебор, и я бы не рекомендовал его.

---

2) Еще одна вещь, которую мы должны доказать тот факт, что ll и lr короче l когда 2 <= length l.

Так как if -expression в маскировать match, а также (это работает для любого индуктивного типа данных с точно два конструктора), нам нужен некоторый механизм, чтобы помнить, что leb 2 (length l) = true в then отрасли. Опять же, поскольку мы не имеем leb в любом месте, эта информация теряется.

Есть по крайней мере два возможных решения этой проблемы:

• либо мы помним leb 2 (length l) как уравнение (так же, как мы это делали в 1-й части), или
• мы можем использовать некоторые сравнения функции с тип результата ведет себя как bool (поэтому он может представлять две альтернативы), но он также должен помнить некоторую дополнительную информацию, которая нам нужна. Затем мы могли бы сопоставить образец по результату сравнения и извлечь информацию, которая, конечно же, в этом случае должна быть доказательством 2 <= length l.

Что нам нужно, это тип, который способен нести доказательство в том случае, когда leb m n возвращается true и доказательство, скажем, m > n иначе. В стандартной библиотеке есть тип, который делает именно это! Это называется sumbool:

Inductive sumbool (A B : Prop) : Set := 
    left : A -> {A} + {B} | right : B -> {A} + {B} 

{A} + {B} просто обозначение (синтаксический сахар) для sumbool A B. Точно так же, как bool, он имеет два конструктора, но кроме того, он помнит доказательство любого из двух предложений A и B. Его преимущество перед bool появляется, когда вы делаете анализ ситуации на нем с if: вы получите доказательство A в ветке then и доказательство B в филиале else. Другими словами, вы можете использовать контекст, который вы сохранили заранее, тогда как bool не имеет контекста (только в уме программиста).

И нам нужно именно это! Ну, не в филиале else, но мы хотели бы получить 2 <= length l в нашей ветке then. Итак, давайте спросим Coq, если он уже имеет функцию сравнения с типом возвращаемого значения, как, что:

Search (_ -> _ -> {_ <= _} + {_}). 

(* 
output: 
le_lt_dec: forall n m : nat, {n <= m} + {m < n} 
le_le_S_dec: forall n m : nat, {n <= m} + {S m <= n} 
le_ge_dec: forall n m : nat, {n <= m} + {n >= m} 
le_gt_dec: forall n m : nat, {n <= m} + {n > m} 
le_dec: forall n m : nat, {n <= m} + {~ n <= m} 
*) 

Любой из пяти результатов будет делать, потому что нам нужно доказательство только в одном случае.

Следовательно, мы можем заменить if leb 2 (length l) then ... на if le_lt_dec 2 (length l) ... и получить 2 <= length в контексте доказательства, который позволит нам закончить доказательство.