proposition: Lemma gsc_iff: forall (g: LGraph) h, length (g_gen (glabel g)) <= length (spaces h) -> Forall (generation_space_compatible g) (combine (combine (nat_inc_list (length (g_gen (glabel g)))) (g_gen (glabel g))) (spaces h)) <-> forall gen, graph_has_gen g gen -> generation_space_compatible g (gen, nth_gen g gen, nth_space h gen).
proof: Proof. intros. rewrite Forall_forall. remember (g_gen (glabel g)). remember (nat_inc_list (length l)). remember (spaces h). assert (length (combine l0 l) = length l) by (subst; rewrite combine_length, nat_inc_list_length, Nat.min_id; reflexivity). assert (length (combine (combine l0 l) l1) = length l) by (rewrite combine_length, H0, min_l by assumption; reflexivity). cut (forall x, In x (combine (combine l0 l) l1) <-> exists gen, graph_has_gen g gen /\ x = (gen, nth_gen g gen, nth_space h gen)). - intros. split; intros. + apply H3. rewrite H2. exists gen. subst l1; intuition auto. + rewrite H2 in H4. destruct H4 as [gen [? ?]]. subst l1 x. apply H3. assumption. - intros. assert (forall gen, graph_has_gen g gen -> nth gen (combine (combine l0 l) l1) (0, null_info, null_space) = (gen, nth_gen g gen, nth_space h gen)). { intros. red in H2. rewrite <- Heql in H2. rewrite combine_nth_lt; [|rewrite H0; lia | lia]. rewrite combine_nth by (subst l0; rewrite nat_inc_list_length; reflexivity). rewrite Heql0. rewrite nat_inc_list_nth by assumption. rewrite Heql. unfold nth_gen, nth_space. rewrite Heql1. reflexivity. } split; intros. + apply (In_nth (combine (combine l0 l) l1) x (O, null_info, null_space)) in H3. destruct H3 as [gen [? ?]]. exists gen. rewrite H1 in H3. assert (graph_has_gen g gen) by (subst l; assumption). split. 1: assumption. rewrite H2 in H4 by assumption. subst x. reflexivity. + destruct H3 as [gen [? ?]]. rewrite <- H2 in H4 by assumption. subst x. apply nth_In. rewrite H1. subst l. assumption. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen