Определение функции интервала в Coq

Question

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

Как вы можете видеть, я использую хорошо обоснованную рекурсию по длине интервала. Я определяю меру как это значение, т. Е. S n - m.

я бы ожидать, чтобы попросить доказательства того, что forall m, n, true = m <= n -> S n - S m < S n - m

Однако обязательства доказательство, что я получаю не похожи на это и довольно запутанным. Я попросил, чтобы доказать, что:

m : nat 
    n : nat 
    intervalo : forall m0 n0 : nat, 
       match m0 with 
       | 0 => S n0 
       | S l => n0 - l 
       end < match m with 
        | 0 => S n 
        | S l => n - l 
        end -> list nat 
    Heq_anonymous : true = (m <= n) 
    ============================ 
    n - m < match m with 
      | 0 => S n 
      | S l => n - l 
      end 

И что:

============================ 
    well_founded 
    (Wf.MR lt 
     (fun recarg : {_ : nat & nat} => 
     match projT1 recarg with 
     | 0 => S (projT2 recarg) 
     | S l => projT2 recarg - l 
     end)) 

Может кто-то пожалуйста, объясните мне, почему Coq просит меня, чтобы доказать это, вместо того, чтобы просто forall m, n, true = m <= n -> S n - S m < S n - m. Кроме того, как я могу закончить это доказательство? Или как я могу заставить его больше походить на то, что я ожидаю, что Кок попросит у меня доказательства?

спасибо.

Answer 1

Что смущает вас, так это то, что термин S n - m частично раскрыт и что у вас есть дополнительная гипотеза. Если вы наберете:

clear intervalo. 
change (match m with 
     | 0 => S n 
     | S l => n - l 
     end) with (S n - m). 
change (n - m) with (S n - S m). 

, то вы увидите, что первая цель вы попросили, чтобы доказать это на самом деле является прямым следствием forall m, n, true = m <= n -> S n - S m < S n - m.

Вторая заявка заключается в том, что ваша мера является обоснованной (еще раз с некоторой степенью разворачивания S n - m). У меня, вероятно, есть другая версия Coq (версия 8.5beta2), потому что в моем случае эта вещь выгружается автоматически.