proposition: Lemma sound_by_invariance: forall (P: reach_input -> Prop) (Q: list V -> Prop) i, P i -> invariant P -> sound1 P Q -> sound2 P Q -> Q (construct_reachable i).
proof: Proof. intros. remember (lengthInput i). assert (lengthInput i <= n) by lia; clear Heqn. revert i H H3; induction n; intros; remember (construct_reachable i) as r; destruct i as [[len pr] rslt]; simpl in *; rewrite construct_reachable_unfold in Heqr; destruct pr; simpl in Heqr. + subst. apply H1 in H; auto. + destruct (le_dec len (length rslt)). - subst; apply H2 in H; auto. - exfalso; lia. + subst. apply H1 in H; auto. + destruct (le_dec len (length rslt)). - subst; apply H2 in H; auto. - subst. apply IHn; [apply H0; auto |]. simpl. lia. Qed.
imports: Coq.Sets.Finite_sets Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles Coq.Lists.List VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph