proposition: Fact list_discrete_bij_nat X (l : list X) : (forall x y : X, { x = y } + { x <> y }) -> { n : nat & { f : X -> nat & { g : nat -> option X | (forall x, In x l -> f x < n) /\ (forall x, In x l -> g (f x) = Some x) /\ (forall p, p < n -> exists x, g p = Some x /\ f x = p) } } }.
proof: Proof. intros D. destruct (list_discrete_bij_pos l D) as (n & f & g & H1 & H2 & H3). exists n. exists (fun x => match in_dec D x l with | left H => pos2nat (f x H) | right _ => 0 end). exists (fun k => match le_lt_dec n k with | left _ => None | right H => Some (g (nat2pos H)) end). msplit 2. + intros x H; destruct (in_dec D x l); try tauto; apply pos2nat_prop. + intros x H; destruct (in_dec D x l) as [ Hx | Hx ]; try tauto. destruct (le_lt_dec n (pos2nat (f x Hx))) as [ H' | H' ]. * generalize (pos2nat_prop (f _ Hx)); lia. * f_equal; rewrite nat2pos_pos2nat; auto. + intros p Hp. exists (g (nat2pos Hp)); split. * destruct (le_lt_dec n p) as [ | ? ]; try (exfalso; lia). do 2 f_equal; apply pos2nat_inj. rewrite !pos2nat_nat2pos; auto. * destruct (in_dec D (g (nat2pos Hp)) l) as [ | [] ]; auto. rewrite H3, pos2nat_nat2pos; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)