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

Question

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

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

Inductive bool : Type :=
  | true : bool
  | false : bool.

Fixpoint leq_nat (m:nat) (n:nat) : bool :=
match m with
  | 0 => true
  | S x => match n with
    | 0 => false
    | S y => leq_nat x y
  end
end. 

Notation "m <= n" := (leq_nat m n).
Notation "x :: l" := (cons x l) (at level 60, right associativity).

Program Fixpoint intervalo (m:nat) (n:nat) {measure ((S n) - m)}: list nat := 
match m <= n with
  | false => nil
  | true => m :: (intervalo (S m) n)
end.
Next Obligation.

Как видите, я использую обоснованную рекурсию по длине интервала. Я определяю меру, чтобы быть этим значением, то есть 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, Кроме того, как я могу закончить это доказательство? Или как я могу сделать так, чтобы это выглядело так, как я ожидаю, что Coq попросит меня доказать?

Спасибо.

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), потому что в моем случае эта вещь разряжается автоматически.