Julien Puydt (May 13 2022 at 15:59): Julien Puydt (May 13 2022 at 15:59):I'm trying to understand how to work with complex numbers with mathcomp and affiliated:
Section WithRealClosed.
From mathcomp Require Import rat.
From mathcomp.real_closed Require Import complex realalg.
Open Scope complex_scope.
Definition RR := { realclosure rat }.
Definition CC := complex RR.
Check 1 +i* 2.
Compute Re (1 +i* 2).
Compute Im (1 +i* 2).
Variable w z: CC.
Check w.
Check Re w.
Fail Check w + z.
End WithRealClosed.
Section WithField.
From mathcomp Require Import algC.
Open Scope C_scope.
Check Crat.
Fail Check 'i.
Variable w z: algC.
Fail Check w + z.
End WithField.
I have to say it isn't clear :-/
Yves Bertot (May 16 2022 at 14:05):The inductive type complex is a parameterized type of pairs of two elements of the same type, with the first project named Re and the second project named Im. It does not assume that the type satisfies any property.
When you type Check 1 +i* 2. Coq simply construct such a pair, with natural numbers 1 and 2 as the components, so this object is in type nat[i]. This type is not the type of natural numbers so natural number addition is not adapted to work on these numbers. If you do not open any other scope, "_ + _" is only interpreted as natural number addition.
Usually, in mathcomp, when you want to consider addition of numbers (that are not naturals), we work with a ring. A complex construction over a type which is a ringType inherits the structure of being a ring, through the expected addition and multiplication of complex numbers with respect to their components.
The scope complex_scope is not concerned with adding the notation for addition for complex numbers, because this is simply the addition for a ring. So, just because you opened the scope complex_scope, it does not mean that + will be understood as addition of complex numbers. It is still the default expecting two natural numbers.
If we want addition to parse and be interpreted correctly, we need to say that we want addition to be ring addition by default (and this will be inherited for any type that is at least as strong as a ring, like a field.
After the line Variable w z : CC. you can actually write:
Check (w + z)%R.
Now, if want to build the complex number 1 + 2 i in the type CC, you cannot use the text "1 +i* 2", because this 1 and 2 are natural numbers. The expression "1 +i* 1" does exist, because there is a specific notation so that 1 represents the neutral element for multiplication in any ring. But there is no direct notation mechanism so that 2 is understood directly as a member of the ring. What mathcomp provides instead, is 2%:R, which hides a recursive function that adds 1 to itself a certain number of times, where that number is given by a natural number.
So
Check (w + 1 +i* 2%:R)%R.
succeeds.
I suggest that you add Open Scope ring_scope. Just next to the line where you have Open Scope complex_scope.
For the end of your file, I am a bit confused, because I am not able to reproduce the penultimate failure. But there is one thing that you did which I did not reproduce: My file starts with all the Require Import commands, then there are three lines about implicit arguments,
then there Section opening commands. I do not include the Require Import commands inside any section. I have vague memories that this is frowned upon in Coq practice.
For the last failure, I can again avoid it by making sure addition is interpreted in the right scope:
Check (w + z)%R.
Here is my whole file (tested with coq 8.15.0, mathcomp 1.14.0)
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.real_closed Require Import complex realalg.
From mathcomp Require Import algC.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope complex_scope.
(* Open Scope ring_scope. *)
Definition RR := { realclosure rat }.
Definition CC := complex RR.
Locate "_ +i* _".
Check 1 +i* 2.
Fail Check (1 +i* 2) + (1 +i* 3).
Compute Re (1 +i* 2).
Compute Im (1 +i* 2).
Section WithRealClosed.
Variable w z : CC.
Check (w + z)%R.
Check (w + 1 +i* 2%:R)%R.
Check w.
Check Re w.
End WithRealClosed.
Section WithField.
Open Scope C_scope.
Check Crat.
Check 'i.
Variables w z : algC.
Check (w + z)%R.
End WithField.
To supplement that very precise answer, in the next version of mathcomp (not yet released) you will be able to write 2 instead of 2%:R.
Julien Puydt (May 16 2022 at 22:05):@Yves Bertot Thanks, that definitely helps. I dropped the Set/Unset lines since I don't know what they mean yet.
@Pierre Roux Ah, that was something I was wondering: it's because the next mathcomp version will use HB and have better coercions, isn't it?
Here is a better experiment:
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.real_closed Require Import complex realalg.
Open Scope ring_scope.
Open Scope complex_scope.
Definition RR := { realclosure rat }.
Definition CC := complex RR.
Section EasyTests.
(* uh? *)
Fail Check 1+i*2%R.
Check 1 +i* 2%:R.
(* very good! *)
Variables w z: CC.
Check w + z.
Check w * z.
Check w ^*.
(* those don't fail officially... but still *)
Compute Re (1+i*1).
Compute 'i * 'i.
Compute 'i + 'i.
Compute 'i^*.
End EasyTests.
(I want to see what I can do with trigonometric functions)
Yves Bertot (May 17 2022 at 06:42):@Julien Puydt I still strongly recommend that you include the 3 lines I suggested about implicit arguments, because it is the way the language is supposed to be used in math-comp: These instructions configure Coq so that every theorem or dependently typed function that you define is typed in a way that maximizes usage of implicit arguments. So in the long run, it will be good to understand them enough to work more idiomatically in math-comp and ssreflect. This is a good reminder for us to write a little article to explain what each of this command provides us.
Incidentally, I have been played a little with algC after looking at your question, and it turns out that you need to import some of the ssrnum and ssralg submodules for things to become smooth enough, with respect to notations, for instance.
From mathcomp Require Import all_ssreflect all_algebra all_field.
From mathcomp Require Import ssrnum.
(* From mathcomp.real_closed Require Import complex realalg. *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section WithField.
Variables w z : algC.
(* Check 'Im w. fails, you can't even parse the command with a Fail prefix. *)
(* Note that the header of algC.v also contains Import Order.TTheory. *)
Import GRing.Theory Num.Theory.
(* now the notation is defined, but not in scope. *)
Fail Check 'Im w.
Open Scope ring_scope.
Check 'Im w.
Check (1 + 'i * 2%:R).
(* The answer says that this value could be in any numClosedField *)
Check (1 + 'i * 2%:R + w).
End WithField.
@Yves Bertot Ok, I added those three lines to my test file ; I'll have to check, but I think there was something about them in the mathematical components book, so it's possible it's already documented.
"Import GRing GRing.Field." is something I should have done sooner: it does shorten lines!
I stopped using realalg/algC because I want to play with trigonometry, so I need to have $\pi$ in the real field, even if I introduce it axiomatically:
Variable pi: RR.
Hypothesis def_pi: expi (pi / 2%:R) = 'i. (* FIXME: very incomplete definition! *)
I can prove a few results on $\cos$ and $\sin$ already ; I'm currently stuck trying to prove $\frac12+\frac12=1$ in RR, on the way to get "expi(pi)=-1" :
Lemma two_halves: 1 / 2%:R + 1 / 2%:R = 1 :> RR.
Proof.
rewrite addf_div.
rewrite mul1r. (* FIXME: can't fusion with above !? *)
Admitted.
I probably need to figure out how to work in the rationals where it should be straightforward then push it into reals... then I'll multiply by pi somehow (congr1 of something unclear)...
The ultimate goal in my trigonometry experiments is $\cos(\pi/3)=\frac12$. That will require learning a bit more of Coq/MC!
Pierre Roux (May 17 2022 at 08:47):I think you have many results about trigonometry in MathComp Analysis.
Yves Bertot (May 17 2022 at 11:52):As I recommended before, you should import a few modules to work comfortably. I took my inspiration from the module imports visible at the beginning of algC.v.
Import Order.TTheory GRing.Theory Num.Theory.
If you don't include this line in your header, one of the lemmas mentioned here will not be found.
To prove two_halves : rewrite with distributivity to have (1 + 1) / 2%:R mulrDl then simplify the division using divff and then prove that 1 + 1 is non-zero in one of two ways:
1+1 to 2%:R by the tacticrewrite -[1 + 1]/2%:R. and then use theorem pnatr_neq0.0 < 1 and that the sum of two positive numbers is positive (theorem addr_gt0) to obtain that 0 < 1 + 1 and then use the fact that < is irreflexive.My preferred script is the one using the first of these two alternatives:
by rewrite -mulrDl divff // -[1 + 1]/2%:R pnatr_eq0.
To prove that 1 + 1 is non-zero, you can also use paddr_eq0, ler01 and oner_neq0
Julien Puydt (May 17 2022 at 14:59):Hmmm... if I import Num.Theory, then the one-line proof below fails, because Re gets interpreted as 'Re and then a complex can't be broken in two parts like it wants:
Lemma conjRe: forall z: CC, Re z^* = Re z.
Proof.
by move=> [a b].
Qed.
Well, the good news is that I got better at finding results to use:
Lemma three_thirds: 1 / 3%:R + 1 / 3%:R + 1 / 3%:R = 1 :> RR.
by rewrite -mulr2n addrC -mulrS -mulr_natr div1r mulVf // Num.Theory.pnatr_eq0.
Qed.
and the other news is "by field" does the trick, as I should have expected for trivial rational relations!
Julien Puydt (May 17 2022 at 19:38):I finally managed to prove $\cos(\pi/3)$ satisfies some equation. Now I'm done with complex numbers, I'll dive into polynomials and see whether I can push things through. I'll still have to dive back to my proofs and see if I can simplify them... the lot of them looks awful!
@Pierre Roux Sorry, I see I didn't answer you sooner ; I'm learning as I go, so perhaps indeed MC-analysis has many things -- but I'm more interested in the scenery along path than getting to the destination. I know MC-analysis already has many things and in the future will have even more. I'll probably contribute to it at some point. I'm too weak yet.
Pierre Roux (May 18 2022 at 07:24):Sure, my point is rather that if you are looking for good "solutions" to your exercises, there may be some there.
Julien Puydt (May 18 2022 at 16:28):@Pierre Roux Indeed, fair point!
Notification Bot (May 18 2022 at 16:28):Julien Puydt has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC