coq - 用 Coq 证明实数和定理

Question

我只是用 Coq 证明定理的初学者，我坚持这个目标：

1 subgoal
______________________________________(1/1)  
~ ((1 <= 2 - 0)%R /\ (5 <= 2 + 1 + ( 0 - 1))%R)

任何人都可以为我做这件事吗？

Answer 1

你应该包含一些关于你迄今为止尝试过的信息，或者如果你知道使用什么策略，你将如何证明它。

这里有一些想法。我敢打赌，其中大部分已经被证明了。使用SearchAbout和SearchPattern命令查找证明的名称。这没有保修。

Require Import Coq.Reals.Reals.

Conjecture C01 : forall p1, True /\ p1 <-> p1.
Conjecture C02 : forall r1 r2 r3, (r1 + (r2 + r3))%R = (r1 + r2 + r3)%R.
Conjecture C03 : forall r1 r2, (r1 + - r2)%R = (r1 - r2)%R.
Conjecture C04 : forall r1, (0 - r1)%R = (- r1)%R.
Conjecture C05 : forall r1, (r1 - 0)%R = r1.
Conjecture C06 : forall r1 r2, (r1 + r2 - r2)%R = r1%R.
Conjecture C07 : forall r1, (1 * r1)%R = r1.
Conjecture C08 : forall r1 r2 r3, ((r1 + r2) * r3)%R = (r1 * r3 + r2 * r3)%R.
Conjecture C09 : forall r1, (r1 <= r1 + 1)%R <-> True.
Conjecture C10 : forall r1 r2, ~ (r1 <= r2)%R <-> (r2 < r1)%R.
Conjecture C11 : forall r1 r2 r3, (r1 + r3 < r2 + r3)%R <-> (r1 < r2)%R.
Hint Rewrite C01 C02 C03 C04 C05 C06 C07 C08 C09 C10 C11 : Hints.

Conjecture C12 : forall r1, (r1 < r1 + 1)%R.
Conjecture C13 : forall r1 r2, (r1 < r2)%R -> (r1 < r2 + 1)%R.
Hint Resolve C12 C13 : Hints.

Goal ~ ((1 <= 2 - 0)%R /\ (5 <= 2 + 1 + ( 0 - 1))%R).
Proof. autorewrite with Hints. eauto with Hints. Qed.

Answer 2

有一个使用傅立叶的简单解决方案：

Require Import Coq.Reals.Reals.
Open Local Scope R_scope.
Require Import Fourier.

Lemma ident: ~ ((1 <= 2 - 0) /\ (5 <= 2 + 1 + ( 0 - 1))).
Proof.
  unfold not.
  intro. destruct H.
  fourier.
Qed.

Answer 3

经过多次尝试，我的解决方案是：

Ltac prove_it:=
 match goal with
| [ H : context[(_ <= _)%R] |- False] => (apply Rgt_not_le in H; [|omega_sup]; assumption) || clear H
end.

Proof.
intuition; repeat prove_it.
Qed.

PS：我正在将我的证明推广到这种形式的任何目标：

~ (( _ <= _)%R /\ ( _ <= _)%R /\ (_ <= _)%R /\ ( _ <= _)%R /\ .... * n times )