1

帰納述語についての簡単な証明に行き詰まっています。自然の 0 が正ではないことを証明する必要があります。ここで、自然はビットのリストであり、0 は 0 のビットのみを含む任意のリストです。

H1: pos Empt
____________ (1/1)
Nat

依存型を使用した認定プログラミングのこの章では、を使用することをお勧めしているようですinversionが、エラー メッセージが表示されます。

Require Import Coq.Program.Program.

Inductive Bit: Type :=
  | Zer: Bit
  | One: Bit.

Inductive List (type1: Type): Type :=
  | Empt: List type1
  | Fill: type1 -> List type1 -> List type1.

Implicit Arguments Empt [[type1]].

Implicit Arguments Fill [[type1]].

Definition Nat: Type := List Bit.

Inductive pos: Nat -> Prop :=
  | pos_1: forall nat1: Nat, pos (Fill One nat1)
  | pos_2: forall nat1: Nat, pos nat1 -> forall bit1: Bit, pos (Fill bit1 nat1).

Program Fixpoint pred (nat1: Nat) (H1: pos nat1): Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat2 => Fill One (pred nat2 H1)
  | Fill One nat2 => Fill Zer nat2
  end.

Next Obligation.
inversion H1.
4

1 に答える 1

1

あなたTheorem T1は と同等ではありませんObligation。Nat後者では、それ自体がの要素を構築することになっていますType(ところで、なぜSetここで使用しないのですか? この開発では高次の型を操作していないようです)。

inversionエラーメッセージが示すように、 for thatの要素に対してケース分析 ( is built on that ) を実行することはできません(特にCoq マニュアルPropのセクション 4.5.4 を参照してください)。ただし、この場合、実際の を構築することに興味はありません。このケースが不可能であることを証明したいだけです。そのためには、（または、ではなくを使用することを選択した場合）ことができますが、証明する必要があります。であるため、 を使用できます。Natapply False_rectFalse_recSetTypeFalseFalsePropinversion H1

の定義の 2 番目のブランチに問題があることに注意してpredください。最も簡単な方法はおそらくここにも穴を残すことです:(pred nat2 H1)H1pos nat2(pred nat2 _)inversionpos nat2Prop

于 2012-11-27T15:13:33.563 に答える