The Coq mailing list

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

On Mon, Jun 27, 2011 at 13:55, Stéphane Glondu <steph AT glondu.net> wrote:

Le 27/06/2011 19:47, Lucian M. Patcas a écrit :

> 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 inCoq.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?

Can you give an example of what you think should work, but doesn't?

I've tried to replicate what they did in the standard library in Coq.setoid_ring.ArithRing for nat, but I'm stuck proving the Lemma

Inductive my_r :=
| origin : my_r
| next : my_r -> my_r.

Fixpoint my_r_plus (n m : my_r) : my_r :=
  match n with
    | origin => m
    | next p => next (my_r_plus p m)
  end.

Fixpoint my_r_mult (n m : my_r) : my_r :=
  match n with
    | origin => origin
    | next p => my_r_plus m (my_r_mult p  m)
  end.

Check semi_ring_theory origin (next origin).

Lemma my_r_th : semi_ring_theory origin (next origin) my_r_plus my_r_mult (@eq my_r).

Add Ring my_r : my_r_th.

It's just me not knowing how to prove that Lemma or I am missing something and registering a ring doesn't work this way?

Thanks,
Lucian