proposition: Lemma eformat_adj: forall (g: UAdjMatGG) u v, adjacent g u v <-> evalid g (eformat (u,v)).
proof: Proof. intros. split. intros. + destruct H. destruct H. destruct H. destruct H0; destruct H0. assert (x = (u,v)). { rewrite (edge_src_fst g) in H0. rewrite (edge_dst_snd g) in H2. rewrite <- H0, <- H2. destruct x; simpl; auto. } subst x. rewrite eformat1; auto. simpl. rewrite <- H0. rewrite <- H2 at 2. apply (undirected_edge_rep g); auto. assert (x = (v,u)). { rewrite (edge_src_fst g) in H0; rewrite (edge_dst_snd g) in H2. rewrite <- H0, <- H2. destruct x; simpl; auto. } subst x. rewrite eformat2. simpl. auto. simpl. rewrite <- H0. rewrite <- H2 at 2. apply (undirected_edge_rep g); auto. + intros. destruct (Z.lt_trichotomy u v). rewrite eformat1 in H. 2: simpl; lia. assert (evalid g (u,v)). auto. exists (u,v). split. apply (evalid_strong_evalid g); auto. left. rewrite (edge_src_fst g), (edge_dst_snd g); auto. destruct H0. rewrite eformat1 in H. 2: simpl; lia. assert (evalid g (u,v)). auto. exists (u,v). split. apply (evalid_strong_evalid g); auto. left. rewrite (edge_src_fst g), (edge_dst_snd g); auto. rewrite eformat2 in H. 2: simpl; lia. simpl in H. assert (evalid g (v,u)). auto. exists (v,u). split. apply (evalid_strong_evalid g); auto. rewrite (edge_src_fst g), (edge_dst_snd g); auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph