proposition: Lemma sound_wedge_to_cdata_inj: forall size (g: @EdgeListGG size), (forall x y : LE * EType, In x (graph_to_wedgelist g) -> In y (graph_to_wedgelist g) -> wedge_to_cdata x = wedge_to_cdata y -> x = y).
proof: Proof. intros. unfold graph_to_wedgelist in H, H0. apply list_in_map_inv in H. destruct H. apply list_in_map_inv in H0. destruct H0. destruct H. destruct H0. unfold edge_to_wedge in H. unfold edge_to_wedge in H0. subst x. subst y. apply EList_evalid in H2. apply EList_evalid in H3. assert (Hvvalid_x0: vvalid g (fst x0) /\ vvalid g (snd x0)). { rewrite <- (src_fst g), <- (dst_snd g) by auto. apply edge_valid; auto. } destruct Hvvalid_x0 as [Hx0_1 Hx0_2]. assert (Hvvalid_x1: vvalid g (fst x1) /\ vvalid g (snd x1)). { rewrite <- (src_fst g), <- (dst_snd g) by auto. apply edge_valid; auto. } destruct Hvvalid_x1 as [Hx1_1 Hx1_2]. unfold wedge_to_cdata in H1; simpl in H1. apply pair_equal_spec in H1. destruct H1. apply pair_equal_spec in H0. destruct H0. apply Vint_injective in H. apply Vint_injective in H0. apply Vint_injective in H1. apply repr_inj_signed in H. rewrite H. 2: unfold repable_signed; apply (weight_valid g); auto. 2: unfold repable_signed; apply (weight_valid g); auto. replace x0 with (fst x0, snd x0). 2: destruct x0; auto. replace x1 with (fst x1, snd x1). 2: destruct x1; auto. apply repr_inj_signed in H0. rewrite H0. apply repr_inj_signed in H1. rewrite H1. auto. all: unfold repable_signed. apply (@vertex_representable size) in Hx0_2. lia. apply (size_bound g). apply (@vertex_representable size) in Hx1_2. lia. apply (size_bound g). apply (@vertex_representable size) in Hx0_1. lia. apply (size_bound g). apply (@vertex_representable size) in Hx1_1. lia. apply (size_bound g). Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist