(* This file is distributed under the terms of the MIT License, also
   known as the X11 Licence.  A copy of this license is in the README
   file that accompanied the original distribution of this file.

   Based on code written by:
     Brian Aydemir *)

Require Import Coq.Arith.Peano_dec.
Require Import Coq.Lists.SetoidList.
Require Import Lia.

Require Import Metalib.CoqUniquenessTac.

(* *********************************************************************** *)

Hint Resolve eq_nat_dec : eq_dec.

(* *********************************************************************** *)

Scheme le_ind' := Induction for le Sort Prop.

Lemma le_unique : ∀ (x y : nat) (p q: x ≤ y), p = q.
Proof.
  induction p using le_ind';
  uniqueness 1;
  assert False by lia; intuition.

Qed.

(* ********************************************************************** *)

Section Uniqueness_Of_SetoidList_Proofs.

  Variable A : Type.
  Variable R : A → A → Prop.

  Hypothesis R_unique : ∀ (x y : A) (p q : R x y), p = q.
  Hypothesis list_eq_dec : ∀ (xs ys : list A), {xs = ys} + {xs ≠ ys}.

  Scheme lelistA_ind' := Induction for lelistA Sort Prop.
  Scheme sort_ind' := Induction for sort Sort Prop.
  Scheme eqlistA_ind' := Induction for eqlistA Sort Prop.

  Theorem lelistA_unique :
    ∀ (x : A) (xs : list A) (p q : lelistA R x xs), p = q.
  Proof. induction p using lelistA_ind'; uniqueness 1. Qed.

  Theorem sort_unique :
    ∀ (xs : list A) (p q : sort R xs), p = q.
  Proof. induction p using sort_ind'; uniqueness 1. apply lelistA_unique. Qed.

  Theorem eqlistA_unique :
    ∀ (xs ys : list A) (p q : eqlistA R xs ys), p = q.
  Proof. induction p using eqlistA_ind'; uniqueness 2. Qed.

End Uniqueness_Of_SetoidList_Proofs.

(* *********************************************************************** *)

Inductive vector (A : Type) : nat → Type :=
  | vnil : vector A 0
  | vcons : ∀ (n : nat) (a : A), vector A n → vector A (S n).

Theorem vector_O_eq : ∀ (A : Type) (v : vector A 0),
  v = vnil _.
Proof. intros. uniqueness 1. Qed.