The Coq mailing list

[George Van Treeck <treeck AT yahoo.com>]

Unfortunately, case analysis does not work because both variables are uninstantiated and the cyclic_successor definition is not inductive. Using the destruct/reflexivity tactics for case analysis requires an infinite number of proof steps (generates the same subgoals as the induction/reflexivity tactics).

But, your suggestion of there being link of beq_nat to eq gave me an idea of equating less than to not beq_nat, which eliminates the need for case analysis. In case someone else might find it useful:

Lemma lt_beq_false : forall m n: nat,

  m < n -> beq_nat m n = false.

Proof.

  intros.

  apply beq_nat_false_iff.

  auto with *.

Qed.

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,

  m < setsize -> cyclic_successor m setsize = S m.

Proof.

  intros.

  unfold cyclic_successor.

  apply lt_beq_false in H.

  rewrite -> H.

  trivial.

Qed.

Thank you for the suggestion.

-George

On Friday, February 20, 2015 11:36 AM, Frédéric Besson <frederic.besson AT inria.fr> wrote:

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
>