1

less_thanCoqに関するいくつかの定理を証明しようとしています。私はこの帰納的な定義を使用しています：

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ますか？）

ありがとう！

4

1 に答える 1

5

まず、 の定義はless_than、2 番目のコンストラクターが冗長であるという意味で少し残念です。より単純なものに切り替えることを検討する必要があります。

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.

2 番目の節は冗長でした(a, b)。の証明が必要なless_than a b場合は、いつでもlt3 a時間を適用してから適用できますlt1。実際lt2には、他の 2 つのコンストラクターの結果です。

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.
于 2013-03-18T02:15:57.647 に答える