Блог

У меня есть вопрос о доказательстве того, что функция nat -> QArith .Q (рациональные значения из стандартной библиотеки Coq) монотонны (всегда неубывающие) как часть упражнения по работе с рациональными значениями в Coq. Проблема в том, что я застрял на этапе индукции процесса доказательства. Предположим, я определил функцию следующим образом.

 Definition silly (n:nat) : QArith_base.Q :=
    match n with
    | 0 => 1#1 
    | 1 => 2#1
    | 2 => 3#1
    | 3 => 4#1
    | 4 => 5#1
    | 5 => 6#1
    | S n =>  Z.of_N (N.of_nat(S n))   7#1
    end.
  

Где N.of_nat — определение, которое формализует натуральные числа двоичным способом (https://coq.inria.fr/library/Coq.NArith .BinNatDef.html ) с помощью положительного индуктивного типа (https://coq.inria.fr/library/Coq.Numbers .BinNums.html#N). Z.of_N создает целое число из библиотеки Z, которое будет использоваться конструктором Q, Qmake, для построения рационального числа. Я определил это так, чтобы было «проще определить» функцию (по крайней мере, так я думал).

Допустим, я хочу доказать следующее:

Lemma sillyIsNondecrescent : forall n, Qle (silly n) (silly(S n)) , Qle логическое значение меньше или равно для Q.

Доказательство продолжается нормально, пока я не попаду в ветку (S n), что дает мне следующую подцель:

 (silly (S n) <= silly (S (S n)))%Q
  

что нормально, поскольку я доказываю это с помощью индукции, тогда контекст доказательства таков

 n : nat
IHn : (silly n <= silly (S n))%Q
______________________________________(1/1)
(silly (S n) <= silly (S (S n)))%Q
  

Затем я продолжаю разворачивать определение глупого. Цель разворачивается до:

 (match n with
 | 0 => 5 # 1
 | 1 => 8 # 1
 | 2 => 11 # 1
 | 3 => 14 # 1
 | 4 => 17 # 1
 | S (S (S (S (S _)))) => Z.of_N (N.of_nat (S n))   16 # 1
 end <=
 match n with
 | 0 => 8 # 1
 | 1 => 11 # 1
 | 2 => 14 # 1
 | 3 => 17 # 1
 | S (S (S (S _))) => Z.of_N (N.of_nat (S (S n)))   16 # 1
 end)%Q
  

Затем я продолжаю анализ случая на N, пока не дойду до ветки-преемника. Теперь этап доказательства

 n : nat
IHn : (silly n <= silly (S n))%Q
n0, n1, n2, n3, n4 : nat
______________________________________(1/1)
(Z.of_N (N.of_nat (S (S (S (S (S (S n4)))))))   16 # 1 <=
 Z.of_N (N.of_nat (S (S (S (S (S (S (S n4))))))))   16 # 1)%Q
  

Разворачивая N.of_nat, цель

 (match N.of_nat (S (S (S (S (S (S n4)))))) with
 | 0%N => 0
 | N.pos p => Z.pos p
 end   16 # 1 <=
 match N.of_nat (S (S (S (S (S (S (S n4))))))) with
 | 0%N => 0
 | N.pos p => Z.pos p
 end   16 # 1)%Q
  

и в этом я застрял. Никакой анализ случая на n4 или уничтожение n4 здесь не подойдет, потому что он будет генерировать две цели, каждая для каждого конструктора nat (что и ожидается этой тактикой).

Как я могу исходить из этого? Есть ли более красивый способ продолжить доказательства, подобные этому? Я неправильно определил функцию?

Я чувствую, что мне не хватает чего-то довольно простого. Любые советы будут высоко оценены.

Заранее спасибо, Эрик.

РЕДАКТИРОВАТЬ: следуя ответу Артура, глупый переопределяется как

 silly (n:nat) : QArith_base.Q :=
    if Nat.leb n 5 then Z.of_nat (S n)#1 else Z.of_nat (S n)   7#1
  

рассмотрим следующий подход к доказательству:

 Lemma sillyIsNondecrescent : forall n, Qle (silly n) (silly (S n)).
  Proof.
    intros. case_eq (Nat.leb n 5).
    - intros. unfold silly. rewrite H0. case_eq (Nat.leb (S n) 5).
      intros.
  

дает мне следующий контекст:

 1 subgoal
n : nat
H0 : (n <=? 5) = true
H1 : (S n <=? 5) = true
______________________________________(1/1)
(Z.of_nat (S n) # 1 <= Z.of_nat (S (S n)) # 1)%Q
  

что возвращается к ситуации, аналогичной исходной, представленной здесь. Я, если я явно знаю «n», Coq (очевидно) будет знать, как решить эту задачу. В противном случае я застреваю. Правильно ли я формализовал лемму? Я подумываю о том, чтобы переписать ее в терминах «Qeq_bool», который определен в той же библиотеке (Q), что и

 Definition Qeq_bool x y :=
  (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
  

Есть идеи?

Как правило, доказательство по индукции уместно, когда объект, о котором вы хотите рассуждать, определяется рекурсивно в терминах предшественника числа. Здесь нет рекурсивного шаблона, поэтому индукция вряд ли поможет. Я думаю, было бы проще поступить следующим образом:

1. Переопределите silly как

    silly n := if n <= 5 then S n
              else n   7
     

   (Вставка приведений по мере необходимости, чтобы сделать этот действительный Coq.)

2. Докажите, что silly это монотонно, рассматривая отдельно случаи n < 5 , n = 5 , и n > 5 .