3

私は何度もこの問題に直面してきました: Coq には、同じ等式の両側の一致を含む証明状態があります。

複数の一致を 1 つに書き換える標準的な方法はありますか?

例えば。

match expression_evaling_to_Z with
    Zarith.Z0 => something
    Zartih.Pos _ => something_else
    Zarith.Neg _ => something_else
end = yet_another_thing.

で破壊するexpresion_evaling_to_Zと、同じゴールが 2 つ得られます。目標の1つだけを取得する方法を見つけたいと思います。

4

3 に答える 3

3

標準的な解決策は、破壊されたときに適切な条件とケースを導入する型ファミリを使用して、データ型の「ビュー」を定義することです。特定のケースでは、次のことができます。

Require Import Coq.ZArith.ZArith.

Inductive zero_view_spec : Z -> Type :=
| Z_zero  :                      zero_view_spec Z0
| Z_zeroN : forall z, z <> Z0 -> zero_view_spec z.

Lemma zero_viewP z : zero_view_spec z.
Proof. now destruct z; [constructor|constructor 2|constructor 2]. Qed.

Lemma U z : match z with
              Z0              => 0
            | Zpos _ | Zneg _ => 1
            end = 0.
Proof.
destruct (zero_viewP z).
Abort.

zこれは、型ファミリの引数をインスタンス化するための特別なサポートを提供する math-comp などの一部のライブラリで一般的なイディオムです。

于 2016-05-29T23:26:43.377 に答える
0

入力を気にしない場合はreplace、 RHS を目標の LHS に置き換えるために使用できます。これにより、問題を簡単に解決できます。その後、書き換えが実際に問題ないことを証明する必要があります。

Open Scope Z.
Lemma L a b :
  match a + b with
      Z0     => a + b
    | Zpos _ => b + a
    | Zneg _ => b + a
  end = a + b.
  replace (b+a) with (a+b). (* 1. replace the RHS with something trivially true *)
  destruct (a+b); auto.     (* 2. solve the branches in one fell swoop *)
  apply Z.add_comm.         (* 3. solve only once what is required for the two brances *)
Qed.

おそらく、いくつかの Ltac-fu やその他のレンマを使用して、RHS を手動で入力する必要がないようにすることもできます。

于 2016-05-30T08:20:34.573 に答える