Library Coq.Numbers.Cyclic.Int31.Ring31


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 Lia 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.

#[deprecated(note="Consider Numbers.Cyclic.Int63.Ring63 instead", since="8.10")]
Lemma Int31_canonic : forall x y, phi x = phi y -> x = y.

#[deprecated(note="Consider Numbers.Cyclic.Int63.Ring63 instead", since="8.10")]
Lemma ring_theory_switch_eq :
 forall A (R R':A->A->Prop) zero one add mul sub opp,
  (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'.

#[deprecated(note="Consider Numbers.Cyclic.Int63.Ring63 instead", since="8.10")]
Lemma Int31Ring : ring_theory 0 1 add31 mul31 sub31 opp31 Logic.eq.

#[deprecated(note="Consider Numbers.Cyclic.Int63.Ring63 instead", since="8.10")]
Lemma eqb31_eq : forall x y, eqb31 x y = true <-> x=y.

#[deprecated(note="Consider Numbers.Cyclic.Int63.Ring63 instead", since="8.10")]
Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y.

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

Section TestRing.
Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x.
Defined.
End TestRing.