The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi,

> On 20 févr. 2015, at 19:09, George Van Treeck 
> <treeck AT yahoo.com>
>  wrote:
> 
> Given a definition and lemma like:
> 
> Definition cyclic_successor (m setsize: nat) : nat :=
>   if beq_nat m setsize then 1 else S m.
> 
> Lemma cyclic_successor_induction1 : forall m setsize: nat,
>   1 <= m < setsize -> cyclic_successor m setsize = S m.
> 
> Clearly « beq_nat m setsize" always fails where "m < setsize".

There should be in the library theorem linking the boolean equality test  
beq_nat : nat -> nat -> bool with the equality predicate  =.
After doing a case analysis over the condition, the proof should be purely 
arithmetic.




> So, the proof should be trivial. But, when I attempt to use induction it 
> creates new goals with larger successors because the definition is not 
> inductive with a decreasing term. Which rewrite tactics that can be used 
> here to equate the two conditions?
> 
> -George
>