Commits · bug-report-parametricity · BERTOT Yves / triangles · GitLab

Mentions légales du service

Snippets Groups Projects

GitLab upgrade completed. Current version is 17.11.4.

Oct 08, 2019
- this version is long but it shows the anomaly · 0df60c26
  BERTOT Yves authored 5 years ago
  
  0df60c26
- move eq_op as part of naive5 notation · b7590f15
  BERTOT Yves authored 5 years ago
  
  b7590f15
- Make the algorithm be parameterized by an equality function · 9d9ed68b
  BERTOT Yves authored 5 years ago
  9d9ed68b
- Remove a little more dead code · 21054a7c
  BERTOT Yves authored 5 years ago
  
  21054a7c
Oct 04, 2019
- Major simplification: all proofs in a realDomainType · 0a215776
  BERTOT Yves authored 5 years ago
  0a215776
- A much simpler proof of Knuth's 4th axiom thanks to tail_coefD_gt0 · eca60236
  BERTOT Yves authored 5 years ago
  
  eca60236
- marks two theorems as dead code. · 9486ee47
  BERTOT Yves authored 5 years ago
  9486ee47
- Knuth_2 works on arbitrary type now, and cannot so easily be used as a view · 64168b2c
  BERTOT Yves authored 5 years ago
  64168b2c
Oct 03, 2019
- adds to_ccw_system.v to _CoqProject · 7b3c4d26
  BERTOT Yves authored 5 years ago
  
  7b3c4d26
- end of merge · d1b663c8
  BERTOT Yves authored 5 years ago
  
  d1b663c8
- compacting sentences · c4d0cd68
  BERTOT Yves authored 5 years ago
  
  c4d0cd68
Sep 18, 2019
- properties expressed without finType properties and equivalence · 843210e7
  BERTOT Yves authored 5 years ago
  
  843210e7
- section name change · dd68b51a
  BERTOT Yves authored 5 years ago
  
  dd68b51a
Sep 16, 2019
- adds definitions of correctness that are independent from fintype and 2 proofs · f08737ad
  BERTOT Yves authored 5 years ago
  
  f08737ad
Sep 14, 2019
- now pushed the finType construction in the function int_naive5, but · 0bb79b63
  BERTOT Yves authored 5 years ago
  0bb79b63
- obtain an executable version of the algorithm with (int * int) as input type · 9d3ff06a
  BERTOT Yves authored 5 years ago
  9d3ff06a
Sep 13, 2019
- In this file, we add the necessary map construction and the ccw definition · 11844a0c
  BERTOT Yves authored 5 years ago
  11844a0c
- now fixed the size of the map to make it work on non-finite types · 10b977f7
  BERTOT Yves authored 5 years ago
  
  10b977f7
- rearrange the structure of cc_systems · ae7a7908
  BERTOT Yves authored 5 years ago
  
  ae7a7908
Sep 11, 2019
- restructured the proofs of Knuth axioms 4 and 5 · 73ba7bd8
  BERTOT Yves authored 5 years ago
  
  73ba7bd8
- make the equality formulas on determinants work on general rings · 499ded80
  BERTOT Yves authored 5 years ago
  
  499ded80
- proof of axiom5 and axiom5' · 7ae06513
  BERTOT Yves authored 5 years ago
  
  7ae06513
- proved axiom 4 · 3fdb6622
  BERTOT Yves authored 5 years ago
  
  3fdb6622
- cleans up the proof for the first Knuth axiom, extract the unicity property · ee3e8f22
  BERTOT Yves authored 5 years ago
  
  ee3e8f22
Sep 10, 2019
- this adds a more elegant proof of Knuth's first axiom for advanced ccw · 560fe7b4
  BERTOT Yves authored 5 years ago
  
  560fe7b4
- finished proving that the sign of the tail coefficient is the sign · d1046d77
  BERTOT Yves authored 5 years ago
  d1046d77
- closed the section and removed a now useless lemma · dc181a42
  BERTOT Yves authored 5 years ago
  
  dc181a42
Sep 09, 2019
- the statement of ptbd_value is more compatible with tail_coef theorems · 4a7eeaed
  BERTOT Yves authored 5 years ago
  
  4a7eeaed
- makes expand_ptb regular with respect to tail_coef theorems · 2acb272f
  BERTOT Yves authored 5 years ago
  
  2acb272f
Sep 08, 2019
- there was no mistake after all, and the proof of this lemma is complete · 6f7e999b
  BERTOT Yves authored 5 years ago
  
  6f7e999b
- maybe there is a bug in ccw, because not enough tests are made to capture · b99bb786
  BERTOT Yves authored 5 years ago
  b99bb786
Sep 05, 2019
- a little more line optimization · 24b6e0a7
  BERTOT Yves authored 5 years ago
  
  24b6e0a7
- slightly shortened_version · b88b2a1a
  BERTOT Yves authored 5 years ago
  
  b88b2a1a
Sep 03, 2019
- separates computations to make functions available in the polynomial ring · c352f1eb
  BERTOT Yves authored 5 years ago
  
  c352f1eb
- checkpoint · e158ace5
  BERTOT Yves authored 5 years ago
  
  e158ace5
- adds notions of least non zero coefficient, named tail_coef · 9f062321
  BERTOT Yves authored 5 years ago
  
  9f062321
- proved that the perturbed polynomial is never 0 · 20d20500
  BERTOT Yves authored 5 years ago
  
  20d20500
- now did the two side determinants · 99cde8f9
  BERTOT Yves authored 5 years ago
  
  99cde8f9
- prove that the second determinant is the product of differences · 2d91ec97
  BERTOT Yves authored 5 years ago
  
  2d91ec97
- reduce the amount of mathematical structure required for each result · 550c5a1d
  BERTOT Yves authored 5 years ago
  
  550c5a1d