summaryrefslogtreecommitdiff
path: root/test-suite/success/MatchFail.v
blob: c2d87a4476880217ecb3cc896d38b4e9e954dc6d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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. *)
Ltac compute_POS :=
  match goal with
  |  |- context [(Zpos (xI ?X1))] =>
      let v := constr:X1 in
      match constr:v with
      | 1%positive => fail 1
      | _ =>  rewrite (BinInt.Pos2Z.inj_xI v)
      end
  |  |- context [(Zpos (xO ?X1))] =>
      let v := constr:X1 in
      match constr:v with
      | 1%positive => fail 1
      | _ =>  rewrite (BinInt.Pos2Z.inj_xO v)
      end
  end.

Goal forall x : positive, Zpos (xI (xI x)) = (4 * Zpos x + 3)%Z.
intros.
repeat compute_POS.
 ring.
Qed.