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
|
Require Export NumPrelude.
Module Type DomainSignature.
Parameter Inline N : Set.
Parameter Inline E : relation N.
Parameter Inline e : N -> N -> bool.
(* Theoretically, we it is enough to have decidable equality e only.
If necessary, E could be defined using a coercion. However, after we
prove properties of natural numbers, we would like them to eventually
use ordinary Leibniz equality. E.g., we would like the commutativity
theorem, instantiated to nat, to say forall x y : nat, x + y = y + x,
and not forall x y : nat, eq_true (e (x + y) (y + x))
In fact, if we wanted to have decidable equality e only, we would have
some trouble doing rewriting. If there is a hypothesis H : e x y, this
means more precisely that H : eq_true (e x y). Such hypothesis is not
recognized as equality by setoid rewrite because it does not have the
form R x y where R is an identifier. *)
Axiom E_equiv_e : forall x y : N, E x y <-> e x y.
Axiom E_equiv : equiv N E.
Add Relation N E
reflexivity proved by (proj1 E_equiv)
symmetry proved by (proj2 (proj2 E_equiv))
transitivity proved by (proj1 (proj2 E_equiv))
as E_rel.
Delimit Scope NScope with Nat.
Bind Scope NScope with N.
Notation "x == y" := (E x y) (at level 70) : NScope.
Notation "x # y" := (~ E x y) (at level 70) : NScope.
End DomainSignature.
(* Now we give DomainSignature, but with E being Leibniz equality. If
an implementation uses this signature, then more facts may be proved
about it. *)
Module Type DomainEqSignature.
Parameter Inline N : Set.
Definition E := (@eq N).
Parameter Inline e : N -> N -> bool.
Axiom E_equiv_e : forall x y : N, E x y <-> e x y.
Definition E_equiv : equiv N E := eq_equiv N.
Add Relation N E
reflexivity proved by (proj1 E_equiv)
symmetry proved by (proj2 (proj2 E_equiv))
transitivity proved by (proj1 (proj2 E_equiv))
as E_rel.
Delimit Scope NScope with Nat.
Bind Scope NScope with N.
Notation "x == y" := (E x y) (at level 70) : NScope.
Notation "x # y" := ((E x y) -> False) (at level 70) : NScope.
(* Why do we need a new notation for Leibniz equality? See DepRec.v *)
End DomainEqSignature.
Module DomainProperties (Import DomainModule : DomainSignature).
(* It also accepts module of type NatDomainEq *)
Open Local Scope NScope.
(* The following easily follows from transitivity of e and E, but
we need to deal with the coercion *)
Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
Proof.
intros x x' Exx' y y' Eyy'.
case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
assert (x == y); [rewrite Exx'; now rewrite Eyy' |
rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
Qed.
End DomainProperties.
|
