An attempt at a version of List.In which has UIP

In_UIP_attempt.v

Require Import Coq.Logic.EqdepFacts Coq.Logic.Eqdep_dec.
Require Import Coq.Lists.List.

Fixpoint In {A} (adjust : forall x y : A, x <> y -> x <> y) (a : A) (xs : list A) : Prop
  := match xs with
     | nil => False
     | x :: xs
       => x = a \/ ((exists pf : x <> a, adjust _ _ pf = pf) /\ In adjust a xs)
     end.

Lemma In_ext_impl {A} adjust1 adjust2 (adjust2_fix : forall x y (pf : x <> y), adjust1 _ _ pf = pf -> exists pf', adjust2 x y pf' = pf')
      {a xs} : @In A adjust1 a xs -> @In A adjust2 a xs.
Proof.
  induction xs as [|x xs IHxs]; cbn in *; [ easy | ].
  intros [H|[[pf H1] H2]]; eauto.
Qed.

Lemma In_ext_iff {A} adjust1 adjust2 (adjust_fix : forall x y, (exists pf, adjust1 x y pf = pf) <-> (exists pf, adjust2 x y pf = pf))
      {a xs} : @In A adjust1 a xs <-> @In A adjust2 a xs.
Proof.
  split; apply In_ext_impl; intros; apply adjust_fix; eauto.
Qed.

Import EqNotations.
(* N.B. This proof was fiendishly hard to construct, and it was
    non-trivial to settle on the type of [PI_adjust_strong], which
    effectively encodes that [adjust] is constant in a way that
    doesn't require funext *)
Lemma PI_adjust_UIP_strong {A adjust} {x y : A}
      (PI_adjust_strong : forall (pf : x <> y), (fun pf' => adjust x y pf = pf') = (fun pf' => adjust x y pf' = pf'))
      (p q : exists pf : x <> y, adjust _ _ pf = pf)
  : p = q.
Proof.
  cut (forall p' q' : { pf : _ | adjust x y pf = pf }, p' = q').
  { intro Hall.
    destruct p as [p Hp], q as [q Hq].
    specialize (Hall (exist _ p Hp) (exist _ q Hq)).
    clear -Hall.
    inversion_sigma; subst; cbn; reflexivity. }
  { pose proof q as q'; destruct q' as [ref Href].
    rewrite <- (PI_adjust_strong ref).
    clear; intros [? ?] [? ?].
    generalize dependent (adjust x y ref); intros; subst; reflexivity. }
Qed.

Lemma PI_In {A adjust}
      (PI_adjust_strong : forall x y (pf : x <> y), (fun pf' => adjust x y pf = pf') = (fun pf' => adjust x y pf' = pf'))
      (A_UIP : forall x y (p q : x = y :> A), p = q)
      {a xs} (p q : @In A adjust a xs)
  : p = q.
Proof.
  induction xs as [|x xs IHxs]; cbn in *; [ exfalso; assumption | ].
  destruct p as [p|[[p1 p2] p3]], q as [q|[[q1 q2] q3]]; try apply f_equal; try apply A_UIP; try apply f_equal2;
    try solve [ (idtac + exfalso); eauto ].
  apply PI_adjust_UIP_strong; auto.
Qed.

Definition adjust_of_dec {A} (dec : forall x y : A, x = y \/ x <> y) {x y : A} (pf : x <> y) : x <> y
  := match dec x y with
     | or_introl Heq => match pf Heq with end
     | or_intror Hneq => Hneq
     end.

Lemma adjust_of_dec_idempotent {A dec x y pf} : @adjust_of_dec A dec x y (@adjust_of_dec A dec x y pf) = @adjust_of_dec A dec x y pf.
Proof.
  cbv [adjust_of_dec]; edestruct dec; [ edestruct pf | reflexivity ].
Qed.

Lemma adjust_of_dec_good {A dec x y} : x <> y -> exists pf, @adjust_of_dec A dec x y pf = pf.
Proof.
  intro pf; unshelve (eexists; eapply adjust_of_dec_idempotent); eassumption.
Qed.

Lemma PI_adjust_of_dec_strong {A dec}
      x y (pf : x <> y)
  : (fun pf' => @adjust_of_dec A dec x y pf = pf') = (fun pf' => @adjust_of_dec A dec x y pf' = pf').
Proof.
  cbv [adjust_of_dec]; edestruct dec; [ exfalso; eauto | reflexivity ].
Qed.

Lemma PI_In_dec {A dec}
      (A_UIP : forall x y (p q : x = y :> A), p = q)
      {a xs} (p q : @In A (@adjust_of_dec A dec) a xs)
  : p = q.
Proof. apply PI_In; try assumption; apply PI_adjust_of_dec_strong. Qed.

Lemma In_dec_of_any {A dec adjust a xs} : @In A adjust a xs -> @In A (@adjust_of_dec A dec) a xs.
Proof. apply In_ext_impl; intros; apply adjust_of_dec_good; assumption. Qed.

Lemma In_dec_to_any {A dec adjust} (adjust_fix : forall x y (pf : x <> y), exists pf', adjust x y pf' = pf') {a xs}
  : @In A (@adjust_of_dec A dec) a xs -> @In A adjust a xs.
Proof. apply In_ext_impl; intros; apply adjust_fix; assumption. Qed.

Set Allow StrictProp.
Inductive SFalse : SProp := .
Definition adjust_of_sprop {A} {x y : A} (pf : x <> y) : x <> y
  := fun e : x = y => SFalse_ind (fun _ => False) (match pf e return SFalse with end).
Definition adjust_of_sprop_idempotent {A x y pf} : @adjust_of_sprop A x y (@adjust_of_sprop A x y pf) = @adjust_of_sprop A x y pf.
Proof. cbv [adjust_of_sprop]; reflexivity. Defined.
Lemma adjust_of_sprop_good {A x y} : x <> y -> exists pf, @adjust_of_sprop A x y pf = pf.
Proof.
  intro pf; unshelve (eexists; eapply adjust_of_sprop_idempotent); eassumption.
Qed.

Lemma PI_adjust_of_sprop_strong {A}
      x y (pf : x <> y)
  : (fun pf' => @adjust_of_sprop A x y pf = pf') = (fun pf' => @adjust_of_sprop A x y pf' = pf').
Proof. cbv [adjust_of_sprop]; reflexivity. Qed.

Lemma PI_In_sprop {A}
      (A_UIP : forall x y (p q : x = y :> A), p = q)
      {a xs} (p q : @In A (@adjust_of_sprop A) a xs)
  : p = q.
Proof. apply PI_In; try assumption; apply PI_adjust_of_sprop_strong. Qed.

Lemma In_sprop_of_any {A adjust a xs} : @In A adjust a xs -> @In A (@adjust_of_sprop A) a xs.
Proof. apply In_ext_impl; intros; apply adjust_of_sprop_good; assumption. Qed.

Lemma In_sprop_to_any {A adjust} (adjust_fix : forall x y (pf : x <> y), exists pf', adjust x y pf' = pf') {a xs}
  : @In A (@adjust_of_sprop A) a xs -> @In A adjust a xs.
Proof. apply In_ext_impl; intros; apply adjust_fix; assumption. Qed.