aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/setoid_ring/Ring_equiv.v
blob: 945f6c684e512576c61f2b3a9585e1689c1f83d0 (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
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.