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.
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Int63 numbers defines Z/(2^63)Z, and can hence be equipped

with a ring structure and a ring tactic 
Require Import Cyclic63 CyclicAxioms.

Local Open Scope int63_scope.
Detection of constants 
Ltac isInt63cst t :=
  match eval lazy delta [add] in (t + 1)%int63 with
  | add _ _ => constr:(false)
  | _ => constr:(true)
  end.

Ltac Int63cst t :=
  match eval lazy delta [add] in (t + 1)%int63 with
  | add _ _ => constr:(NotConstant)
  | _ => constr:(t)
  end.
The generic ring structure inferred from the Cyclic structure 
Module Int63ring := CyclicRing Int63Cyclic.
Unlike in the generic CyclicRing, we can use Leibniz here. 
forall x y : int, φ (x) = φ (y) -> x = y

Proof to_Z_inj.


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 add mul sub opp eq


ring_theory 0 1 add mul sub opp eq

exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int63_canonic Int63ring.CyclicRing).
Qed.


forall x y : int, (x == y) = true -> x = y


forall x y : int, (x == y) = true -> x = y
 now apply eqb_spec. Qed.

Add Ring Int63Ring : Int63Ring
 (decidable eq31_correct,
  constants [Int63cst]).

Section TestRing.

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


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