Программа Fixpoint с взаимной рекурсией с зависимым типом в Coq - PullRequest
Новая
       5

Программа Fixpoint с взаимной рекурсией с зависимым типом в Coq

0 голосов
/ 11 сентября 2018

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

  Require Import Program.

  Variable P : nat -> Prop.

  Program Fixpoint a (n : nat) : sigT P := _
  with b (n : nat) : sigT P := _.
  Next Obligation.

Однако в случае взаимной рекурсии, как указано выше, после перехода в режим проверки a и b больше не видны друг другу. 

1 subgoal (ID 183)

  P : nat -> Prop
  n : nat
  ============================
  {x : nat & P x}

Есть ли способ определить такую ​​вещь, используя преимущества как Program, так и режима доказательства?

...