From stdpp Require Import numbers option sorting ssreflect.
From stdpp Require Import options.

Definition transportf {X} (P : X → Type) {x x' : X} : x = x' → P x → P x'.
Proof. by induction 1. Defined.

Instance HdRel_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} a l : ProofIrrel (HdRel R a l).
Proof.
  intros HR1 HR2.
  assert (Hnil : ∀ xs (Hxs : [] = xs) (HR : HdRel R a xs),
             HR = transportf _ Hxs (HdRel_nil R a)).
  { intros. destruct HR; last done.
    by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
  assert (Hcons : ∀ xs x y xs' (Hxs : y :: xs' = xs) (HR : HdRel R x xs) (Hxy : R x y),
             HR = transportf (HdRel R x) Hxs (HdRel_cons R x y xs' Hxy)).
  { intros. destruct HR; first done.
    injection Hxs as <- <-.
    replace Hxs with (eq_refl (y :: xs')); last apply eq_pi, list_eq_dec.
    simpl.
    by replace r with Hxy by apply H. }
  destruct l.
  - trans (transportf (HdRel R a) eq_refl (HdRel_nil R a)).
    + apply Hnil.
    + symmetry. apply Hnil.
  - apply HdRel_inv in HR1 as Haa0.
    trans (transportf (HdRel R a) eq_refl (HdRel_cons R a a0 l Haa0)).
    + apply Hcons.
    + symmetry. apply Hcons.
Qed.

Instance Sorted_pi {A} (R : relation A) `{!EqDecision A} `{!∀ x y, ProofIrrel (R x y)} l : ProofIrrel (Sorted R l).
Proof.
  intros HS1 HS2.
  assert (Hbase : ∀ xs (Hxs : [] = xs) (HS : Sorted R xs), HS = transportf _ Hxs (Sorted_nil R)).
  { intros. destruct HS; last done.
    by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
  assert (Hind : ∀ xs x xs'
                   (Hxs : x :: xs' = xs) (HS : Sorted R xs)
                   (Hx : HdRel R x xs') (HS' : Sorted R xs')
                   (IH : ∀ HS1' HS2' : Sorted R xs', HS1' = HS2'),
             HS = transportf _ Hxs (Sorted_cons HS' Hx)).
  { intros. destruct HS; first done.
    injection Hxs as <- <-.
    replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
    simpl.
    replace h with Hx by apply: HdRel_pi.
    by replace HS with HS' by apply IH. }
  induction l.
  - trans (transportf _ eq_refl (Sorted_nil R)).
    + apply Hbase.
    + symmetry. apply Hbase.
  - destruct (Sorted_inv HS1) as [Hl Hal].
    trans (transportf _ eq_refl (Sorted_cons Hl Hal)).
    + apply Hind, IHl.
    + symmetry. apply Hind, IHl.
Qed.

Instance Forall_pi {A} (P : A → Prop) (l : list A) `{!EqDecision A} `{!∀ a, ProofIrrel (P a)} : ProofIrrel (Forall P l).
Proof.
  intros HF1 HF2.
  assert (Hbase : ∀ xs (Hxs : [] = xs) (HF : Forall P xs), HF = transportf (Forall P) Hxs (ListDef.Forall_nil P)).
  { intros xs Hxs HF. destruct HF; last done.
    by replace Hxs with (eq_refl ([] : list A)); last apply eq_pi, list_eq_dec. }
  assert (Hind : ∀ xs x xs'
                   (Hxs : x :: xs' = xs) (HF : Forall P xs)
                   (Hx : P x) (HF' : Forall P xs')
                   (IH : ∀ HF1' HF2' : Forall P xs', HF1' = HF2'),
             HF = transportf _ Hxs (ListDef.Forall_cons P x xs' Hx HF')).
  { intros. destruct HF; first done.
    injection Hxs as <- <-.
    replace Hxs with (eq_refl (x :: xs')); last apply eq_pi, list_eq_dec.
    simpl.
    replace p with Hx by apply H.
    by replace HF with HF' by apply IH. }
  induction l.
  - trans (transportf _ eq_refl (ListDef.Forall_nil P)).
    + apply Hbase.
    + symmetry. apply Hbase.
  - apply Forall_inv in HF1 as Ha.
    apply Forall_inv_tail in HF1 as Hl.
    trans (transportf _ eq_refl (ListDef.Forall_cons P a l Ha Hl)).
    + apply Hind, IHl.
    + symmetry. apply Hind, IHl.
Qed.

Instance ex_pi {A} {B : A → Prop} `{!ProofIrrel A} `{!∀ x, ProofIrrel (B x)} :
  ProofIrrel (∃ (x : A), B x).
Proof.
  intros [x Hx] [y Hy].
  assert (y = x) by apply proof_irrel. subst.
  assert (Hx = Hy) by apply proof_irrel. by subst.
Qed.