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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
Require Import Ring.
Require Export NumPrelude.
Module Type NDomainSignature.
Parameter Inline N : Set.
Parameter Inline E : N -> N -> Prop.
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 NatScope with Nat.
Bind Scope NatScope with N.
Notation "x == y" := (E x y) (at level 70) : NatScope.
Notation "x # y" := (~ E x y) (at level 70) : NatScope.
End NDomainSignature.
(* Now we give NDomainSignature, but with E being Leibniz equality. If
an implementation uses this signature, then more facts may be proved
about it. *)
Module Type NDomainEqSignature.
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 NatScope with Nat.
Bind Scope NatScope with N.
Notation "x == y" := (E x y) (at level 70) : NatScope.
Notation "x # y" := ((E x y) -> False) (at level 70) : NatScope.
(* Why do we need a new notation for Leibniz equality? See DepRec.v *)
End NDomainEqSignature.
Module NDomainProperties (Import NDomainModule : NDomainSignature).
(* It also accepts module of type NatDomainEq *)
Open Local Scope NatScope.
Theorem Zneq_symm : forall n m, n # m -> m # n.
Proof.
intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
Qed.
(* 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.
Theorem NE_stepl : forall x y z : N, x == y -> x == z -> z == y.
Proof.
intros x y z H1 H2; now rewrite <- H1.
Qed.
Declare Left Step NE_stepl.
(* The right step lemma is just transitivity of E *)
Declare Right Step (proj1 (proj2 E_equiv)).
Ltac stepl_ring t := stepl t; [| ring].
Ltac stepr_ring t := stepr t; [| ring].
End NDomainProperties.
|
