Докажите, что что-то меньше или равно другому, используя индукцию в COQ.

Question

Мне нужно доказать, что высота дерева формулы всегда меньше количества узлов одного и того же дерева, но я застрял после предположения и не знаю, как поступить. Может ли кто-нибудь помочь мне заполнить «признать». пространства?

Require Import String.
Require Import Init.Nat.
Require Import PeanoNat.
Require Import Plus.
Require Import Le.

Theorem le_plus_trans2 : forall n m p, (n <= m) -> (n <= p + m).

Proof.
 intros n m p.
 intros x.
 apply le_trans with (m:= m).
 assumption.
 admit.
Qed.

Answer 1

Если вы Require Import Coq.omega.Omega, вы можете заменить все свои admit s на omega.

В качестве альтернативы, если вам нужно менее удачное решение, вы можете заменить свои admit sс

 etransitivity; [ eassumption | apply le_plus_l || apply le_plus_r ].

То есть вы можете использовать тот факт, что x <= x + y и y <= x + y, для x : nat и y : nat.

Редактировать (после вашего обновления вопроса).Ваш вопрос теперь содержит совершенно другую цель, но эта цель все еще может быть решена стандартным арифметическим молотком.Если вы Require Import Coq.omega.Omega, вся ваша теорема доказана intros; omega.

Answer 2

Попробуйте использовать Plus.le_plus_trans и PeanoNat.Nat.add_comm.