diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/success/MatchFail.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/success/MatchFail.v')
-rw-r--r-- | test-suite/success/MatchFail.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v new file mode 100644 index 00000000..d89ee3be --- /dev/null +++ b/test-suite/success/MatchFail.v @@ -0,0 +1,28 @@ +Require Export ZArith. +Require Export ZArithRing. + +(* Cette tactique a pour objectif de remplacer toute instance + de (POS (xI e)) ou de (POS (xO e)) par + 2*(POS e)+1 ou 2*(POS e), pour rendre les expressions plus + à même d'être utilisées par Ring, lorsque ces expressions contiennent + des variables de type positive. *) +Tactic Definition compute_POS := + (Match Context With + | [|- [(POS (xI ?1))]] -> Let v = ?1 In + (Match v With + | [xH] -> + (Fail 1) + |_-> + Rewrite (POS_xI v)) + | [ |- [(POS (xO ?1))]] -> Let v = ?1 In + Match v With + |[xH]-> + (Fail 1) + |[?]-> + Rewrite (POS_xO v)). + +Goal (x:positive)(POS (xI (xI x)))=`4*(POS x)+3`. +Intros. +Repeat compute_POS. +Ring. +Qed. |