JasonGross · March 26, 2021 20:50 · Mar 26, 2021 · Mar 26, 2021
diff --git a/In_UIP_attempt.v b/In_UIP_attempt.v
@@ -90,3 +90,32 @@ 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.
diff --git a/In_UIP_attempt.v b/In_UIP_attempt.v
@@ -0,0 +1,92 @@
+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.
No results found