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
|
Require Import Setoid_ring_theory.
Require Import LegacyRing_theory.
Require Import Ring_theory.
Set Implicit Arguments.
Section Old2New.
Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aopp : A -> A.
Variable Aeq : A -> A -> bool.
Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
Let Aminus := fun x y => Aplus x (Aopp y).
Lemma ring_equiv1 :
ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
Proof.
destruct R.
split; eauto.
Qed.
End Old2New.
Section New2OldRing.
Variable R : Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
Variable reqb : R -> R -> bool.
Variable reqb_ok : forall x y, reqb x y = true -> x = y.
Lemma ring_equiv2 :
Ring_Theory radd rmul rI rO ropp reqb.
Proof.
elim Rth; intros; constructor; eauto.
intros.
apply reqb_ok.
destruct (reqb x y); trivial; intros.
elim H.
Qed.
Definition default_eqb : R -> R -> bool := fun x y => false.
Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
Proof.
discriminate 1.
Qed.
End New2OldRing.
Section New2OldSemiRing.
Variable R : Type.
Variable (rO rI : R) (radd rmul: R->R->R).
Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
Variable reqb : R -> R -> bool.
Variable reqb_ok : forall x y, reqb x y = true -> x = y.
Lemma sring_equiv2 :
Semi_Ring_Theory radd rmul rI rO reqb.
Proof.
elim SRth; intros; constructor; eauto.
intros.
apply reqb_ok.
destruct (reqb x y); trivial; intros.
elim H.
Qed.
End New2OldSemiRing.
|
