diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-30 14:40:25 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-30 14:40:25 +0000 |
| commit | 0b52b95c747f220576468f4e12ab4156499a649f (patch) | |
| tree | eff0164d0c3224dad06ac56483cb2046684a1428 /theories/Reals/DiscrR.v | |
| parent | d74d12df2b673b9de5858ee15c10cd2f0f09061d (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2252 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/DiscrR.v')
| -rw-r--r-- | theories/Reals/DiscrR.v | 48 |
1 files changed, 29 insertions, 19 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index c955c57ef..9005b6089 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -12,28 +12,38 @@ Require Rbase. Recursive Tactic Definition Isrealint trm:= Match trm With - | [``0``] -> Idtac - | [``1``] -> Idtac - | [``?1+?2``] -> (Isrealint ?1);(Isrealint ?2) - | [``?1-?2``] -> (Isrealint ?1);(Isrealint ?2) - | [``?1*?2``] -> (Isrealint ?1);(Isrealint ?2) - | [``-?1``] -> (Isrealint ?1) + | [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. -Recursive Tactic Definition Sup0 := + +Tactic Definition Sup0 := Match Context With - | [ |- ``1>0`` ] -> Unfold Rgt;Apply Rlt_R0_R1 - | [ |- ``1+?1>0`` ] -> - Apply (Rgt_trans ``1+?1`` ?1 ``0``); - [Pattern 1 ``1+?1``;Rewrite Rplus_sym;Unfold Rgt; - Apply Rlt_r_r_plus_R1|Sup0]. + | [ |- (Rgt R1 R0) ] -> Unfold Rgt;Apply Rlt_R0_R1 + | [ |- (Rgt (Rplus R1 ?1) R0) ] -> + Apply (Rgt_trans (Rplus R1 ?1) ?1 R0); + [Pattern 1 (Rplus R1 ?1);Rewrite Rplus_sym;Unfold Rgt; + Apply Rlt_r_r_plus_R1 + |Sup0]. Tactic Definition DiscrR := - Try Match Context With - | [ |- ~(?1==?2) ] -> - Isrealint ?1;Isrealint ?2; - Apply Rminus_not_eq; Ring ``?1-?2``; + Match Context With + | [ |- ~R1==R0 ] -> Red;Intro;Apply R1_neq_R0;Assumption + | [ |- ~((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 ] -> (Isrealint ?1);Rewrite Rminus_Ropp; DiscrR + | [ |- ~(?1==?2) ] -> ((Isrealint ?1);(Isrealint ?2); + Apply Rminus_not_eq; Ring (Rminus ?1 ?2); (Match Context With - | [ |- ``-1+?<>0`` ] -> - Repeat Rewrite <- Ropp_distr1;Apply Ropp_neq - | _ -> Idtac);Apply Rgt_not_eq;Sup0. + | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> + Repeat Rewrite <-Ropp_distr1; DiscrR + | [ |- ? ] -> DiscrR) + Orelse (Apply Rminus_not_eq_right; DiscrR)). + + + |