Removing lemmas #79
Removing lemmas #79
Conversation
DafinaTrufas
force-pushed
the
removing-lemmas
branch
from
6e504bb to
49aa295
Compare
|
It's not final, I'm going to add more commits. Sorry, I wasn't aware of the possibility to mark a PR as draft. |
DafinaTrufas
force-pushed
the
removing-lemmas
branch
from
56ca37b to
d908110
Compare
|
I feel a little biased about removing some results about streams and stream filtering and also about topological sorting (maybe because I've been working on them). My feeling is that some are general purpose lemmas, which might not be used now, but could be eventually (e.g., about streams / stream filtering), while others help make the argument about the correctness of an algorithm (e.g., about topological sorting). On the other hand, we don't really know when we're going to need those and might not make sense to maintain them in the hope that they would sometime be useful. So I'm wondering whether it would make sense to tag the current master and remove them, keeping it mind that if we sometime need them, we can take a look at the tagged version. |
There was a problem hiding this comment.
@DafinaTrufas an important goal with removing lemmas is to remove code, that is, to make files smaller and more surveyable. Hence, you should remove lemmas and not comment them out.
However, that is not to say that all currently commented-out lemmas in this PR should actually be removed in the end. But please change the PR to use full removal, and we'll take it from there.
Ok. I'm changing it now. |
There was a problem hiding this comment.
You removed a lemma I recently added (elem_of_list_split_2), which will break casper-cbc-proofs. You should certainly add it back.
Regarding the other changes, I have mixed feelings. I think removing lemmas that refer to StrictlyComparable or other in-house stuff seems fine, but these extras that refer to EqDecision etc. seem pretty general and useful.
Maybe we should try to submit these lemmas to the standard library and stdpp before we remove them?
Also, I wonder: does the script consider usage cross-project? Removing elem_of_list_split_2 is clearly a false positive, as it is used in casper-cbc-proofs.
| (* TODO(palmskog): consider submitting a PR to Coq's stdlib. *) | ||
| Lemma set_diff_nodup' `{EqDecision A} (l l' : list A) | ||
| : NoDup l -> NoDup (set_diff l l'). | ||
| Proof. | ||
| induction 1 as [|x l H H' IH]; simpl. | ||
| - constructor. | ||
| - case_decide. | ||
| + by apply IH. | ||
| + by apply set_add_nodup, IH. | ||
| Qed. |
There was a problem hiding this comment.
Maybe if we're removing this one, @palmskog should really submit a PR to the stdlib?
And if you delete it, you should also delete the TODO.
| (** This lemma is needed in fault_weight_state_backwards **) | ||
| Lemma Rplusminus_assoc : forall r1 r2 r3, | ||
| (r1 + r2 - r3)%R = (r1 + (r2 - r3))%R. | ||
| Proof. | ||
| intros. unfold Rminus. | ||
| apply Rplus_assoc. | ||
| Qed. | ||
|
|
||
| (** This lemma is needed in fault_weight_state_sorted_subset **) |
There was a problem hiding this comment.
I do agree that removing these looks like a good idea, but what about the comment? @traiansf
theories/VLSM/Lib/SsrExport.v
Outdated
| @@ -4,4 +4,4 @@ From Coq Require Export ssreflect. | |||
| #[export] Set SsrOldRewriteGoalsOrder. | |||
| #[export] Set Asymmetric Patterns. | |||
| #[export] Set Bullet Behavior "None". | |||
| Definition iYC2 := True. | |||
There was a problem hiding this comment.
@palmskog What is this line doing?
There was a problem hiding this comment.
@wkolowski some of the tooling (coq-dpdgraph, I think) requires there to be a constant defined in each file. So we add this dummy constant.
|
There are still too many removals here that require more discussion. I think we should trim the PR to only the uncontroversial removals. I may be able to get to this next week. |
|
@palmskog It seems this PR has been stale for around 1.5 years and also I have removed plenty of duplicated/unnecessary lemmas over time, e.g. some of the stuff in |
No description provided.