Вложенная рекурсия и `Program Fixpoint` или`Function`

Question

Я хотел бы определить следующую функцию, используя Program Fixpoint или же Function в Coq:

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Wf.
Require Import Recdef.

Inductive Tree := Node : nat -> list Tree -> Tree.

Fixpoint height (t : Tree) : nat :=
  match t with
   | Node x ts => S (fold_right Nat.max 0 (map height ts))
  end.

Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map (fun t => mapTree f t) ts)
  end.
Next Obligation.

К сожалению, на данный момент у меня есть обязательство доказать height t < height (Node x ts) не зная, что t является членом ts,

Аналогично с Function вместо Program Fixpoint, только это Function обнаруживает проблему и отменяет определение:

Error:
the term fun t : Tree => mapTree f t can not contain a recursive call to mapTree

Я ожидал бы получить доказательство обязательства In t ts → height t < height (Node x ts),

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

Isabelle

Чтобы оправдать это ожидание, позвольте мне показать, что происходит, когда я делаю то же самое в Изабель, используя function команда, которая (AFAIK) связана с Coq Function команда:

theory Tree imports Main begin

datatype Tree = Node nat "Tree list"

fun height where
  "height (Node _ ts) = Suc (foldr max (map height ts) 0)"

function mapTree where
  "mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"
by pat_completeness auto

termination
proof (relation "measure (λ(f,t). height t)")
  show "wf (measure (λ(f, t). height t))" by auto
next
  fix f :: "nat ⇒ nat" and x :: nat  and ts :: "Tree list" and t
  assume "t ∈ set ts"
  thus "((f, t), (f, Node x ts))  ∈ measure (λ(f, t). height t)"
    by (induction ts) auto
qed

В доказательство прекращения я получаю предположение t ∈ set ts,

Обратите внимание, что Изабель здесь не требует ручного подтверждения завершения, и следующее определение работает просто отлично:

fun mapTree where
  "mapTree f (Node x ts) = Node (f x) (map (λ t. mapTree f t) ts)"

Это работает, потому что map функция имеет "конгруэнтную лемму" вида

xs = ys ⟹ (⋀x. x ∈ set ys ⟹ f x = g x) ⟹ map f xs = map g ys

что function Команда использует, чтобы выяснить, что доказательство прекращения нужно только рассмотреть t ∈ set ts..

Если такая лемма недоступна, например, потому что я определяю

definition "map' = map"

и использовать это в mapTreeЯ получаю то же недоказуемое доказательство, что и в Coq. Я могу заставить его работать снова, объявив конгруэнтную лемму для map'например, используя

declare map_cong[folded map'_def,fundef_cong]

Answer 1

В общем, было бы целесообразно избежать этой проблемы. Но если кто-то действительно хочет получить обязательство по доказательству, которое дает Изабель, вот один из способов:

В Изабель, мы можем дать внешнюю лемму, которая map применяет свои аргументы только к членам данного списка. В Coq мы не можем сделать это во внешней лемме, но мы можем сделать это в типе. Так что вместо нормального типа карты

forall A B, (A -> B) -> list A -> list B

мы хотим, чтобы тип сказал "f применяется только к элементам списка:

forall A B (xs : list A), (forall x : A, In x xs -> B) -> list B

(Требуется изменить порядок аргументов так, чтобы тип f могу упомянуть xs).

Написание этой функции не тривиально, и мне было проще использовать пробный скрипт:

Definition map {A B} (xs : list A) (f : forall (x:A), In x xs -> B) : list B.
Proof.
  induction xs.
  * exact [].
  * refine (f a _ :: IHxs _).
    - left. reflexivity.
    - intros. eapply f. right. eassumption.
Defined.

Но вы также можете написать это "от руки":

Fixpoint map {A B} (xs : list A) : forall (f : forall (x:A), In x xs -> B), list B :=
  match xs with
   | [] => fun _ => []
   | x :: xs => fun f => f x (or_introl eq_refl) :: map xs (fun y h => f y (or_intror h))
  end.

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

Program Fixpoint mapTree (f : nat -> nat) (t : Tree)  {measure (height t)} : Tree :=
  match t with 
    Node x ts => Node (f x) (map ts (fun t _ => mapTree f t))
  end.
Next Obligation.

и мне не нужно ничего делать с новым аргументом f, но это проявляется в обязательстве о прекращении действия, так как In t ts → height t < height (Node x ts) по желанию. Так что я могу доказать это и определить mapTree:

  simpl.
  apply Lt.le_lt_n_Sm.
  induction ts; inversion_clear H.
  - subst. apply PeanoNat.Nat.le_max_l.
  - rewrite IHts by assumption.
    apply PeanoNat.Nat.le_max_r.
Qed.

Работает только с Program Fixpoint, не с Function, к несчастью.

Answer 2

В этом случае вам фактически не нужна обоснованная рекурсия в ее полной общности:

Require Import Coq.Lists.List.

Set Implicit Arguments.

Inductive tree := Node : nat -> list tree -> tree.

Fixpoint map_tree (f : nat -> nat) (t : tree) : tree :=
  match t with
  | Node x ts => Node (f x) (map (fun t => map_tree f t) ts)
  end.

Coq в состоянии понять, что рекурсивные вызовы map_tree выполняются на строгих условиях. Однако доказать что-либо об этой функции сложно, так как принцип индукции, созданный для tree не полезно:

tree_ind : 
  forall P : tree -> Prop, 
    (forall (n : nat) (l : list tree), P (Node n l)) ->
    forall t : tree, P t

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

Require Import Coq.Lists.List.
Import ListNotations.

Unset Elimination Schemes.
Inductive tree := Node : nat -> list tree -> tree.
Set Elimination Schemes.

Fixpoint tree_ind
  (P : tree -> Prop)
  (IH : forall (n : nat) (ts : list tree),
          fold_right (fun t => and (P t)) True ts ->
          P (Node n ts))
  (t : tree) : P t :=
  match t with
  | Node n ts =>
    let fix loop ts :=
      match ts return fold_right (fun t' => and (P t')) True ts with
      | [] => I
      | t' :: ts' => conj (tree_ind P IH t') (loop ts')
      end in
    IH n ts (loop ts)
  end.

Fixpoint map_tree (f : nat -> nat) (t : tree) : tree :=
  match t with
  | Node x ts => Node (f x) (map (fun t => map_tree f t) ts)
  end.

Unset Elimination Schemes Команда не дает Coq генерировать свой принцип индукции по умолчанию (и не полезный) для tree, Возникновение fold_right на индукции гипотеза просто выражает, что предикат P трюмы каждого дерева t' появляется в ts,

Вот утверждение, которое вы можете доказать, используя этот принцип индукции:

Lemma map_tree_comp f g t :
  map_tree f (map_tree g t) = map_tree (fun n => f (g n)) t.
Proof.
  induction t as [n ts IH]; simpl; f_equal.
  induction ts as [|t' ts' IHts]; try easy.
  simpl in *.
  destruct IH as [IHt' IHts'].
  specialize (IHts IHts').
  now rewrite IHt', <- IHts.
Qed.

Answer 3

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