Newbie here, I created a proof with mmj2. How do I add the proof to the database #3908
Comments
|
This doesn't solve the file conversion problem, but the following theorems are relevant to move antecedents: ex Also, for closure and if statement specifically, there is: ifcld |
|
Hey thanks very much, that already helped me. Currently I am trying to show that F is a permutation. |
You can open the *.mmp file in mmj2, and then copy the content displayed and paste it into a *.mm file. You have to edit a little bit. Your example noideahowtonameit (in mmj2): would become: I usually write the theorem in an *.mm file, import it into mmj2, prove it in mmj2, and copy the proof back to the *.mm file. |
Here is what I came up with. I get |
|
Incidentally this is very similar to https://us.metamath.org/mpeuni/fzto1st.html |
|
Oh wow that was awesome. @tirix , you are awesome. Thank you very much. @icecream17 thanks for the link as well. I'll be studying your process. Also I have figured out that natural deduction is so good. When I started my journey a few days ago I had really big issues on getting any deduction. Not knowing which theorems are applicable for a given use case was extremely daunting. For some reason, I wasn't able to even show that A<B, B<C -> A<C, and searching in metamath-exe engine was not yielding the correct results, even though I was absolutely certain that something like that MUST be in the database. One question on the approach. To build bigger statements, do I start from the inside and do hypothesis building with a1i, Because sometimes I need to show A -> B where A and B syntactically differ in the inside. I have made a WIP draft of what I want to show. I want to show that I'd already be quite happy. Is my current approach correct. Do you have any ideas for improvement. I'd love to hear your opinion. After all I don't want to use an approach that leads me to a dead end without me knowing that I am stuck. |
|
Yes, natural deduction is really nice to use, so maybe one tip I'd give is to rather write your theorem in a deduction form, as in: This way it will be much easier to use later on.
I think one of the biggest hurdle when starting with Metamath is to find the theorem you're looking for. There are some naming patterns which may help. For example, the one you're stating is "Lower Than is TRansitive, Induction version", so it's named
Generally I like to work with deduction form, in which case your A would be broken down into a conjunction (like Then you have to derive |
|
If you have a function Several of your functions seem to be permutation cycles, or compositions of a few cycles. I've started to define permutation cycles and prove some of their properties in my mathbox. Maybe it would be easier to deal with these cycles, but that would be a different approach from your PDF, so maybe it's not the approach you prefer. |
|
You are my hero. That was what I was searching. I just couldn't find the fitting theorem. I'll check out your mathbox and I'll likely try both approaches to see what is easier. My goal overall is to define later. The actual proof of that statement was a big case distinction, as the defined value of Also recall the definition of I'd hope to show that with above restriction that I assume that there are theorems in metamath for closed ranges that make this possible. Something like Because if I want to calculate As well as the evaluation of the indicator function twice. This gives me a total of 16 cases that I have to check, because I need to check that the image of one application fulfils the condition of the next function to be able to evaluate it. I have thought to evaluate the image on all 16 parts for all functions |
|
Well i have tried using f1o2d, here is what I put in Autocomplete gave me which just can't be right. Let us focus on d4: The other steps seem simpler. Intuitively it is clear what i need to do. I need to check the cases. But I have no clue how to get the substitution. I have studied the theorems that use f1o2d, but the final condition in the last step is usually trivial, like this one There must be an easier way. Am I missing something? |
|
Yes it does not seem right! MMJ2's autocomplete is not an oracle and sometimes goes the wrong way... Here I've filled in the first case: |
|
Alright I was working few hours on this problem. The learning curve is really steep. My thought process is to use the same &W2 and &W3 as you I am also struggling to understand your bootstrapping of the theorem. I see that you are using eqeq2 and bibiid* and I see that it works, but I don't understand the rationale behind it. For example if I try to finish the problem I already know that I will have problems with nested ifs and I don't know how to resolve them Next I've tried to resolve 40 partially. It is hideous, but for now I am happy that I was way faster. It only took me 8 hours to get that down, and some proof steps are also done via deduction, which I am somewhat happy that I am slowly grasping the concepts. But some things are still unclear. Intuitively it is clear and Which is a contradiction. I tried it out The deduction mode takes time to get used to, but I think it will be better. This is my proof of concept, I likely will need to rewrite it eventually to make sure that ph is correct. Do you have any feedback, I'd love to hear it. |
|
in this case the theorem is mtod and xrltnr also perhaps looking at the proof of mteqand and the various theorems that use it would be helpful Perhaps we should add a section on how to find theorems we don't know about. There are two strategies I can think of: using the website: table of contents, this theorem is referenced by, definitons, and nearby theorems using the search functionality of metamath.exe, mmj2, or the online metamath proof maker (I forget the name, feel free to edit my post) Although dealing with propositions is less amenable to these strategies. It's why earlier me proved ioin9i8, because it was a very nontrivial process for past me to figure out... |
Here is how to complete the hypotheses for The idea is that we handle the cases of the
Then In This results again in a two-cases situation with an |
|
Ah thanks, sorry I was busy working and I couldn't reply. I think I might have chosen the wrong path to define the function. Recently I was thinking by defining F as a union F1, F2, F3. where All I want is to have function definitions so that I can evaluate F(x). But to do that I need to be able to make sure that there exists exaclty one y such that xFy. This has been so far the bane of my problems. By defining F1,F2,F3 I wanted to show independently that they are 1-1 and onto with disjoint domains and ranges and then glue them together. I think this is a more sensible approach, but I have no reference if that will actually be easier. Does my approach make sense, and if so what's the best way moving forward. I was thinking of defining F3 something like that But then I would need to show that F_3 is a function from and I have figured that my reasoning is abstract, since I know why this function is surjective, but without knowing how to prove it in metamath. |
|
the idea would work ( ~ f1oco ) I think it would work similarly to tirix's proof above, where a theorem like f1o2d would be used (f1o2d seems like the most practical theorem for proving bijectivity) (incidentally I thought the proof would make this task solved) |
|
Actually writing the function as a union of other functions is a clever idea. Proving that each individual function is 1-1 and onto should not be too difficult (we have for example |
So the mmp file format looks different than the mm file format. And for the love of god I couldn't find any utility to convert it.
The mmj2 repo help says that there is no functionality to add a proof automatically.
In the attachment there is a file of a subproof I am hoping is helpful. What I want to show is that a function is a permutation.
proofsandsupproofs.zip
In the zip archive there are three files. One is a subproof that mmj2 already says is correct. (File: noideahowtonameit.mmp)
The second and third one is the actual proof .
Here I am still debating if I can generalize to include the case ( 1 ... 0 ) --> ( 1 ... 0 ) which is a map from the empty to the empty set.
This is a map, which should also be bijective, so it should work.
I want to show that the function defined by F is a permutation. The domain is ( 1 ... N ) where N is in NN0 (here I am debating if NN0 is better than NN, it might make more sense to define it that way, but the only use case will be N in NN). Let the domain be A.
I want to show that F: A->A is a function from A to A.
Then I planned to use the fact that A is finite together with an injection/surjection (I still don't know which one is easier) -> F bijective.
Let i \in {1,...,m}
The function F is defined by two if statements. In Latexlike it would be something like
{1,...,m} -> {1,...,m}
j |-> m-i+j+\chi(m-i+j,i) if 1 \leq j \leq i-1
j |-> j if i=j
j |-> j-i+\chi(j-i,i) i+1 \leq j \leq m
Eventually I want to show that this is a permutation. For now, I'd be more than happy to show that it is a function with dom=cod={1,...,m}
This is why I developed this new lemma. My hope is that I can show
(x e. ( 1 ... M ) -> bla)
by showing
(x e. (1 ... M ) and x = I ) -> bla
(x e. (1 ... M ) and x \neq I and x < l) -> bla
(x e. (1 ... M ) and x \neq I and not ( x < l )) -> bla
where bla is the fact that the evaluation of F(x) is in (1...m)
Then I can use my theorem to eliminate all, such that the unification works. But I didn't find a good way. The only thing I've found is a syllogism rule, which is quite helpful, but I didn't find how I can move antecedents inside and outside of the if statements.
The text was updated successfully, but these errors were encountered: