search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Carathéodory #81

Closed Tragicus closed 2 years ago

Tragicus commented 2 years ago

Strengthens convA' and convACA' and adds a few lemmas. Defines l-modules as convex spaces. Proves Carathéodory's Theorem. Contains general purpose lemmas that should not stay here (e.g. everything in section split_prod and everything in section caratheodory except lemma caratheodory).

affeldt-aist commented 2 years ago

You seem to have created the PR from your master branch.

affeldt-aist commented 2 years ago

I tried to improve a few things in this branch: https://github.com/affeldt-aist/infotheo/commits/tragicus_master. You can maybe cherry-pick the last commit.

Tragicus commented 2 years ago

You seem to have created the PR from your master branch.

Indeed, is that bad practice ?

affeldt-aist commented 2 years ago

Indeed, is that bad practice ?

Yes. :-)

Tragicus commented 2 years ago

Indeed, is that bad practice ?

Yes. :-)

Oh, sorry. I do not see a way to change the branch now, I will pay attention in the future. Many thanks for the review and sorry for the "admit". I see that some checks failed, should I make the code compatible with mathcomp-1.13.0? Also, the "Require Import div" raises a warning, should it be put at the beginning of the file?

affeldt-aist commented 2 years ago

should I make the code compatible with mathcomp-1.13.0?

If it is not too much of a burden.

Also, the "Require Import div" raises a warning, should it be put at the beginning of the file?

Yes.

Tragicus commented 2 years ago

I have just tried to rebase. The HB.instance line 2040 does not compile and I could not fix it (everything else works fine).

affeldt-aist commented 2 years ago

I have just tried to rebase. The HB.instance line 2040 does not compile and I could not fix it (everything else works fine).

You mean fun_orderedConvType? I am a bit puzzled because the last commit compiles fine on my machine. About your PR: you are PRing from your master and the list of commits seems to reveal duplications of commits that are already in master.

Tragicus commented 2 years ago

I have just tried to rebase. The HB.instance line 2040 does not compile and I could not fix it (everything else works fine).

You mean fun_orderedConvType? I am a bit puzzled because the last commit compiles fine on my machine. About your PR: you are PRing from your master and the list of commits seems to reveal duplications of commits that are already in master.

I had missed the updated dependency on hierarchy-builder, it is fixed. I may have messed up with the rebase. Should I try to make a new clean branch and redo the PR ?

affeldt-aist commented 2 years ago

Should I try to make a new clean branch and redo the PR ?

I think it is easier this way.

affeldt-aist commented 2 years ago

I couldn't push (at least without push-force) so I put a new commit in another branch: https://github.com/affeldt-aist/infotheo/pull/85

affeldt-aist commented 2 years ago

You'll find a new commit here: https://github.com/affeldt-aist/infotheo/pull/85 (still reading)

affeldt-aist commented 2 years ago

@Tragicus We've merged PR #85 which should contained all the commits of this PR, so that it should be ok to close.

Tragicus commented 2 years ago

Your second proofreading does not appear in the list of commits. Besides, the definition of linear_affine was broken due to HB, I have just fixed it.

affeldt-aist commented 2 years ago

Your second proofreading does not appear in the list of commits.

Really? I thought I squashed my last commits into one.

Besides, the definition of linear_affine was broken due to HB, I have just fixed it.

I also fixed it in PR #85 .

Tragicus commented 2 years ago

Ah ok, then everything is all right.