Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to make the tactic ring use my ring structure?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make the tactic ring use my ring structure?


chronological Thread 
  • From: "Lucian M. Patcas" <lucian.patcas AT gmail.com>
  • To: Laurent Théry <Laurent.Thery AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to make the tactic ring use my ring structure?
  • Date: Mon, 27 Jun 2011 16:34:37 -0400
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:reply-to:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=E3kdqpZiDfWF141vbGQPx2RE+9eSUF5Bup9IAfaZqIVZn3ghyo759ibLJvx0WcnuDQ bJ1h+oI99YgXqnrAbP8zuppGiFLnXukrpMDYFgTnoayi/jY4D9tEH3qTu0rSue5GThMa +Kw+YwrI/O+idttp02+jm0wDrUUh3QHd9J9I4=
Thank you, Laurent. I see, know. I got the Add Ring part right, but I didn't know now to start proving that lemma (split was the answer).

Many thanks to the others for their help.

Best,
Lucian

2011/6/27 Laurent Théry <Laurent.Thery AT inria.fr>

Hi,

your example is ok, you've just forgot to prove your lemma my_r_th:


(*****************************************************)

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


Add Ring my_r : my_r_th.


(* This works! *)
Goal forall x, my_r_plus x origin = x.
intros.
ring.

(*****************************************************)


Now to prove my_r_th starts with


(*****************************************************)


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

(*****************************************************)

and you see what you have to prove.




Archive powered by MhonArc 2.6.16.

Top of Page