Set Implicit Arguments.
Require Export Arith.
From Coq Require Import Lia.

Require Import Coq.Classes.SetoidTactics.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Classes.Morphisms.

#[local] Open Scope signature_scope.

Lemma beq_nat_neq: ∀ x y : nat, x <> y → false = Nat.eqb x y.

Lemma if_beq_nat_nat_eq_dec : ∀ A (x y:nat) (a b:A),
  (if Nat.eqb x y then a else b) = if eq_nat_dec x y then a else b.

Definition ifte A (test:bool) (thn els:A) := if test then thn else els.

Add Parametric Morphism (A:Type) : (@ifte A)
  with signature (eq ⇒eq ⇒ eq ⇒ eq) as ifte_morphism1.

Add Parametric Morphism (A:Type) x : (@ifte A x)
  with signature (eq ⇒ eq ⇒ eq) as ifte_morphism2.

Add Parametric Morphism (A:Type) x y : (@ifte A x y)
  with signature (eq ⇒ eq) as ifte_morphism3.

Fixpoint compn (A:Type)(f:A → A → A) (x:A) (u:nat → A) (n:nat) {struct n}: A :=
   match n with O ⇒ x | (S p) ⇒ f (u p) (compn f x u p) end.

Lemma comp0 : ∀ (A:Type) (f:A → A → A) (x:A) (u:nat → A), compn f x u 0 = x.

Lemma compS : ∀ (A:Type) (f:A → A → A) (x:A) (u:nat → A) (n:nat),
              compn f x u (S n) = f (u n) (compn f x u n).

Lemma if_then : ∀ (P:Prop) (b:{ P }+{ ¬ P })(A:Type)(p q:A),
      P → (if b then p else q) = p.

Lemma if_else : ∀ (P :Prop) (b:{ P }+{ ¬ P })(A:Type)(p q:A),
      ¬P → (if b then p else q) = q.

Lemma if_then_not : ∀ (P Q:Prop) (b:{ P }+{ Q })(A:Type)(p q:A),
      ¬ Q → (if b then p else q) = p.

Lemma if_else_not : ∀ (P Q:Prop) (b:{ P }+{ Q })(A:Type)(p q:A),
      ¬P → (if b then p else q) = q.

Definition class (A:Prop) := ¬ ¬ A → A.

Lemma class_neg : ∀ A:Prop, class ( ¬ A).

Lemma class_false : class False.
#[export] Hint Resolve class_neg class_false : core.

Definition orc (A B:Prop) := ∀ C:Prop, class C → (A → C) → (B → C) → C.

Lemma orc_left : ∀ A B:Prop, A → orc A B.

Lemma orc_right : ∀ A B:Prop, B → orc A B.

#[export] Hint Resolve orc_left orc_right : core.

Lemma class_orc : ∀ A B, class (orc A B).

Arguments class_orc [A B].

Lemma orc_intro : ∀ A B, ( ¬ A → ¬ B → False) → orc A B.

Lemma class_and : ∀ A B, class A → class B → class (A ∧ B).

Lemma excluded_middle : ∀ A, orc A ( ¬ A).

Definition exc (A :Type)(P:A → Prop) :=
   ∀ C:Prop, class C → (∀ x:A, P x → C) → C.

Lemma exc_intro : ∀ (A :Type)(P:A → Prop) (x:A), P x → exc P.

Lemma class_exc : ∀ (A :Type)(P:A → Prop), class (exc P).

Lemma exc_intro_class : ∀ (A:Type) (P:A → Prop), ((∀ x, ¬ P x) → False) → exc P.

Lemma not_and_elim_left : ∀ A B, ¬ (A ∧ B) → A → ¬B.

Lemma not_and_elim_right : ∀ A B, ¬ (A ∧ B) → B → ¬A.

#[export] Hint Resolve class_orc class_and class_exc excluded_middle : core.

Lemma class_double_neg : ∀ P Q: Prop, class Q → (P → Q) → ¬ ¬ P → Q.

Definition feq A B (f g : A → B) := ∀ x, f x = g x.

Lemma feq_refl : ∀ A B (f:A→B), feq f f.

Lemma feq_sym : ∀ A B (f g : A → B), feq f g → feq g f.

Lemma feq_trans : ∀ A B (f g h: A → B), feq f g → feq g h → feq f h.

#[export] Hint Resolve feq_refl : core.
#[export] Hint Immediate feq_sym : core.
#[export] Hint Unfold feq : core.

Add Parametric Relation (A B : Type) : (A → B) (feq (A:=A) (B:=B))
  reflexivity proved by (feq_refl (A:=A) (B:=B))
  symmetry proved by (feq_sym (A:=A) (B:=B))
  transitivity proved by (feq_trans (A:=A) (B:=B))
as feq_rel.

Lemma CompSpec_rect : ∀ (A : Type) (eq lt : A → A → Prop) (x y : A)
       (P : comparison → Type),
       (eq x y → P Eq) →
       (lt x y → P Lt) →
       (lt y x → P Gt)
    → ∀ c : comparison, CompSpec eq lt x y c → P c.

Lemma dec_sig_lt : ∀ P : nat → Prop, (∀ x, {P x}+{ ¬ P x})
  → ∀ n, {i | i < n ∧ P i}+{∀ i, i < n → ¬ P i}.

Lemma dec_exists_lt : ∀ P : nat → Prop, (∀ x, {P x}+{ ¬ P x})
  → ∀ n, {exists i, i < n ∧ P i}+{¬ exists i, i < n ∧ P i}.

Definition eq_nat2_dec : ∀ p q : nat*nat, { p=q }+{¬ p=q }.
Defined.

Lemma nat_compare_specT
   : ∀ x y : nat, CompareSpecT (x = y) (x < y)%nat (y < x)%nat (Nat.compare x y).

Require Export NArith.

Lemma N2Nat_lt_mono : ∀ n m, (n < m)%N ↔ (N.to_nat n < N.to_nat m)%nat.

Lemma N2Nat_le_mono : ∀ n m, (n <= m)%N ↔ (N.to_nat n <= N.to_nat m)%nat.

Lemma N2Nat_inj_lt : ∀ n m, (n < m)%N → (N.to_nat n < N.to_nat m)%nat.

Lemma N2Nat_inj_le : ∀ n m, (n <= m)%N → (N.to_nat n <= N.to_nat m)%nat.

Lemma N2Nat_inj_pos : ∀ n, (0 < n)%N → (0 < N.to_nat n)%nat.
#[export] Hint Resolve N2Nat_inj_lt N2Nat_inj_pos N2Nat_inj_le : core.

Lemma Nsucc_pred_pos: ∀ n : N, (0 < n)%N → N.succ (N.pred n) = n.
#[export] Hint Resolve Nsucc_pred_pos : core.

Lemma Npos : ∀ n, (0 <= n)%N.
#[export] Hint Resolve Npos : core.

Lemma Neq_lt_0 : ∀ n, (n=0)%N ∨ (0<n)%N.
#[export] Hint Resolve Neq_lt_0 : core.

Lemma Nlt0_le1 : ∀ n, (0<n)%N → (1<=n)%N.
#[export] Hint Immediate Nlt0_le1 : core.

Ltac Nineq :=
     match goal with
      |- (N.le ?n ?m) ⇒ compute; discriminate
    | |- (N.lt ?n ?m) ⇒ compute; reflexivity
    | |- ¬ (eq (A:=N) ?n ?m) ⇒ rewrite <- N.compare_eq_iff; compute; discriminate
    end.