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

В этом случае вам действительно не нужна хорошо обоснованная рекурсия во всей ее общности:

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.

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

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

В Изабель мы можем дать внешнюю лемму, которая показывает, что 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.