diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-16 17:13:43 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-16 17:13:43 +0000 |
| commit | d1f49a3d69a300620b016bd7f3857111f3b51567 (patch) | |
| tree | 22da3a7a88266b2867b6f8d05254dc35fa3128ec /theories/Reals/DiscrR.v | |
| parent | 896264fe823e4367fea48bd98e4228a366753bc4 (diff) | |
Ajout de RCompute
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3514 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/DiscrR.v')
| -rw-r--r-- | theories/Reals/DiscrR.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index f7e3e0b1f..2d8d0476a 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -69,4 +69,10 @@ Recursive Tactic Definition Sup := | [ |- (Rlt (Ropp ?1) (Ropp ?2)) ] -> Apply Rlt_Ropp; Sup | [ |- (Rlt (Ropp ?1) ?2) ] -> Apply Rlt_trans with ``0``; Sup | [ |- (Rlt ?1 ?2) ] -> SupOmega - | _ -> Idtac.
\ No newline at end of file + | _ -> Idtac. + +Lemma IZR_eq : (z1,z2:Z) z1=z2 -> (IZR z1)==(IZR z2). +Intros; Rewrite H; Reflexivity. +Qed. + +Tactic Definition RCompute := Replace R1 with (IZR `1`); [Replace R0 with (IZR `0`); [Repeat Rewrite <- plus_IZR Orelse Rewrite <- mult_IZR Orelse Rewrite <- Ropp_Ropp_IZR Orelse Rewrite Z_R_minus; Apply IZR_eq; Ring | Reflexivity] | Reflexivity]. |