blob: a4ada571f13e94ad8feb9109ebea983172c41f39 (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Bool ZArith.
Require Import Zify ZifyClasses.
Require Import Lia.
Local Open Scope Z_scope.
(** [Z_of_comparison] is the injection function for comparison *)
Definition Z_of_comparison (c : comparison) : Z :=
match c with
| Lt => -1
| Eq => 0
| Gt => 1
end.
Lemma Z_of_comparison_bound : forall x, -1 <= Z_of_comparison x <= 1.
Proof.
destruct x ; simpl; compute; intuition congruence.
Qed.
Instance Inj_comparison_Z : InjTyp comparison Z :=
{ inj := Z_of_comparison ; pred :=(fun x => -1 <= x <= 1) ; cstr := Z_of_comparison_bound}.
Add Zify InjTyp Inj_comparison_Z.
Definition ZcompareZ (x y : Z) :=
Z_of_comparison (Z.compare x y).
Program Instance BinOp_Zcompare : BinOp Z.compare :=
{ TBOp := ZcompareZ }.
Add Zify BinOp BinOp_Zcompare.
Instance Op_eq_comparison : BinRel (@eq comparison) :=
{TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.
Add Zify BinRel Op_eq_comparison.
Instance Op_Eq : CstOp Eq :=
{ TCst := 0 ; TCstInj := eq_refl }.
Add Zify CstOp Op_Eq.
Instance Op_Lt : CstOp Lt :=
{ TCst := -1 ; TCstInj := eq_refl }.
Add Zify CstOp Op_Lt.
Instance Op_Gt : CstOp Gt :=
{ TCst := 1 ; TCstInj := eq_refl }.
Add Zify CstOp Op_Gt.
Lemma Zcompare_spec : forall x y,
(x = y -> ZcompareZ x y = 0)
/\
(x > y -> ZcompareZ x y = 1)
/\
(x < y -> ZcompareZ x y = -1).
Proof.
unfold ZcompareZ.
intros.
destruct (x ?= y) eqn:C; simpl.
- rewrite Z.compare_eq_iff in C.
lia.
- rewrite Z.compare_lt_iff in C.
lia.
- rewrite Z.compare_gt_iff in C.
lia.
Qed.
Instance ZcompareSpec : BinOpSpec ZcompareZ :=
{| BPred := fun x y r => (x = y -> r = 0)
/\
(x > y -> r = 1)
/\
(x < y -> r = -1)
; BSpec := Zcompare_spec|}.
Add Zify BinOpSpec ZcompareSpec.
|
