proposition: Theorem decidable_PER_fp_quotient l R : (forall x, R x x <-> exists y, In y l /\ R x y) -> per R -> dec R -> fp_quotient R.
proof: Proof. revert R. induction on l as IHl with measure (length l); intros R Hl (H1 & H2) H3. destruct l as [ | x l ]. + exists 0 (fun _ => None) (@pos_O_invert _). * intros p; invert pos p. * intros x; rewrite Hl; split; auto. intros _ (? & [] & _). * intros x y; split. - intros H4. assert (R x x) as C. { apply H2 with y; auto. } apply Hl in C. destruct C as (? & [] & _). - intros (_ & []); auto. + destruct list_discrim with (P := R x) (Q := fun y => ~ R x y) (l := l) as (lx & m & G1 & G2 & G3). 1: { intro; apply H3. } rewrite Forall_forall in G2, G3. set (T u v := ~ R x u /\ R u v). destruct (IHl m) with (R := T) as [ n cl rp Q1 Q2 Q3 ]. * apply Permutation_length in G1; rewrite app_length in G1. simpl; lia. * intros u; unfold T; split. - rewrite Hl. intros (F1 & w & [ -> | F2 ] & F3). ++ apply H1 in F3; tauto. ++ exists w; split; auto. apply Permutation_in with (1 := G1), in_app_or in F2. destruct F2; auto. apply G2 in H. contradict F1. apply H2 with w; auto. - intros (v & F1 & F2 & F3); split; auto. apply H2 with v; auto. * split. - intros u v (F1 & F2); split; auto. contradict F1; apply H2 with v; auto. - intros a b c (F1 & F2) (F3 & F4); split; auto. apply H2 with b; auto. * intros u v; unfold T. destruct (H3 x u); destruct (H3 u v); tauto. * destruct (H3 x x) as [ Hx | Hx ]. - set (cl' y := match H3 x y with | left Hy => Some (pos0) | right Hy => match cl y with | Some p => Some (pos_nxt p) | None => None end end). set (rp' p := match pos_S_inv p with | inl _ => x | inr (exist _ q _) => rp q end). exists _ cl' rp'. ++ intros p; invert pos p; unfold cl', rp'; simpl. ** destruct (H3 x x) as [ | [] ]; auto. ** rewrite Q1. destruct (H3 x (rp p)) as [ | H ]; auto. unfold T in Q2. specialize (Q1 p). contradict Q1. rewrite (proj1 (Q2 _)); try tauto; discriminate. ++ intros u; unfold cl'; split. ** intros H; destruct (H3 x u) as [ F1 | F1 ]. { contradict H; apply H2 with x; auto. } rewrite (proj1 (Q2 _)); auto. intros (? & ?); tauto. ** destruct (H3 x u) as [ F1 | F1 ]; try discriminate. intros F2 F3. destruct (proj1 (Q3 u u)) as (E & ?). red; auto. destruct (cl u); try discriminate; tauto. ++ intros u v; split. ** intros H. unfold cl'. destruct (H3 x u) as [ F1 | F1 ]. { split; try discriminate. destruct (H3 x v) as [ F2 | F2 ]; auto. contradict F2; apply H2 with u; auto. } destruct (H3 x v) as [ F2 | F2 ]. { contradict F1; apply H2 with v; auto. } destruct (proj1 (Q3 u v)) as (F3 & F4). { red; auto. } rewrite <- F3. destruct (cl u); auto. split; auto; discriminate. ** intros (F1 & F2); revert F1 F2. unfold cl'. { destruct (H3 x u) as [ F1 | F1 ]; destruct (H3 x v) as [ F2 | F2 ]. + intros _ _; apply H2 with x; auto. + destruct (cl v); discriminate. + destruct (cl u); discriminate. + case_eq (cl u). 2: intros _ _ []; auto. case_eq (cl v); try discriminate. intros p Hp q Hq E _; apply Q3. rewrite Hp, Hq; split; try discriminate. f_equal. apply Some_inj, pos_nxt_inj in E; subst; auto. } - exists _ cl rp; auto. ++ intros u; split. ** intros H; apply Q2; unfold T; tauto. ** intros H; apply Q2 in H; contradict H; split; auto. contradict Hx; apply H2 with u; auto. ++ intros u v; split. ** intros H; apply Q3. split; auto. contradict Hx; apply H2 with u; auto. ** intros H; apply Q3 in H; destruct H; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(utils_list utils_decidable fin_base) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(measure_ind)