The Coq mailing list

[Razvan Voicu <razvan AT comp.nus.edu.sg>]

Dear all,

Thank you all for your replies, and sorry for my getting back to you so 
late. The reason I asked how "straightforward" the proofs appear to you 
is because my proofs are by "implicit induction" (a more precise name 
would probably be 'proofs by descente infinie'). I find such proofs less 
dependent on the existence of an adequate induction principle, and thus 
easier to produce in general (and maybe automate). So I was trying to 
understand the level of familiarity of such proofs in the community.

All the three answers that I received were looking at the proofs from a 
'formalizing mathematics' perspective. I wonder if any of you could 
comment from a 'proof automation' perspective.

Thanks again for taking the time to reply.

Razvan

Muad Dib wrote:
> Hi Razvan, I would just like to point out:
>
> Inductive multiple (d : nat) : nat -> Prop :=
> | mO : multiple d 0
> | mS n : multiple d n -> multiple d (d + n).
>
> Definition even := multiple 2.
> Definition m3 := multiple 3.
> Definition m6 := multiple 6.
>
> And that also forall d i, multiple d i <-> (exists k, i = k * d).
>
> I would consider these proofs part of arithmetic (and prove them
> arithmetically) rather than as inductive properties which happen to be
> indexed by numbers, but then again your proofs are shorter so either
> way is fine.
>