Library MetaCoq.Template.utils.MCArith

From Coq Require Import Arith ZArith Lia.

Inductive BoolSpecSet (P Q : Prop) : bool → Set :=
    BoolSpecT : P → BoolSpecSet P Q true | BoolSpecF : Q → BoolSpecSet P Q false.

Lemma leb_spec_Set : ∀ x y : nat, BoolSpecSet (x ≤ y) (y < x) (x <=? y).
Proof.
  intros.
  destruct (Nat.leb_spec0 x y).
  now constructor.
  constructor. now lia.
Qed.

Lemma nat_rev_ind (max : nat) :
  ∀ (P : nat → Prop),
    (∀ n, n ≥ max → P n) →
    (∀ n, n < max → P (S n) → P n) →
    ∀ n, P n.
Proof.
  intros P hmax hS.
  assert (h : ∀ n, P (max - n)).
  { intros n. induction n.
    - apply hmax. lia.
    - destruct (Nat.leb_spec0 max n).
      + replace (max - S n) with 0 by lia.
        replace (max - n) with 0 in IHn by lia.
        assumption.
      + replace (max - n) with (S (max - S n)) in IHn by lia.
        apply hS.
        × lia.
        × assumption.
  }
  intro n.
  destruct (Nat.leb_spec0 max n).
  - apply hmax. lia.
  - replace n with (max - (max - n)) by lia. apply h.
Qed.

Lemma strong_nat_ind :
  ∀ (P : nat → Prop),
    (∀ n, (∀ m, m < n → P m) → P n) →
    ∀ n, P n.
Proof.
  intros P h n.
  assert (∀ m, m < n → P m).
  { induction n ; intros m hh.
    - lia.
    - destruct (Nat.eqb_spec n m).
      + subst. eapply h. assumption.
      + eapply IHn. lia.
  }
  eapply h. assumption.
Qed.

Lemma Z_of_pos_alt p : Z.of_nat (Pos.to_nat p) = Z.pos p.
Proof.
  induction p using Pos.peano_ind.
  rewrite Pos2Nat.inj_1. reflexivity.
  rewrite Pos2Nat.inj_succ. cbn. f_equal. lia.
Qed.