The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Basically, you have to prove your own induction principle, with one hypothesis for each case. You could also maybe encode it into an inductive. (Like the pos_view thing for positive numbers that you can find in the standard library).

For Z, the use of the lia tactic is convenient, here.

Require Import ZArith.
Require Import Psatz.

Section zind.
  Variable P : Z -> Prop.
  Hypothesis Hneg : forall z, Zlt z 0 -> P z.

  Hypothesis H_0_to_10 : forall (z : Z), Zle 0 z -> Zle z 10 -> P z.
  Hypothesis H_11 : P 11.
  Hypothesis H_gt_11 : forall z, Zlt 11 z -> P z.
  
  Lemma dicho : forall (z : Z), Zle 0 z -> (Zle z 10 \/ z = 11%Z \/ Zlt 11 z). 

    intros. lia.
  Qed.

  Lemma lia_helper :forall p,  (0 <= Zpos p)%Z. 
  Proof. 
    intros. unfold Zle; discriminate.   
  Qed.
  Hint Immediate lia_helper.
  Lemma Zind : forall z, P z.

  Proof.
    induction z. apply H_0_to_10; lia. 
    destruct (dicho _ (lia_helper p)) as [H |[H |H]].
    apply H_0_to_10; try lia; auto.
    rewrite H. assumption.
    apply H_gt_11. auto.
    apply Hneg. unfold Zlt. simpl. auto.

  Qed.
End zind.

Check Zind.

Lemma toto : forall (z : Z), Zle 0 (z * z).
Proof.
  induction z using Zind.
Abort

With best regards

thomas

On Wed, Sep 1, 2010 at 3:49 PM, Michael <michaelschausten AT googlemail.com> wrote:

Hello,

I'd like to prove a Lemma (x : Z) with [induction x]. This gives me three
cases: x==0, x == Zpos p and x == Zneg p (p : positive).
However, I would like to have more self-defined cases, e.g.: x = Zneg p, x ==
0, 1 <= x <= 10, x == 11 and x > 11. I tried it with bindings (induction term
with bindings_list), but only received error. How can I do create those
self-defined cases?

Sincerely,