Как бороться с действительно большими терминами, сгенерированными программой Fixpoint в Coq?

Я пытаюсь определить и доказать правильность в Coq функции, которая эффективно выводит два отсортированных списка. Поскольку он не всегда повторяется на структурно меньшем сроке (первый или второй список меньше), Fixpoint не приму это, поэтому я пытаюсь использовать Program Fixpoint вместо.

При попытке доказать свойство функции с помощью тактики simpl или же program_simplCoq тратит минуты на вычисления, а затем выдает гигантский термин, сотни строк. Мне было интересно, если я использую Program Fixpoint неправильный путь или альтернатива, если есть другие тактики, которые следует использовать вместо упрощения при рассуждении об этом?

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

Обратите внимание, что я попытался определить более простую версию make_diff, который только взял l1 и l2 в качестве параметров и зафиксировал тип A и отношение R, но это все еще произвело гигантский термин, когда program_simpl или же simpl тактика была применена.

* Изменить: мои включения (хотя они могут не все здесь):

Require Import Coq.Sorting.Sorted.
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Definitions.
Require Import Recdef.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.

Код:

Definition is_decidable (A : Type) (R : relation A) := forall x y, {R x y} + {~(R x y)}.
Definition eq_decidable (A : Type) := forall (x y : A), { x = y } + { ~ (x = y) }.

Inductive diff (X: Type) : Type :=
  | add : X -> diff X
  | remove : X -> diff X 
  | update : X -> X -> diff X.

Program Fixpoint make_diff (A : Type) 
    (R : relation A)
    (dec : is_decidable A R)
    (eq_dec : eq_decidable A)
    (trans : transitive A R) 
    (lt_neq : (forall x y, R x y -> x <> y))
    (l1 l2 : list A)
     {measure (length l1 + length l2) } : list (diff A) :=
  match l1, l2 with
  | nil, nil => nil
  | nil, (new_h::new_t) => (add A new_h) :: (make_diff A R dec eq_dec trans lt_neq nil new_t)
  | (old_h::old_t), nil => (remove A old_h) :: (make_diff A R dec eq_dec trans lt_neq old_t nil)
  | (old_h::old_t) as old_l, (new_h::new_t) as new_l => 
    if dec old_h new_h 
      then (remove A old_h) :: make_diff A R dec eq_dec trans lt_neq old_t new_l
      else if eq_dec old_h new_h 
        then (update A old_h new_h) :: make_diff A R dec  eq_dec trans lt_neq old_t new_t
        else  (add A new_h) :: make_diff A R dec eq_dec trans lt_neq old_l new_t 
  end.
Next Obligation.
Proof.
  simpl.
  generalize dependent (length new_t).
  generalize dependent (length old_t).
  auto with arith.
Defined.
Next Obligation.
Proof.
  simpl.
  generalize dependent (length new_t).
  generalize dependent (length old_t).
  auto with arith.
Defined.
Источник

2 ответа

Решение

В этом конкретном случае мы можем избавиться от Program Fixpoint и использовать простой простой Fixpoint, Поскольку при каждом рекурсивном вызове мы вызываем make_diff либо в конце первого списка, либо в конце второго списка, мы можем вложить две функции с фиксированной запятой следующим образом. (Я использовал Section механизм здесь, чтобы избежать передачи слишком много одинаковых аргументов)

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Relations.Relations.

Section Make_diff.

Variable A : Type.
Variable R : relation A.
Variable dec : is_decidable A R.
Variable eq_dec : eq_decidable A.
Variable trans : transitive A R.
Variable lt_neq : forall x y, R x y -> x <> y.

Fixpoint make_diff (l1 l2 : list A) : list (diff A) :=
  let fix make_diff2 l2 :=
  match l1, l2 with
  | nil, nil => nil
  | nil, new_h::new_t => (add A new_h) :: make_diff2 new_t
  | old_h::old_t, nil => (remove A old_h) :: make_diff old_t nil
  | old_h::old_t, new_h::new_t =>
    if dec old_h new_h 
    then (remove A old_h) :: make_diff old_t l2
    else if eq_dec old_h new_h 
         then (update A old_h new_h) :: make_diff old_t new_t
         else (add A new_h) :: make_diff2 new_t
  end
  in make_diff2 l2.

End Make_diff.

Обратите внимание, что Section механизм не будет включать неиспользуемые параметры в результирующую подпись. Вот наивный тест:

(* make the first 2 arguments implicit *)    
Arguments make_diff [A R] _ _ _ _.

Require Import Coq.Arith.Arith.

Compute make_diff lt_dec Nat.eq_dec [1;2;3] [4;5;6].
(* = [remove nat 1; remove nat 2; remove nat 3; add nat 4; add nat 5; add nat 6] 
      : list (diff nat) *)
Источник

Для тех, кто сталкивается с проблемой, лучшей альтернативой сейчас является плагин Equations, который в конечном итоге заменит функцию и точку фиксации программы.

Источник
Другие вопросы по тегам