У меня есть вопрос о том, чтобы доказать, что функция 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 (что и ожидается в этой тактике).
Как я могу исходить из этого пункта? Есть ли более красивый способ использовать доказательства, подобные этому? Я неправильно определил функцию?
Я чувствую, что упускаю что-то довольно простое. Любые советы будут с благодарностью.
Заранее спасибо,
Erick.
РЕДАКТИРОВАТЬ: после ответа Артура, глупый переопределяется как
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.
Есть идеи?