Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)
This library has been deprecated since Coq version 8.10.

Int31 numbers defines Z/(2^31)Z, and can hence be equipped

with a ring structure and a ring tactic 
Require Import Int31 Cyclic31 CyclicAxioms.

Local Open Scope int31_scope.
Detection of constants 
Local Open Scope list_scope.

Ltac isInt31cst_lst l :=
 match l with
 | nil => constr:(true)
 | ?t::?l => match t with
               | D1 => isInt31cst_lst l
               | D0 => isInt31cst_lst l
               | _ => constr:(false)
             end
 | _ => constr:(false)
 end.

Ltac isInt31cst t :=
 match t with
 | I31 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10
       ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20
       ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30 =>
    let l :=
      constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10
      ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
      ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
    in isInt31cst_lst l
 | Int31.On => constr:(true)
 | Int31.In => constr:(true)
 | Int31.Tn => constr:(true)
 | Int31.Twon => constr:(true)
 | _ => constr:(false)
 end.

Ltac Int31cst t :=
 match isInt31cst t with
 | true => constr:(t)
 | false => constr:(NotConstant)
 end.
The generic ring structure inferred from the Cyclic structure 
Module Int31ring := CyclicRing Int31Cyclic.
Unlike in the generic CyclicRing, we can use Leibniz here. 
forall x y : int31, phi x = phi y -> x = y


forall x y : int31, phi x = phi y -> x = y

 
x, y:int31
EQ:phi x = phi y
x = y

 now rewrite <- (phi_inv_phi x), <- (phi_inv_phi y), EQ.
Qed.


forall (A : Type) (R R' : A -> A -> Prop)
  (zero one : A) (add mul sub : A -> A -> A)
  (opp : A -> A),
(forall x y : A, R x y -> R' x y) ->
ring_theory zero one add mul sub opp R ->
ring_theory zero one add mul sub opp R'


forall (A : Type) (R R' : A -> A -> Prop)
  (zero one : A) (add mul sub : A -> A -> A)
  (opp : A -> A),
(forall x y : A, R x y -> R' x y) ->
ring_theory zero one add mul sub opp R ->
ring_theory zero one add mul sub opp R'


A:Type
R, R':A -> A -> Prop
zero, one:A
add, mul, sub:A -> A -> A
opp:A -> A
Impl:forall x y : A, R x y -> R' x y
Ring:ring_theory zero one add mul sub opp R
ring_theory zero one add mul sub opp R'

constructor; intros; apply Impl; apply Ring.
Qed.


ring_theory 0 1 add31 mul31 sub31 opp31 eq


ring_theory 0 1 add31 mul31 sub31 opp31 eq

exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int31_canonic Int31ring.CyclicRing).
Qed.


forall x y : int31, eqb31 x y = true <-> x = y


forall x y : int31, eqb31 x y = true <-> x = y


forall x y : int31,
match x ?= y with
| Eq => true
| _ => false
end = true <-> x = y
 
x, y:int31
match x ?= y with
| Eq => true
| _ => false
end = true <-> x = y


x, y:int31
match (phi x ?= phi y)%Z with
| Eq => true
| _ => false
end = true <-> x = y
 
x, y:int31
phi x = phi y -> true = true <-> x = y
x, y:int31
(phi x < phi y)%Z -> false = true <-> x = y
x, y:int31
(phi y < phi x)%Z -> false = true <-> x = y


x, y:int31
H:phi x = phi y
H0:true = true
x = y
x, y:int31
(phi x < phi y)%Z -> false = true <-> x = y
x, y:int31
(phi y < phi x)%Z -> false = true <-> x = y
 
x, y:int31
(phi x < phi y)%Z -> false = true <-> x = y
x, y:int31
(phi y < phi x)%Z -> false = true <-> x = y


x, y:int31
(phi y < phi x)%Z -> false = true <-> x = y

intuition; subst; auto with zarith; try discriminate.
Qed.


forall x y : int31, eqb31 x y = true -> x = y


forall x y : int31, eqb31 x y = true -> x = y
 now apply eqb31_eq. Qed.

Add Ring Int31Ring : Int31Ring
 (decidable eqb31_correct,
  constants [Int31cst]).

Section TestRing.

forall x y : int31,
1 + x * y + x * x + 1 = 1 * 1 + 1 + y * x + 1 * x * x


x, y:int31
1 + x * y + x * x + 1 = 1 * 1 + 1 + y * x + 1 * x * x
 ring.
Qed.
End TestRing.