various cleanups and simplifications in util (!212) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Merged Björn Brandenburg requested to merge MathComp-PR-cleanups-and-simplifications into master 2 years ago

Apr 19, 2022
- reorganize `util.sum` and add some comments · 45391d62
  Björn Brandenburg authored 2 years ago
  
  45391d62
- Simplify proof of sum_of_ones · fb3e19b5
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  fb3e19b5
- Remove sum0 · 9e195050
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  It is exactly big1_eq
  9e195050
- Simplify proof of sum_majorant_eqn · e6205fed
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  e6205fed
- Remove sum_seq_cond_gt0P · fd7baf22
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  It was subsumed by sum_nat_gt0
  fd7baf22
- Simplify proof of sumnB_nat · a9431bf0
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  a9431bf0
- Simplify proof of leq_sum_seq_pred · d15b1e83
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  d15b1e83
- Simplify proof of {l,}eq_sum_seq · 1c1a8bf9
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  1c1a8bf9
- Simplify proof of leq_sum_sub_uniq · fb9eb1f3
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  fb9eb1f3
- Simplify proof of sum_pred_diff · 9a537fa3
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  9a537fa3
- Simplify proof of sum_majorant_constant · e1d58324
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  e1d58324
- Simplify proof of sum_notin_rem_eqn · 2d72fd86
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  2d72fd86
- Simplify sum_nat_gt0 · 594d4da6
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  594d4da6
- Generalize and simplify proof of sum_nat_eq0_nat · 4a9a0cfc
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  4a9a0cfc
- Rewrite 2 proofs in more ssreflect style · 162e01f4
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  162e01f4
- Remove add_mul_diff · 8ff12f1c
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  Too specific and one liner with existing MathComp lemmas.
  8ff12f1c
- Remove exists_or_not_add_mul_cases · 0e8d85e0
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  Subsumed by existing MathComp lemmas on division.
  0e8d85e0
- Prepare leq_subRL_impl for MathComp PR · 010ef216
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  010ef216
- Prepare subdnD for MathComp PR · bb76b8bd
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  bb76b8bd
Apr 14, 2022
- Remove leq_addk · b782b2d7
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  leq_trans and leq_addr seem to be enough.
  b782b2d7
- Remove subn_abba · eda66272
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago
  
  Too specific.
  eda66272

various cleanups and simplifications in util

Merge request reports

Activity