Add NoDup_bind, vec_enum, vec_finite.
This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can vec_finite be used to simplify the proof of list_finite?
Merge request reports
Activity
4227 4227 Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 → 4228 4228 Forall2 P (l1 ≫= f) (l2 ≫= g). 4229 4229 Proof. induction 1; csimpl; auto using Forall2_app. Qed. 4230 Lemma NoDup_bind l : 4231 (∀ a a' b, b ∈ f a → b ∈ f a' → a = a') → 4232 (∀ a, NoDup (f a)) → NoDup l → NoDup (l ≫= f). 4233 Proof. 4234 intros inj Hf Hl; induction l; cbn; [constructor|inversion_clear Hl]. 4235 apply NoDup_app; repeat split; auto; intros b H1 H2. 4236 apply elem_of_list_bind in H2 as (a'&?&?). 4237 apply (inj a a') in H1; subst; done. -
ahere has never been explicitly named, so CI rejects this proof script. Please only refer to names that are introduced explicitly. We don't want the proof to fail in the future if Coq's automatic naming changes.Also please don't use
H1orH2; use descriptive names instead.Edited by Ralf Jung
I tweaked the proofs a bit, strengthened some statements, added a missing lemma for
cardonvec, implemented the suggestion to simplifylist_finite, and tweakedprod_finitebased on ideas in this MR.For the moment, you can see my changes here: https://gitlab.mpi-sws.org/iris/stdpp/-/commits/herman/vec_finite
@bergwerf Could you enable the setting that allows me to push to this MR? That makes it easier to incorporate my changes.
And forgot to say, @bergwerf: Thanks for the contribution to std++.
@robbertkrebbers I cannot check the allow contributions setting when the target branch is protected. Should I set another target branch?
-
FYI, it is generally better to not use the
master/mainbranch for MRs. Instead, create dedicated feature branches for that. That would also avoid the branch protection issues. (This applies both to GitLab and GitHub.)However I don't think you can change the branch of an already created MR. So either you need to change your repo config to remove
masterbranch protection, or you have to open a new MR.Edited by Ralf Jung mentioned in commit 425519d9
Closing in favor of !458 (merged)
mentioned in merge request !458 (merged)
mentioned in commit 20ad7f5a
mentioned in commit 919087b3
