Метод Бове-Капретты в Coq - PullRequest
Новая
       48

Метод Бове-Капретты в Coq

0 голосов
/ 03 июня 2018

В качестве упражнения по определению общих рекурсивных функций в Coq я пытаюсь реализовать функцию слияния списков, используя специальный предикат, так называемый метод Bove-Capretta.

Для этого я следую схеме в примере для функции log2 в главе 15 Бертота и Кастерана.Сначала я определил доменный предикат для слияния следующим образом: 

Inductive merge_acc : list nat -> list nat -> Prop :=
 | Merge1 : forall xs, merge_acc xs nil
 | Merge2 : forall ys, merge_acc nil ys 
 | Merge3 : forall x y xs ys,
      x <= y -> merge_acc xs (y :: ys) -> merge_acc (x :: xs) (y :: ys)
 | Merge4 : forall x y xs ys,
      x > y -> merge_acc (x :: xs) ys -> merge_acc (x :: xs) (y :: ys).

Далее я определил соответствующие леммы обращения для рекурсивных вызовов merge: 

 Ltac inv H := inversion H ; subst ; clear H.

 Lemma merge_acc_inv3
     : forall xs ys x y,
        merge_acc (x :: xs) (y :: ys) -> 
        x <= y -> 
        merge_acc xs (y :: ys).
 Proof.
    induction xs ; destruct ys ; intros x y H Hle ; inv H ; eauto ; try omega.
 Defined.

 Lemma merge_acc_inv4
    : forall xs ys x y, 
        merge_acc (x :: xs) (y :: ys) -> 
        x > y -> 
       merge_acc (x :: xs) ys.
 Proof.
   induction xs ; destruct ys ; intros x y H Hxy ; inv H ; eauto ; try omega.
 Defined.

После этихопределения, я пробовал следующую реализацию merge: 

 Fixpoint merge_bc 
     (xs ys : list nat)(H : merge_acc xs ys) {struct H}: list nat :=
     match xs, ys with
     | nil, ys => ys
     | xs , nil => xs
     | (x :: xs) , (y :: ys) =>
        match le_gt_dec x y with
        | left _ h1 => x :: merge_bc (merge_acc_inv3 xs ys x y H h1) 
        | right _ h2 => y :: merge_bc (x :: xs) ys (merge_acc_inv4 _ _ _ _ H h2)
        end 
     end.

Но я получаю сообщение об ошибке, которое, похоже, связано с отсутствием уточнения типа в сопоставлении с образцом: 

    The term "H" has type "merge_acc xs ys" while it is expected to have type
       "merge_acc (x :: xs0) (y :: ys0)".

Далее я попытался определить merge, используя тактику refine: 

  Definition merge_bc : forall xs ys, merge_acc xs ys -> list nat.
     refine (fix merge_bc xs ys (H : merge_acc xs ys) {struct H}: list nat :=
        match xs as xs' return xs = xs' -> list nat with
        | nil => fun _ => ys
        | x :: xs => fun _ =>
          (match ys as ys' return ys = ys' -> list nat with
           | nil => fun _ => x :: xs
           | y :: ys => fun _ =>
             match le_gt_dec x y with
             | left _ Hle => x :: merge_bc xs (y :: ys) _
             | right _ Hgt => y :: merge_bc (x :: xs) ys _
             end
           end (eq_refl ys))
        end (eq_refl xs)).
     +
       subst.
       apply merge_acc_inv3 with (x := x).
       exact H. exact Hle.
    +
       subst.
       apply merge_acc_inv4 with (y := y).
       exact H.
       exact Hgt.
  Defined.

И Coq возвращает следующее сообщение об ошибке: 

 Recursive call to merge_bc has principal argument equal to
    "eq_ind_r
        (fun xs1 : list nat => merge_acc xs1 ys -> merge_acc xs0 (y :: ys0))
        (fun H : merge_acc (x :: xs0) ys => ...

, которое я упростилнемного.Кажется, что рекурсия не была сделана на структурно меньшем подтерме merge_acc xs ys.

Мой вопрос: что я делаю не так?Я что-то упустил?

Полный рабочий пример приведен на следующем gist .

EDIT : Исправление правописания Кастерана.

1 Ответ

0 голосов
/ 04 июня 2018

Я думаю, что проблема здесь в том, что тот факт, что вы используете подтерму H, скрыт ненужным усложнением, которое вы ввели в определения merge_acc_inv3 и merge_acc_inv4.Нет необходимости в induction xs.

Кроме того, во время сопоставления с шаблоном на xs и ys вы теряете соединение с xs и ys в типеH.Итак, вот что у меня есть:

  • Инверсионные леммы без induction и более простые в использовании (см. Использование ограничений равенства xxs = x :: xs) 
  Lemma merge_acc_inv3
     : forall xs ys x y xxs yys,
        xxs = x :: xs -> yys = y :: ys ->
        merge_acc xxs yys ->
        x <= y ->
        merge_acc xs yys.
 Proof.
    intros xs ys x y xxs yys eqx eqy H Hle;
    subst; inv H ; eauto ; try omega.
 Defined.

 Lemma merge_acc_inv4
    : forall xs ys x y xxs yys,
      xxs = x :: xs -> yys = y :: ys ->
      merge_acc xxs yys ->
      x > y ->
     merge_acc xxs ys.
 Proof.
   intros xs ys x y xxs yys eqx eqy H Hxy ;
   subst ; inv H ; eauto ; try omega.
 Defined.
  • Зависимое сопоставление с образцом, которое сохраняет связь между тем, как выглядит совпадение, и оригиналом xs / ys: 
 Fixpoint merge_bc
     (xs ys : list nat)(H : merge_acc xs ys) {struct H}: list nat :=
   (match xs as us, ys as vs return xs = us -> ys = vs -> list nat with
     | nil, ys => fun _ _ => ys
     | xs , nil => fun _ _ => xs
     | (x :: xs) , (y :: ys) =>
        match le_gt_dec x y with
        | left _ h1 => fun eqx eqy =>
            let H' := merge_acc_inv3 _ _ x y _ _ eqx eqy H h1
            in x :: merge_bc _ _ H'
        | right _ h2 => fun eqx eqy =>
            let H' := merge_acc_inv4 _ _ x y _ _ eqx eqy H h2
            in y :: merge_bc _ _ H'
        end 
     end) eq_refl eq_refl.
...