add elementary lemmas about modules #15

langston-barrett · 2016-11-17T02:45:41Z

Some direct consequences of the module laws

urkud · 2016-11-17T03:01:32Z

theory/modules.v

+Section Module_Lemmas.
+  Context `{Module R M}.
+
+  Lemma mon_unit_unique : forall i, ((forall x : M, x & i = x) -> i = mon_unit).


It seems that this lemma does not need a module structure. You just need M to be a group.
By the way, the following order of quantifiers is enough: ∀x i : M, x & i = x → i = mon_unit.

Lemma mon_unit_unique : ∀ x i, x & i = x → i = mon_unit. Proof. intros x i Hyp. apply (left_cancellation (&) x). now rewrite right_identity. Qed.

@urkud Thanks for the tips!

urkud · 2016-11-17T03:10:02Z

theory/modules.v

+    now rewrite left_identity in Hunit.
+  Qed.
+
+  Lemma mult_rzero : forall x : M, sm 0 x = mon_unit.


Why not use ⋅ notation? It is more readable.
Disclaimer: I'm neither a coq exprert, nor an experienced math-classes user.

I don't know how to type it effectively :'( I should've copy-pasted before making a PR

I use ~/.XCompose under Linux to type these chars.

urkud · 2016-11-17T04:02:20Z

theory/modules.v

+  Lemma mult_rzero : forall x : M, sm 0 x = mon_unit.
+    intros.
+    (* add mon_unit to the left side *)
+    rewrite <- right_identity.


You may use the following for the proof

intros. apply (mon_unit_unique (0 · x) (0 · x)). rewrite <- distribute_r. now rewrite left_identity.

if mon_unit_unique is what I propose above.

I'm getting an error while trying that proof, and it's one I've seen before and had trouble interpreting:

Ltac call to "now" failed. Error: Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints: UNDEFINED EVARS: ?X289==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x |- relation M] (internal placeholder) {?r} ?X290==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x |- relation M] (internal placeholder) {?r0} ?X291==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x (do_subrelation:=do_subrelation) |- Proper (equiv ==> ?X290@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero; __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit; __:=Mnegate; __:=sm; __:=H; __:=x} ==> ?X289@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero; __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit; __:=Mnegate; __:=sm; __:=H; __:=x}) scalar_mult] (internal placeholder) {?p} ?X292==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x |- ProperProxy ?X290@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero; __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit; __:=Mnegate; __:=sm; __:=H; __:=x} x] (internal placeholder) {?p0} ?X295==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x |- relation M] (internal placeholder) {?r1} ?X296==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x (do_subrelation:=do_subrelation) |- Proper (?X289@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero; __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit; __:=Mnegate; __:=sm; __:=H; __:=x} ==> ?X295@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero; __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit; __:=Mnegate; __:=sm; __:=H; __:=x} ==> flip impl) equiv] (internal placeholder) {?p1} ?X297==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x |- ProperProxy ?X295@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero; __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit; __:=Mnegate; __:=sm; __:=H; __:=x} (0 · x)] (internal placeholder) {?p2} .

Sorry, I've copied the last two lines from lines 26, 27 of your commit without checking. I thought that I get an error because I didn't apply your patch about "Proper".

This works:

apply scalar_mult_proper ; [apply right_identity|reflexivity].

I have no idea why it fails to rewrite. And why it rewrites in your proof.

langston-barrett · 2016-11-17T18:43:40Z

@urkud I believe I've addressed all of your comments. Thanks again for the review, very helpful for a beginner like myself 😁

This proof requires a change of notation: the condition `Proper sm` must use the `·` notation. See coq-community/corn#35 for discussion. Additional context: http://stackoverflow.com/questions/40624302/what-does-the-error-message-setoid-rewrite-failed-undefined-evars-mean/40668305#40668305

langston-barrett · 2016-11-18T02:40:08Z

I welcome feedback on lemma names as well (the hardest part of Computer Science, right?)

define ring tactic on modules

urkud · 2016-12-05T01:49:23Z

theory/groups.v

@@ -43,6 +43,12 @@ Proof.
  now rewrite associativity, left_inverse, left_identity.
 Qed.

+Lemma mon_unit_unique : forall x i, x & i = x -> i = mon_unit.


It seems that other lemmas in this project use a different syntax:

Lemma mon_unit_unique x i : x & i = x → i = mon_unit. Proof. intro.

Yep, good eye!

urkud · 2016-12-05T01:51:28Z

theory/modules.v

@@ -0,0 +1,60 @@
+From MathClasses.interfaces Require Import vectorspace canonical_names.
+From MathClasses.theory Require Import groups rings.


I get the following warning:

*** Warning: in file theory/modules.v, required library groups matches several files in path (found groups.v in varieties, . and theory; used the latter)

I have no warning with this form:

From MathClasses Require Import interfaces.vectorspace interfaces.canonical_names theory.groups theory.rings.

Thanks, fixed!

urkud · 2016-12-05T03:10:05Z

theory/modules.v

+  (* So we can use the `ring` tactic when we need to *)
+  Add Ring my_ring : (stdlib_ring_theory R). 
+
+  Lemma mult_rzero : forall x : M, 0 · x = mon_unit.


This and mult_munit are particular cases of the following fact: a SemiGroup_Morphism of two groups preserves mon_unit.
I'm going to submit a pull request for theory/groups.v with this fact included.

Great, please comment here when that is done!

urkud · 2016-12-05T03:12:19Z

theory/modules.v

+    now rewrite left_identity, right_inverse.
+  Qed.
+
+  Lemma multiplication_by_negative_1_is_negation : forall x : M, (-1) · x = - x.


Cf. negate_mult_distr_l and negate_nult_distr_r in rings.v.

Those lemmas are about ring multiplication, and do not apply to sm as far as I can tell. Am I mistaken? Why do you mention them?

I meant that you can use similar names. Sorry for bad wording.

urkud · 2016-12-05T03:13:25Z

theory/modules.v

+    reflexivity.
+  Qed.
+
+  Lemma double_negation : forall x, - (- x) = x.


This is a particular case of groups.negate_involutive (or rings.negate_involutive). Doesn't need module structure.

Removed, thanks!

langston-barrett · 2016-12-05T20:31:16Z

@urkud Thanks for the review!

urkud · 2016-12-06T01:15:04Z

I've pushed the group theory fact mentioned in the review to urkud/math-classes@d41ec3da59c826783e3ad6499a56c90b4765b0d9.

spitters · 2017-06-04T17:56:25Z

Is this PR still valid, or has it been superseded?
If you update, I'll pull the request.

langston-barrett · 2017-06-05T17:58:20Z

@spitters I think it needs cleaning up before it can be merged. I'll comment here if and when I get around to it.

langston-barrett · 2018-03-29T03:26:29Z

I don't think I'm going to get around to fixing this. I'm making an issue to include my fixes to the laws for inner product spaces in case anyone wants to take that up.

urkud reviewed Nov 17, 2016

View reviewed changes

langston-barrett added 2 commits November 17, 2016 17:47

add elementary lemmas about modules

5221596

langston-barrett added 2 commits November 18, 2016 12:13

modules: add negation lemmas

1f81c79

define ring tactic on modules

fix definition of InnerProductSpace

eb698a6

urkud reviewed Dec 5, 2016

View reviewed changes

langston-barrett added 3 commits December 5, 2016 12:16

fix notation in mon_unit_unique

1d6f030

fix module imports

3475871

remove duplicate of groups.negative_involutive

586c90d

langston-barrett closed this Mar 29, 2018

langston-barrett mentioned this pull request Mar 29, 2018

Fix inner product space laws #49

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

add elementary lemmas about modules #15

add elementary lemmas about modules #15

langston-barrett commented Nov 17, 2016

urkud Nov 17, 2016 •

edited

Loading

langston-barrett Nov 17, 2016

urkud Nov 17, 2016

langston-barrett Nov 17, 2016

urkud Nov 17, 2016

urkud Nov 17, 2016

langston-barrett Nov 17, 2016

urkud Nov 17, 2016

urkud Nov 17, 2016

langston-barrett commented Nov 17, 2016

langston-barrett commented Nov 18, 2016

urkud Dec 5, 2016

langston-barrett Dec 5, 2016

urkud Dec 5, 2016

langston-barrett Dec 5, 2016

urkud Dec 5, 2016

langston-barrett Dec 5, 2016

urkud Dec 5, 2016

langston-barrett Dec 5, 2016

urkud Dec 6, 2016

urkud Dec 5, 2016

langston-barrett Dec 5, 2016

langston-barrett commented Dec 5, 2016

urkud commented Dec 6, 2016

spitters commented Jun 4, 2017

langston-barrett commented Jun 5, 2017

langston-barrett commented Mar 29, 2018

		@@ -0,0 +1,60 @@
		From MathClasses.interfaces Require Import vectorspace canonical_names.
		From MathClasses.theory Require Import groups rings.

add elementary lemmas about modules #15

add elementary lemmas about modules #15

Conversation

langston-barrett commented Nov 17, 2016

urkud Nov 17, 2016 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

langston-barrett commented Nov 17, 2016

langston-barrett commented Nov 18, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

langston-barrett commented Dec 5, 2016

urkud commented Dec 6, 2016

spitters commented Jun 4, 2017

langston-barrett commented Jun 5, 2017

langston-barrett commented Mar 29, 2018

urkud Nov 17, 2016 •

edited

Loading