diff options
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. |