Reals and theorem proving with Coq

Question

I am just a beginner in theorem proving with Coq and I am stuck in this goal:

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

Can anyone make this easy for me?

Answer 1

After many tries, my solution is:

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: I am making my proof generalized to any goal of this form :

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

Answer 2

You should have included some information about what you've tried so far or how you would prove it if you knew what tactics to use.

Here are some ideas. I bet most of these have already been proven. Use the SearchAbout and SearchPattern commands to find the name of the proofs. This comes without warranty.

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 3

There is a simple solution using fourier:

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.