diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-23 22:40:38 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-23 22:40:38 +0000 |
| commit | 69bf012d0d2a71ed19fc89b31073747f85f9a11d (patch) | |
| tree | 277a73b0eff5e138208150b3301daf786575a1fa /theories/Reals/DiscrR.v | |
| parent | 174efedc2ee4fce87d94f276a591c2cb9993b2b3 (diff) | |
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/DiscrR.v')
| -rw-r--r-- | theories/Reals/DiscrR.v | 48 |
1 files changed, 19 insertions, 29 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 9005b6089..c955c57ef 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -12,38 +12,28 @@ 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) + | [``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) | _ -> Fail. - -Tactic Definition Sup0 := +Recursive Tactic Definition Sup0 := Match Context With - | [ |- (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]. + | [ |- ``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]. Tactic Definition DiscrR := - 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); + Try Match Context With + | [ |- ~(?1==?2) ] -> + Isrealint ?1;Isrealint ?2; + Apply Rminus_not_eq; Ring ``?1-?2``; (Match Context With - | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> - Repeat Rewrite <-Ropp_distr1; DiscrR - | [ |- ? ] -> DiscrR) - Orelse (Apply Rminus_not_eq_right; DiscrR)). - - - + | [ |- ``-1+?<>0`` ] -> + Repeat Rewrite <- Ropp_distr1;Apply Ropp_neq + | _ -> Idtac);Apply Rgt_not_eq;Sup0. |