Imported Upstream version 8.0pl1upstream/8.0pl1

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.