Пользовательский принцип индукции для взаимно рекурсивных типов

Question

Я немного запутался, пытаясь определить принцип индукции для некоторого конкретного взаимно рекурсивного типа.Использование Schema на самом деле не решает мою проблему, поэтому я подумал об определении самого принципа (может быть, весь мой подход с использованием взаимно рекурсивных типов не подходит ... это тоже вариант).

Я используюБиблиотека Артура extructure (вот откуда взялась ordType, это может быть что-то еще).Итак, мой тип:

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


From extructures Require Import ord fmap.

Section R.

Variables Name Vals : ordType.

Inductive ResponseObject : Type :=
  | SingleResponse : Result -> ResponseObject
  | MultipleResponses : Result -> ResponseObject -> ResponseObject
  with Result : Type :=
       | Empty : Result
       | Null : Name -> Result
       | SingleResult : Name -> Vals -> Result
       | ListResult : Name -> seq Vals -> Result
       | NestedResult : Name -> ResponseObject -> Result
       | NestedListResult : Name -> seq ResponseObject -> Result.

Это в основном непустой список Result объектов, которые сами могут содержать непустые списки (NestedResult и NestedListResult).

Моя проблема связана со случаем NestedListResult, поскольку принцип индукции, сгенерированный с помощью Schema, не проверяет каждый элемент в списке ResponseObject.В нем говорится следующее:

Scheme ResponseObject_ind := Induction for ResponseObject Sort Prop
    with Result_ind := Induction for Result Sort Prop.

Check ResponseObject_ind.
ResponseObject_ind
     : forall (P : ResponseObject -> Prop) (P0 : Result -> Prop),
       (forall r : Result, P0 r -> P (SingleResponse r)) ->
       (forall r : Result, P0 r -> forall r0 : ResponseObject, P r0 -> P (MultipleResponses r r0)) ->
       P0 Empty ->
       (forall s : Name, P0 (Null s)) ->
       (forall (s : Name) (s0 : Vals), P0 (SingleResult s s0)) ->
       (forall (s : Name) (l : seq Vals), P0 (ListResult s l)) ->
       (forall (s : Name) (r : ResponseObject), P r -> P0 (NestedResult s r)) ->
       (forall (s : Name) (l : seq ResponseObject), P0  (NestedListResult s l)) -> forall r : ResponseObject, P r

Я пытался следовать примеру из SSReflect GenTree (где он в основном сворачивается по списку и проверяет, что каждый элемент удовлетворяет предикату), но я получаю синтаксисошибка при попытке определить это (я думаю, это синтаксическая ошибка?), и я не уверен, как это исправить.Я предполагаю, что использование fix и with не правильно, и я должен написать это по-другому?

Моя попытка заключается в следующем:

Definition ResponseObject_ind P Ps IH_SingleResponse IH_MultipleResponses IH_Empty IH_Null IH_SingleResult IH_ListResult IH_NestedResult IH_NestedListResult :=
    fix loop (r : ResponseObject) : P r : Prop :=
       match r with
       | SingleResponse r' => IH_SingleResponse r' (Result_ind r')
       | MultipleResponses r' rs => IH_MultipleResponses r' (Result_ind r') rs (loop rs)
       end
      with Result_ind (r : Result) : Ps r : Prop :=
       match r with
       | Empty => IH_Empty
       | Null l => IH_Null l
       | SingleResult l v => IH_SingleResult l v
       | ListResult l vals => IH_ListResult l vals
       | NestedResult l r' => IH_NestedResult l r' (Result_ind r')
       | NestedListResult l rs =>
         let fix iter_conj rs : foldr (fun r => and (P r)) True rs :=
             if rs is r :: rs' then conj (loop r) (iter_conj rs') else Logic.I
         in
         IH_NestedListResult l rs (iter_conj rs)
       end.

Любая помощь будет оценена:)

PS.На самом деле, может быть, какой-то другой подход лучше, чем использование взаимно рекурсивных типов ... До того, как я использовал ResponseObject в качестве другого конструктора для типа Result и проверил, что он формирует "правильный" список (без формирования вложенных ResponseObject s)странная вещь из дерева).Этот вариант выше кажется более элегантным, но, возможно, он не слишком удобен.

