Move interference definitions out of ideal/iw_instantiation.v

This is another followup of !244 (closed) after discussions with @kbedarka and @sbozhko

Depends on !262 (merged)
Depends on !270 (merged)

changed title from Remove useless lemma another_hep_job_interference_negP to Move interference definitions out of ideal/iw_instantiation.v

approved this merge request

marked this merge request as draft

added 41 commits

• 63a57f05 - ssreflect
• a37077c0 - more-ssreflect-changes
• ab66b9c0 - elf-def-changes
• c4b46201 - Merge branch 'meenal-project' of...
• 63a391e0 - elf-proofs
• 1e5c3379 - ELF-transitive-proof_withrelatedhypothesis
• f8dd25d5 - elf-proofs
• c1ef64a6 - elf-proofs-improved
• 9db47451 - elf-total-proofs
• 73efc035 - elf-proofs-pierresuggestions
• f2e9c228 - elf-proofs-completed
• 5b5a0cd6 - Apply 1 suggestion(s) to 1 file(s)
• e70c042c - Apply 1 suggestion(s) to 1 file(s)
• 2a546d61 - Apply 1 suggestion(s) to 1 file(s)
• d9212c31 - Apply 1 suggestion(s) to 1 file(s)
• 9a6e61c4 - Apply 1 suggestion(s) to 1 file(s)
• db6ea4f2 - Apply 1 suggestion(s) to 1 file(s)
• c65f6244 - Apply 1 suggestion(s) to 1 file(s)
• dab3dc64 - Apply 1 suggestion(s) to 1 file(s)
• b3576826 - Apply 1 suggestion(s) to 1 file(s)
• b5a9c684 - Apply 1 suggestion(s) to 1 file(s)
• 6d7d47cd - Apply 1 suggestion(s) to 1 file(s)
• ce32be9c - Apply 1 suggestion(s) to 1 file(s)
• 914a3870 - Apply 1 suggestion(s) to 1 file(s)
• 8449a848 - Apply 1 suggestion(s) to 1 file(s)
• 409fb870 - elf-def-without-comments
• 5ecda246 - elf-comments-added
• 453e9405 - elf-proofs-refined
• ff17b5c6 - Apply 1 suggestion(s) to 1 file(s)
• f404d04a - Apply 1 suggestion(s) to 1 file(s)
• f9ed8a74 - elf-indent
• b605fdf2 - elf-proof-comm
• 27bb2280 - ELF-Proofs-with-commits
• fe9d9cf5 - fix implicit arguments in model/priority/classes.v
• cceb24e2 - Remove useless lemma another_hep_job_interference_negP
• c521f5d8 - Factorize proofs of two lemmas
• 55bd443c - fix indentation
• f7a7f455 - Cleanout whitespaces
• ba20831a - Move interference definitions out of ideal/iw_instantiation.v
• b84f4b79 - Add basic hp_task properties
• ecbfb33e - Prove some fact about interference

Compare with previous version

unapproved this merge request

Quick question: what's the status of this MR?

I apparently need to rebase it and I guess It could be ready.

Will do in the coming days but don't wait for it to merge anything else.

added 14 commits

• ecbfb33e...19ed2a4e - 12 commits from branch RT-PROOFS:master
• 413da2ce - Move interference definitions out of ideal/iw_instantiation.v
• bd0d3107 - Prove some fact about interference

Compare with previous version

added 5 commits

• 048c19f3 - Definitions of hp_task and its properties
• 78b36707 - Definition of ELF
• 57602910 - Moving interference definitions out of iw_instantiation
• 4c0a6140 - Use _dec definitions directly
• b428b294 - Prove a splitting fact about interference

Compare with previous version

changed the description

Rebased but this depends on !270 (merged), I'll rebase once it is merged.

I also need to add a few comments and there remains a few definitions in iw_instantiations that should probably also be moved to proper definition files.

added 2 commits

• 4fe8b9cd - Use _dec definitions directly
• a9ea8e05 - Prove a splitting fact about interference

Compare with previous version

added 5 commits

• f64dba9a - Moving interference definitions out of iw_instantiation
• f0918b1c - Use _dec definitions directly
• 0dbebf41 - Prove a splitting fact about interference
• 8ff6eb2d - Fix indentation
• 310b5eb8 - Add missing lemma not_hep_hp_task

Compare with previous version

resolved all threads

Thanks for the update. !270 (merged) is now in. Happy to merge this one once you deem it ready.

added 6 commits

• 310b5eb8...35c1cb27 - 2 commits from branch RT-PROOFS:master
• b314531e - Moving interference definitions out of iw_instantiation
• 5547cc2f - Use _dec definitions directly
• e22b6aab - Prove a splitting fact about interference
• d7bcbcc7 - Add missing lemma not_hep_hp_task

Compare with previous version

marked this merge request as ready

Rebased and CI green, I consider this ready.

Thank you, very nice. I just have minor suggestions. Sorry to be nitpicking about model, but I believe we need to make an effort to keep it at least lean-ish.

added 2 commits

• ee0b00e3 - Prove a splitting fact about interference
• 2fe9dcb9 - Add missing lemma not_hep_hp_task

Compare with previous version

resolved all threads

resolved all threads

resolved all threads

Thanks for the review, all your comments should be addressed now.

enabled an automatic merge when the pipeline for 2fe9dcb9 succeeds

merged