Когда я используюFunction чтобы определить неструктурно-рекурсивную функцию в Coq, результирующий объект ведет себя странно, когда запрашивается конкретное вычисление. На самом деле, вместо того, чтобы давать непосредственно результат,Eval compute in ... директива возвращает довольно длинное (обычно 170 000 строк) выражение. Кажется, что Coq не может оценить все и поэтому возвращает упрощенное (но длинное) выражение вместо просто значения.

Кажется, проблема в том, как я докажу обязательства,Function, Сначала я подумал, что проблема возникла из-за непрозрачных терминов, которые я использовал, и я преобразовал все леммы в прозрачные константы. Кстати, есть ли способ перечислить непрозрачные термины, появляющиеся в термине? Или любой другой способ превратить непрозрачные леммы в прозрачные?

Затем я заметил, что проблема возникла более точно из доказательства того, что используемый порядок обоснован. Но я получил странные результаты.

Например, я определяюlog2 на натуральные числа путем многократного примененияdiv2, Вот определение:

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | n => S (log2 (Nat.div2 n))
  end.

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

forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)

intros. apply Nat.lt_div2. apply le_n_S. apply le_0_n.

Второй проверяет, чтоlt это обоснованный заказ. Это уже доказано в стандартной библиотеке. Соответствующая леммаCoq.Arith.Wf_nat.lt_wf.

Если я использую это доказательство, результирующая функция ведет себя нормально.Eval compute in log24 10. возвращается3.

Но если я хочу сделать доказательство самостоятельно, я не всегда получаю такое поведение. Во-первых, если я закончу доказательствоQed вместоDefinedрезультат вычисления (даже для небольших чисел) представляет собой сложное выражение, а не одно число. Так что я используюDefined и попробуйте использовать только прозрачные леммы.

Lemma lt_wf2 : well_founded lt.
Proof.
  unfold well_founded. intros n.
  apply (lemma1 n). clear n.
  intros. constructor. apply H.
Defined.

Здесь лемма 1 является доказательством обоснованной индукции на натуральные числа. Здесь я снова могу использовать уже существующие леммы, такие какlt_wf_ind, lt_wf_rec, lt_wf_rec1 находится вCoq.Arith.Wf_nat, или дажеwell_founded_ind lt_wf, Первый не работает, кажется, потому что он непрозрачный. Три других работают.

Я пытался доказать это напрямую, используя стандартную индукцию по натуральным числам,nat_ind, Это дает:

Lemma lemma1 : forall n (P:nat -> Prop),
  (forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
  intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
  simpl in H0. apply H0 with (n:=S n).
  - intros. inversion H1.
  - intros. inversion H2.
    + apply H. exact H1.
    + apply H1. assumption.
  - apply le_n.
Defined.

С этим доказательством (и некоторыми его вариантами),log2 имеет такое же странное поведение. И в этом доказательстве используются только прозрачные объекты, поэтому, возможно, проблема не в этом.

Как я могу определитьFunction что возвращает понятные результаты по конкретным значениям?