InductionWithSelfDefinedCases

Pierre Letouzey edited this page Oct 27, 2017 · 4 revisions

This Coq-club thread discusses how to do induction using self defined cases. For example, induction x with x : Z leads to three cases : x = 0, x < 0, x > 0. One can improve on this by proving one's own induction principle. (In this example, the use of the tactic lia is convenient.) The main idea is to prove a lemma, with one premises for each desired case.

Require Import ZArith.
Require Import Psatz.
Section zind.
  Variable P : Z -> Prop.
  (* Here, we want to split the induction into 4 cases : z < 0, 0 <=z<= 10, z = 11, 11 < z, so  *)
  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.
  (* here, we provide an helper lemma to split cases *)
  Lemma case_split : forall (z : Z), Zle 0 z -> (Zle z 10 \/ z = 11%Z \/ Zlt 11 z).
    intros. lia.
  Qed.
  (* This lemma is required to solve some cases for Lia *)
  Lemma lia_helper :forall p,  (0 <= Zpos p)%Z.
  Proof.
    intros. unfold Zle; discriminate.
  Qed.
  Hint Immediate lia_helper.
  (* The main lemma *)
  Lemma Zind : forall z, P z.
  Proof.
    induction z. apply H_0_to_10; lia.
    destruct (case_split _ (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.

One can now use the new induction principles in proofs.

induction z using Zind.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.