1 files changed, 0 insertions, 114 deletions
diff --git a/src/versions/standard/Int63/Ring63_standard.v b/src/versions/standard/Int63/Ring63_standard.v
deleted file mode 100644
index 7b9fc1f..0000000
--- a/src/versions/standard/Int63/Ring63_standard.v
+++ /dev/null
@@ -1,114 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \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 Int63Lib Cyclic63 CyclicAxioms.
-
-Local Open Scope int63_scope.
-
-(** Detection of constants *)
-
-Local Open Scope list_scope.
-
-Ltac isInt63cst_lst l :=
- match l with
- | nil => constr:true
- | ?t::?l => match t with
-               | D1 => isInt63cst_lst l
-               | D0 => isInt63cst_lst l
-               | _ => constr:false
-             end
- | _ => constr:false
- end.
-
-Ltac isInt63cst t :=
- match t with
- | I63 ?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
-       ?i31 ?i32 ?i33 ?i34 ?i35 ?i36 ?i37 ?i38 ?i39 ?i40
-       ?i41 ?i42 ?i43 ?i44 ?i45 ?i46 ?i47 ?i48 ?i49 ?i50
-       ?i51 ?i52 ?i53 ?i54 ?i55 ?i56 ?i57 ?i58 ?i59 ?i60
-       ?i61 ?i62 =>
-    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
-      ::i31::i32::i33::i34::i35::i36::i37::i38::i39::i40
-      ::i41::i42::i43::i44::i45::i46::i47::i48::i49::i50
-      ::i51::i52::i53::i54::i55::i56::i57::i58::i59::i60
-      ::i61::i62::nil)
-    in isInt63cst_lst l
- | Int63Lib.On => constr:true
- | Int63Lib.In => constr:true
- | Int63Lib.Tn => constr:true
- | Int63Lib.Twon => constr:true
- | _ => constr:false
- end.
-
-Ltac Int63cst t :=
- match isInt63cst t with
- | true => constr:t
- | false => constr:NotConstant
- end.
-
-(** The generic ring structure inferred from the Cyclic structure *)
-
-Module Int63ring := CyclicRing Int63Cyclic.
-
-(** Unlike in the generic [CyclicRing], we can use Leibniz here. *)
-
-Lemma Int63_canonic : forall x y, phi x = phi y -> x = y.
-Proof.
- intros x y EQ.
- now rewrite <- (phi_inv_phi x), <- (phi_inv_phi y), EQ.
-Qed.
-
-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'.
-Proof.
-intros A R R' zero one add mul sub opp Impl Ring.
-constructor; intros; apply Impl; apply Ring.
-Qed.
-
-Lemma Int63Ring : ring_theory 0 1 add63 mul63 sub63 opp63 Logic.eq.
-Proof.
-exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int63_canonic Int63ring.CyclicRing).
-Qed.
-
-Lemma eqb63_eq : forall x y, eqb63 x y = true <-> x=y.
-Proof.
-unfold eqb63. intros x y.
-rewrite Cyclic63.spec_compare. case Z.compare_spec.
-intuition. apply Int63_canonic; auto.
-intuition; subst; auto with zarith; try discriminate.
-intuition; subst; auto with zarith; try discriminate.
-Qed.
-
-Lemma eqb63_correct : forall x y, eqb63 x y = true -> x=y.
-Proof. now apply eqb63_eq. Qed.
-
-Add Ring Int63Ring : Int63Ring
- (decidable eqb63_correct,
-  constants [Int63cst]).
-
-Section TestRing.
-Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x.
-intros. ring.
-Qed.
-
-Let test2 : forall x, (x - 1) + 1 = x.
-intros. ring.
-Qed.
-End TestRing.
-