blob: d89ee3bec71aeeb069103d16e2b72c7be9f89787 (
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
|
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.
|
