The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hi all,

I need to define a ring structure and convince  the ring tactic to use it. I looked in the manual and in the module Ring_theory. I also looked at how nat is "registered" as a ring in Coq.setoid_ring.ArithRing, but I still don't know how exactly to define a ring structure and how to use Add Ring. Perhaps I'm missing something. Can someone help out?

Coq.setoid_ring.ArithRing

Require  Import Mult.


Require Import BinNat.


Require Import Nnat.
Require Export Ring.



Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).



Lemma nat_morph_N :
   semi_morph 0 1 plus mult (eq (A:=nat))


          0%N 1%N Nplus Nmult Neq_bool nat_of_N.



Ltac natcst t :=
  match isnatcst t with
    true => constr:(N_of_nat t)


  | _ => constr:InitialRing.NotConstant


  end.

Ltac Ss_to_add f acc :=
  match f with
  | S ?f1 => Ss_to_add f1 (S acc)


  | _ => constr:(acc + f)%nat


  end.

Ltac natprering :=
  match goal with
    |- context C [S ?p] =>


    match p with
      O => fail 1 
    | p => match isnatcst p with


           | true => fail 1
           | false => let v := Ss_to_add p (S 0) in


                         fold v; natprering
           end
    end
  | _ => idtac
  end.

Add Ring natr : natSRth


  (morphism nat_morph_N, constants [natcst], preprocess [natprering]).

Thanks,
Lucian