Skip to content

[WIP] Make linear subspaces canonically a tbLatticeType#653

Draft
pi8027 wants to merge 1 commit into
math-comp:masterfrom
pi8027:vspace-lattice
Draft

[WIP] Make linear subspaces canonically a tbLatticeType#653
pi8027 wants to merge 1 commit into
math-comp:masterfrom
pi8027:vspace-lattice

Conversation

@pi8027

@pi8027 pi8027 commented Nov 19, 2020 •
edited
Loading

Copy link
Copy Markdown
Member
Motivation for this change

This is my first attempt to make linear subspaces {vspace vT} canonically a tbLatticeType. In vector.v, some operators for linear subspace (subsetv, fullv, addv, and capv) have been redefined as notations for order operators. The first obstacle is that falgebra.v does not compile since both prodv and capv (Order.meet) distributes over addv (Order.join) and so addv_addoid (in falgebra.v) is now redundant with join_addoid (in order.v).

Closes #613

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

@pi8027 pi8027 added kind: enhancement Issue or PR about addition of features. kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...) labels Nov 19, 2020
@pi8027 pi8027 added this to the 1.13.0 milestone Nov 19, 2020
pi8027
pi8027 commented Nov 19, 2020
View reviewed changes
Comment thread mathcomp/algebra/vector.v Outdated
Comment thread algebra/vector.v
Comment on lines 641 to +666
Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U) && (w \in V).
Proof. by rewrite !memvE subv_cap. Qed.
Proof. by rewrite !memvE lexI. Qed.

@pi8027 pi8027 Nov 19, 2020

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If _ \in _ for linear subspaces is defined by using Order.le as in intervals, this proof can probably be exact: lexI. (I think it requires some more work.)

math-comp/mathcomp/algebra/interval.v

Lines 493 to 494 in 0606b6b

Lemma in_itvI x i1 i2 : x \in i1 `&` i2 = (x \in i1) && (x \in i2).
Proof. exact: lexI. Qed.

@pi8027 pi8027 force-pushed the vspace-lattice branch 3 times, most recently from 5531642 to 4c5ea49 Compare November 23, 2020 02:52
@pi8027 pi8027 added the needs: fix PR that needs to be fix (generally because reviewers asked to). label Nov 23, 2020
@pi8027 pi8027 force-pushed the vspace-lattice branch 4 times, most recently from 5081207 to a1a81b0 Compare November 26, 2020 16:56
@pi8027

pi8027 commented Dec 26, 2020

Copy link
Copy Markdown
Member Author

The first obstacle is that falgebra.v does not compile since both prodv and capv (Order.meet) distributes over addv (Order.join) and so addv_addoid (in falgebra.v) is now redundant with join_addoid (in order.v).

Redefining Monoid.add_law as follows would probably solve this issue. But, if there is a multiplication-like operator that distributes over two different addition-like operators, it does not work. Is there any plan to extend the bigop hierarchy?

math-comp/mathcomp/ssreflect/bigop.v

Lines 349 to 354 in ee410eb

Structure add_law (mul : T -> T -> T) := AddLaw {
add_operator : com_law;
_ : left_distributive mul add_operator;
_ : right_distributive mul add_operator
}.
Local Coercion add_operator : add_law >-> com_law. 

(* We have to swap its parameter (multiplication) and the first projection    *)
(* (addition) so that its canonical instances can be indexed by constants of  *)
(* multiplication rather than addition.                                       *)
Structure mul_distr_law (add : T -> T -> T) := MulDistrLaw {
  mul_distr_operator : T -> T -> T;
  (* The following two axioms are part of `mul_law`. A telescope cannot be used here anymore. *)
  _ : left_zero idm mul_distr_operator;
  _ : right_zero idm mul_distr_operator;

  _ : left_distributive mul_distr_operator add;
  _ : right_distributive mul_distr_operator add
}.

@pi8027

pi8027 commented Feb 10, 2021

Copy link
Copy Markdown
Member Author

But, if there is a multiplication-like operator that distributes over two different addition-like operators, it does not work.

I self answer this: muln distributes over maxn and addn, and so it does not work.

@pi8027 pi8027 force-pushed the vspace-lattice branch 2 times, most recently from 998316f to ab67780 Compare March 18, 2021 19:37
@pi8027 pi8027 modified the milestones: 1.13.0, 1.14.0 May 11, 2021
@CohenCyril CohenCyril modified the milestones: 1.14.0, 1.15.0 Jan 19, 2022
@pi8027 pi8027 removed this from the 1.15.0 milestone Jun 15, 2022
@pi8027 pi8027 added this to the 1.16.0 milestone Jun 15, 2022
@affeldt-aist affeldt-aist modified the milestones: 1.16.0, 1.17.0 Jan 11, 2023
@affeldt-aist affeldt-aist modified the milestones: 1.17.0, 1.18.0 May 9, 2023
@affeldt-aist affeldt-aist modified the milestones: 1.18.0, 2.2.0 Oct 24, 2023
@proux01 proux01 modified the milestones: 2.2.0, 2.3.0 Jan 17, 2024
@CohenCyril CohenCyril modified the milestones: 2.3.0, 2.4.0 Nov 6, 2024
@pi8027 pi8027 modified the milestones: 2.4.0, 2.5.0 Mar 19, 2025
@proux01 proux01 modified the milestones: 2.5.0, 2.6.0 Sep 22, 2025
@pi8027 pi8027 removed this from the 2.6.0 milestone Feb 24, 2026
@pi8027 pi8027 mentioned this pull request Apr 27, 2026
Open
14 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

kind: enhancement Issue or PR about addition of features. kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...) needs: fix PR that needs to be fix (generally because reviewers asked to).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Modular lattice of linear subspaces

4 participants

@pi8027 @CohenCyril @proux01 @affeldt-aist