Answer 1

Ваше решение не учитывает синтаксис и ограничения ввода.Один из способов исправить эти ограничения приводит к следующему коду:

Definition ResponseObject_ind' (P : ResponseObject -> Prop) 
 (Ps : Result -> Prop) IH_SingleResponse IH_MultipleResponses IH_Empty IH_Null
IH_SingleResult IH_ListResult
(IH_NestedResult : forall (s : Name) (r : ResponseObject),
   P r -> Ps (NestedResult s r))
IH_NestedListResult :=
fix loop (r : ResponseObject) : P r : Prop :=
   match r with
   | SingleResponse r' => IH_SingleResponse r' (Result_ind r')
   | MultipleResponses r' rs => IH_MultipleResponses r' (Result_ind r') rs (loop rs)
   end
  with Result_ind (r : Result) : Ps r : Prop :=
   match r with
   | Empty => IH_Empty
   | Null l => IH_Null l
   | SingleResult l v => IH_SingleResult l v
   | ListResult l vals => IH_ListResult l vals
   | NestedResult l r' => IH_NestedResult l r' (loop r')
   | NestedListResult l rs =>
     let fix iter_conj rs : foldr (fun r => and (P r)) True rs :=
         if rs is r :: rs' then conj (loop r) (iter_conj rs') else Logic.I
     in
     IH_NestedListResult l rs (iter_conj rs)
   end
 for loop.

Мне не нравится ваше решение iter_conj.

По моему мнению, вы на самом деле создаете кучуиндуктивные типы, которые содержат три индуктивных типа: ResponseObject, Result и seq ResponseObject.Поэтому вместо того, чтобы ваш принцип индукции брал два предиката P и Ps, у вас должно быть три предиката: P для типа ResponseObject, Ps для Result и Pl для seq ResponseObject.Вот мое решение, следующее за этими строками:

Definition RO_ind := fun
  P P0 P1 
  (f : forall r : Result, P0 r -> P (SingleResponse r))
  (f0 : forall r : Result,
        P0 r ->
        forall r0 : ResponseObject, P r0 -> P (MultipleResponses r r0))
  (f1 : P0 Empty) (f2 : forall n : Name, P0 (Null n))
  (f3 : forall (n : Name) (v : Vals), P0 (SingleResult n v))
  (f4 : forall (n : Name) (l : seq Vals), P0 (ListResult n l))
  (f5 : forall (n : Name) (r : ResponseObject), P r -> P0 (NestedResult n r))
  (f6 : forall (n : Name) (l : seq ResponseObject),
          P1 l -> P0 (NestedListResult n l))
  (f7 : P1 [::])
  (f8 : forall (ro : ResponseObject),  P ro ->
       forall (l : seq ResponseObject),
       P1 l -> (P1 (ro :: l))) (ro : ResponseObject) =>
fix F (r : ResponseObject) : P r :=
  match r as r0 return (P r0) with
  | SingleResponse r0 => f r0 (F0 r0)
  | MultipleResponses r0 r1 => f0 r0 (F0 r0) r1 (F r1)
  end
with F0 (r : Result) : P0 r :=
  match r as r0 return (P0 r0) with
  | Empty => f1
  | Null n => f2 n
  | SingleResult n v => f3 n v
  | ListResult n l => f4 n l
  | NestedResult n r0 => f5 n r0 (F r0)
  | NestedListResult n l => f6 n l
    ((fix F1 l' : P1 l' :=
       match l' with
       | [::] => f7
       | ro :: l' => f8 ro (F ro) l' (F1 l')
       end) l)
  end
for F0.

Это решение было получено путем вызова команды Scheme и последующего редактирования заголовка (для добавления P1 и f7 и f8 для последовательностей)и, наконец, редактирование регистра конструкции NestedListResult.