Доказательство прецедентным анализа в Coq

Question

Я пытаюсь доказать предложение о следующей функции:

Program Fixpoint division (m:nat) (n:nat) {measure m} : nat := 
match lt_nat 0 n with 
    | false => 0 
    | true => match leq_nat n m with 
     | false => 0 
     | true => S (division (menos m n) n) 
    end 
end. 

menos естественно вычитание.

Я пытаюсь доказать некоторый факт, связанный с делением. Я записал неофициальное доказательство, прежде всего, рассмотрел анализ случая в lt_nat 0 n, а затем в случае, когда lt_nat является истинным, еще один анализ случая в leq_nat n m. Это делается для того, чтобы уменьшить определение деления.

Однако я не могу найти, как выразить этот анализ случая в Coq. Я пробовал с destruct (leq_nat n m), но он ничего не делает. Я ожидаю, что Coq сгенерирует два подцеля: один, где мне нужно доказать мое предложение, предполагая, что leq_nat n m = false и один принимают leq_nat n m = true.

Кроме того, я не могу развернуть определение деления в моем доказательстве! Когда я попробую unfold division, я получаю: division_func (existT (fun _ : nat => nat) m n).

Как я могу проанализировать анализ случаев в leq_nat n m? Почему я не могу развернуть определение деления, как я обычно делаю с другими функциями?

спасибо.

Answer 1

Все более сложное, чем обычно, из-за Program Fixpoint, которое не определяет вашу функцию, как вы ожидали бы, с классическим Fixpoint, так как ему нужно найти структурно рекурсивный способ его определения. То, что division действительно есть, скрыто в division_func.

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

Lemma division_eq : forall m n, division m n = match lt_nat 0 n with 
| false => 0 
    | true => match leq_nat n m with 
     | false => 0 
     | true => S (division (menos m n) n) 
    end 
end. 

Теперь вопрос заключается в том, как доказать этот результат. Вот единственное решение, которое я знаю, которое я считаю неудовлетворительным.

Я использую тактику fix_sub_eq, расположенную в Program.Wf, или fix_sub_eq_ext в Program.Wf.WfExtensionality.

Это дает что-то вроде:

Proof. 
    intros. 
    unfold division. unfold division_func at 1. 
    rewrite fix_sub_eq; repeat fold division_func. 
    - simpl. destruct (lt_nat 0 n) eqn:H. 
    destruct (leq_nat n m) eqn:H0. reflexivity. 
    reflexivity. reflexivity. 

Но вторая цель является довольно сложным. Легкий и общий способ его решения - использовать аксиомы proof_irrelevance и functional_extensionality. Должна быть возможность доказать этот конкретный подцель без каких-либо аксиом, но я не нашел правильного пути для этого. Вместо того, чтобы вручную применять аксиомы, вы можете использовать вторую тактику fix_sub_eq_ext, которая называет их напрямую, оставив вам одну цель.

Proof. 
    intros. 
    unfold division. unfold division_func at 1. 
    rewrite fix_sub_eq_ext; repeat fold division_func. 
    simpl. destruct (lt_nat 0 n) eqn:H. 
    destruct (leq_nat n m) eqn:H0. reflexivity. 
    reflexivity. reflexivity. 
Qed. 

Я не нашел лучший способ использовать Program Fixpoint, поэтому я предпочитаю использовать Function, который имеет другие значения по умолчанию, но генерирует непосредственно уравнение леммы.

Require Recdef. 
Function division (m:nat) (n:nat) {measure (fun n => n) m} : nat := 
match lt_nat 0 n with 
    | false => 0 
    | true => match leq_nat n m with 
     | false => 0 
     | true => S (division (menos m n) n) 
    end 
end. 
Proof. 
    intros m n. revert m. induction n; intros. 
    - discriminate teq. 
    - destruct m. discriminate teq0. 
    simpl. destruct n. destruct m; apply le_n. 
    transitivity m. apply IHn. reflexivity. assumption. apply le_n. 
Qed. 

Check division_equation. 

Теперь у вас есть лемма уравнений, вы можете переписать ее с ней, как обычно.

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