3

Coqで実数の簡単な証明をしようとしています。たとえば、2 つの非負数の平均も非負であることを証明したいと考えています。

Example test: forall r1 r2:R, r1 >= 0 -> r2 >= 0 -> (r1 + r2)/2 >= 0.

私の最初のステップは、次のように証明することr1 + r2 >=0です。

Require Export Coq.Reals.RIneq.
Require Export Coq.Reals.R_sqrt.

Local Open Scope Z_scope.
Local Open Scope R_scope.

Example test: forall r1 r2:R, r1 >= 0 -> r2 >= 0 -> (r1 + r2)/2 >= 0.
Proof. intros. 
  assert (r1 + r2 >= 0 + 0).
  apply Rplus_ge_compat; assumption. simpl in H1.

しかし、私は得ることができるだけです

...
H1 : r1 + r2 >= 0 + 0
______________________________________(1/1)
(r1 + r2) / 2 >= 0

仮説で。0 + 0H1 の RHS を に変更できません0。simpl in H1.示されているように試しましたが、何もしませんでした。実数が と違うのはわかりましたnat。しかし、ここで物事をどのように単純化すればよいでしょうか?

(注: 私は実数の初心者です。また、上記のコードはナイーブ/非効率的である可能性があります。改善のための提案は大歓迎です。) また:

Rplus_ge_compat
     : forall r1 r2 r3 r4 : R,
       r1 >= r2 ->
       r3 >= r4 -> r1 + r3 >= r2 + r4
4

1 に答える 1

3

Coq の標準ライブラリの実数は公理的であるため、計算しません。しかし、式を単純化するために、いくつかの定理で書き直すことができます。

rewrite Rplus_0_r in H1.

または、式を通常の形式に変換するために、さまざまな書き換え手順を適用する戦術に依存します。リング上の式を簡略化するには、 を使用できますring_simplify。

ring_simplify in H1.

リング操作に限定されず、分数もある場合は、field_simplify代わりに使用できます (この場合、探している通常の形式にはなりません)。

field_simplify in H1.

もう 1 つの可能性は、 を使用replace ... with ...して、何を置き換えたいか、何を置き換えたいかを正確に記述することです。2 つの式が等しいことを証明する方法をすぐに知っていれば、replace ... with ... by ...その制約をすぐに解除できます。

replace (0 + 0) with 0 in H1 by ring.
于 2015-12-20T19:49:34.230 に答える