证明不到

Question

我试图less_than在Coq中证明一些定理.我正在使用这个归纳定义:

Inductive less_than : nat->nat->Prop :=
   | lt1 : forall a, less_than O (S a)
   | lt2 : forall a b, less_than a b -> less_than a (S b)
   | lt3 : forall a b, less_than a b -> less_than (S a) (S b).

我总是需要显示lt3的倒数,

Lemma inv_lt3, forall a b, less_than (S a) (S b) -> less_than a b.
Proof.
   ???

我被困住了,如果有人对如何继续进行提示,我将非常感激.

(我的归纳定义是否有问题less_than？)

谢谢!

Answer 1

首先less_than,在第二个构造函数是多余的意义上,你的定义有点不幸.您应该考虑切换到更简单的方法:

Inductive less_than : nat -> nat -> Prop :=
| ltO : forall a, less_than O (S a)
| ltS : forall a b, less_than a b -> less_than (S a) (S b)
.

然后反演将匹配coq的反演,使你的证明变得微不足道:

Lemma inv_ltS: forall a b, less_than (S a) (S b) -> less_than a b.
Proof. now inversion 1. Qed.

第二个条款是多余的,因为对于每一对(a, b)st.你想要证明less_than a b,你可以随时申请lt3 a,然后申请lt1.lt2事实上,你是其他两个构造函数的结果:

Ltac inv H := inversion H; subst; clear H; try tauto.

(* there is probably an easier way to do that? *)
Lemma lt2 : forall a b, less_than a b -> less_than a (S b).
Proof.
  intros a b. revert a. induction b; intros.
  inv H.
  inv H.
  apply ltO.
  apply ltS. now apply IHb.
Qed.

现在,如果你真的希望保留你的特定定义,那么你可以尝试以下方法:

Lemma inv_lt: forall a b, less_than (S a) (S b) -> less_than a b.
Proof.
  induction b; intros.
  inv H. inv H2.
  inv H. apply lt2. now apply IHb.
Qed.