diff options
| author |  mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-18 10:14:57 +0000 |
|---|---|---|
| committer | mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-18 10:14:57 +0000 |
| commit | 8a2e6b944ecf4ea688ef4b8d8fac8ef76feabd3b (patch) | |
| tree | 9153b67fcfa615f2943d0fe995b0cf294c968a5c /theories/Reals/DiscrR.v | |
| parent | 2a880279eaf97f0b2bc5dd76220c5516df78b774 (diff) | |
modif test const
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1977 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/DiscrR.v')
| -rw-r--r-- | theories/Reals/DiscrR.v | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 8fe437561..9005b6089 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -10,6 +10,17 @@ Require Rbase. +Recursive Tactic Definition Isrealint trm:= + Match trm With + | [R0] -> Idtac + | [R1] -> Idtac + | [(Rplus ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2) + | [(Rminus ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2) + | [(Rmult ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2) + | [(Ropp ?1)] -> (Isrealint ?1) + | _ -> Fail. + + Tactic Definition Sup0 := Match Context With | [ |- (Rgt R1 R0) ] -> Unfold Rgt;Apply Rlt_R0_R1 @@ -22,12 +33,12 @@ Tactic Definition Sup0 := Tactic Definition DiscrR := Match Context With | [ |- ~R1==R0 ] -> Red;Intro;Apply R1_neq_R0;Assumption - | [ |- ~((Rplus R1 ?1)==R0) ] -> Apply Rgt_not_eq;Sup0 - | [ |- ~(Ropp ?1)==R0 ] -> Apply Ropp_neq; DiscrR + | [ |- ~((Rplus R1 ?1)==R0) ] -> (Isrealint ?1);Apply Rgt_not_eq;Sup0 + | [ |- ~(Ropp ?1)==R0 ] -> (Isrealint ?1);Apply Ropp_neq; DiscrR | [ |- ~(?1==?1) ] -> ElimType False - | [ |- ~(Rminus R0 ?1)==R0 ] -> Rewrite Rminus_Ropp; DiscrR - | [ |- ~(?1==?2) ] -> - (Apply Rminus_not_eq; Ring (Rminus ?1 ?2); + | [ |- ~(Rminus R0 ?1)==R0 ] -> (Isrealint ?1);Rewrite Rminus_Ropp; DiscrR + | [ |- ~(?1==?2) ] -> ((Isrealint ?1);(Isrealint ?2); + Apply Rminus_not_eq; Ring (Rminus ?1 ?2); (Match Context With | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> Repeat Rewrite <-Ropp_distr1; DiscrR |