1

2進数の自然数（ビットのリスト）の先行関数を定義しようとしています。関数の入力を、トリミングされた（先行ゼロがない）数値と正の数値（つまり、ゼロの前身について心配する必要がない）に制限したいと思います。

演算子の定義は次のpredとおりです。

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

私の最初の義務は次のとおりです。

nat1: Nat
H1: is_trim nat1 = True
H2: is_pos nat1 H1 = True
H3: Empt = nat1
______________________________________(1/1)
Nat

しかし、私はそれを解決する方法がわかりません。

矛盾は明らかににありH2ます。しかし、それはに依存するのでH1、私はただrewrite nat1でEmpt、そして次に(is_pos Empt H1)ですることはできませんFalse。

これをどのように証明すればよいですか？

4

1 に答える 1

2

この目標は、Emptの場合に任意の自然数を返すことができるという点で実際に些細なことであり、最初に適切なを渡す必要があるため、誰もその数に到達できないので安心してくださいH2 : is_pos nat1 H1。

このようなことを解決するための次の「正しい」方法は、次の行で依存パターンマッチングを使用することだと思います。

Program Fixpoint pred (nat1: Nat) (H1: is_trim nat1 = True) (H2: is_pos nat1 H1 = True): Nat :=
  match nat1 as nat1' return is_pos nat1' H1 -> Nat with
  | Empt => fun isposEmpt =>
      (* hopefully, is_pos Empt H1 immediately reduces to False, and you can do this: *)
      False_rec Nat isposEmpt
  | Fill Zer nat2 => fun _ => Fill One (pred nat2 H1 H2)
  | Fill One nat2 => fun _ => Fill Zer nat2
  end H2.

つまり、一致の引数としてnat1が正であるという証明が必要であり、Emptの場合、証明は偽物であると結論付けるので、偽物を返すこともできます。

うまくいけば、これはうまくいき、ある程度意味があります。次回、人々があなたの例で遊ぶのを助けるために必要な定義を提供してください。

于 2012-11-25T17:27:01.890 に答える