The Coq mailing list

[Fr�d�ric Besson <frederic.besson AT inria.fr>]

Hello David,

Here is the way I would do it:
* Get rid of Rdiv and Rinv.
* Use (available) decision procedures to discharge the rest

Here is the whole script.

Require Import Reals.
Require Import Rbase.
Require Import Psatz.
(* 
- Coq 8.3 'psatzl R' decide linear arithmetic over R
- Coq 8.4 'lra' does the same
*)

Open Scope R_scope.

Ltac add_eq expr val := set (temp := expr) ; generalize (refl_equal temp) ; 
unfold temp at 1 ; generalize temp ; intro val ; clear temp.

Ltac elim_rinv :=
  match goal with 
      | H : context [Rinv ?X] |- _ => 
          revert H ; 
          let x := fresh in 
            add_eq X x ; generalize (Rinv_r x) ; generalize Rinv x ;
          intros
      | |- context [Rinv ?X] => 
          let x := fresh in 
            add_eq X x ; generalize (Rinv_r x) ; generalize Rinv x ;
          intros
  end.

Ltac simpl_R :=
  unfold Rdiv in * ; repeat elim_rinv. 


Goal forall b:R, 0 < b -> b <> 0.
Proof.
intros.
psatzl R.
Qed.


Theorem b_div_b_is_one : forall (b:R), (0%R <  b)%R -> (1%R = (Rdiv b b)%R).
intros.
simpl_R.
psatzl R.
Qed.

Theorem perm_div2 : forall (a:R) (b:R), ((0%R <  a)%R /\ (0%R <  b)%R) ->
 ((Rdiv (a * b)%R b)%R = ((Rdiv a b)%R * b)%R).
intros.
simpl_R ; psatzl R.
Qed.





On 5 avr. 2012, at 09:31, David MENTRE wrote:

> Hello,
> 
> I laboriously proved following two simple theorems on reals. I tried
> the [fourier] tactic without success. I thought it would help with
> following kind of sub-goal:
> 
>  b : R
>  H : 0 < b
>  ============================
>   b <> 0
> 
> 
> Would readers of this list have suggestions on more efficient way to
> do those proofs?
> 
> ===========
> Require Import Rbase.
> Require Import Fourier.
> 
> 
> Theorem b_div_b_is_one : forall (b:R), (0%R <  b)%R -> (1%R = (Rdiv b b)%R).
> intros.
> field.
> contradict H.
> rewrite H.
> apply Rlt_irrefl.
> Qed.
> 
> Theorem perm_div2 : forall (a:R) (b:R), ((0%R <  a)%R /\ (0%R <  b)%R) ->
>  ((Rdiv (a * b)%R b)%R = ((Rdiv a b)%R * b)%R).
> intros.
> field.
> elim H.
> intros.
> contradict H1.
> rewrite H1.
> apply Rlt_irrefl.
> Qed.
> =================
> 
> Sincerely yours,
> david