Topic: How are "rights" working?

I have been able to use Coq to prove some conjectures about forgetful functors. My plan is to write posts explaining this later. For now, I have questions about ownership of propositions and "rights". I tried to use "rights" and could not get it to work.

I proved a general theorem that allows me to prove some forgetful functors are functors. In the dalilcoin draft the statement looks like this:

Thm MetaCatForgetful_gen : TTpAll A All Obj TpArr A Prop All U TpArr A set All Hom TpArr A TpArr A TpArr TpArr set set Prop Imp All X A Imp Ap Obj X All Y A Imp Ap Obj Y All F TpArr set set Imp Ap Ap Ap Hom X Y F Ap Ap Ap SetHom Ap U X Ap U Y F Ap Ap Ap Ap Ap Ap Ap Ap Ap Ap TTpAp TTpAp TTpAp TTpAp MetaFunctor A TpArr set set set TpArr set set Lam x0 A Ap Obj x0 Hom Lam x0 A Ap Ap CF Ap U x0 Lam x1 set x1 Lam x0 A Lam _ A Lam _ A Lam x3 TpArr set set Lam x4 TpArr set set Ap Ap CF Ap U x0 Lam x5 set Ap x3 Ap x4 x5 Lam _ set True SetHom Lam x0 set Ap Ap CF x0 Lam x1 set x1 Lam x0 set Lam _ set Lam _ set Lam x3 TpArr set set Lam x4 TpArr set set Ap Ap CF x0 Lam x5 set Ap x3 Ap x4 x5 U Lam _ A Lam _ A Lam x2 TpArr set set x2

Here it is in the proof explorer:

https://dalilcoin.com/proofexplorer/que … e04510d583
https://dalilcoin.com/proofexplorer/que … b12b668e42

Since I believed I could use this result to resolve many conjectures, when I declared ownership I include the policy that each right to use it in a new document would cost 5 fraenks payable to an address I have.

Then I wrote a second document that imported it like this:

Known MetaCatForgetful_gen : TTpAll A All Obj TpArr A Prop All U TpArr A set All Hom TpArr A TpArr A TpArr TpArr set set Prop Imp All X A Imp Ap Obj X All Y A Imp Ap Obj Y All F TpArr set set Imp Ap Ap Ap Hom X Y F Ap Ap Ap SetHom Ap U X Ap U Y F Ap Ap Ap Ap Ap Ap Ap Ap Ap Ap TTpAp TTpAp TTpAp TTpAp MetaFunctor A TpArr set set set TpArr set set Lam x0 A Ap Obj x0 Hom Lam x0 A Ap Ap CF Ap U x0 Lam x1 set x1 Lam x0 A Lam _ A Lam _ A Lam x3 TpArr set set Lam x4 TpArr set set Ap Ap CF Ap U x0 Lam x5 set Ap x3 Ap x4 x5 Lam _ set True SetHom Lam x0 set Ap Ap CF x0 Lam x1 set x1 Lam x0 set Lam _ set Lam _ set Lam x3 TpArr set set Lam x4 TpArr set set Ap Ap CF x0 Lam x5 set Ap x3 Ap x4 x5 U Lam _ A Lam _ A Lam x2 TpArr set set x2

I followed the instructions here about publishing:

https://github.com/aliibrahim80/dalilco … ematics.md

I used "commitdraft" and after four confirmations tried "publishdraft". But "publishdraft" gave me this error:

Rights for proposition 0ce5cb2613cc8e51c800d3a13d5108a2e4a80b457fd7fd8c27e5b3b12b668e42 (TTrDdHETnTWUuHhfbzvzAvHHDixLJyiqWb) are not balanced.
Tx is not supported by the current ledger

I thought maybe it was because I needed to buy rights (from myself?) to use the proposition. After a lot of trying I managed to use the command "creategeneraltx" to buy rights. (Is there an easier way?)

creategeneraltx '{"vin":[{"address":"Db32coZtGdFYFpTVjpzqMGqpqAfk1rhun3","assetid":"64a0069d9f71024f7465e192634350921a9c4b6e798caa8597b5cfad7f13fdc9"}],"vout":[{"address":"Db32coZtGdFYFpTVjpzqMGqpqAfk1rhun3","preasset":{"type":"preasset","preassettype":"currency","val":{"fraenks":"14.9974706"}}},{"address":"DsXfRh8gFjJri1re8CPMhtiT96DirXQdwU","preasset":{"type":"preasset","preassettype":"currency","val":{"fraenks":"5"}}},{"address":"Djqd8nCQfJVEMVwNU2VRLwLV4WKedKSDWA","preasset":{"preassettype":"rightsprop","propid":"0ce5cb2613cc8e51c800d3a13d5108a2e4a80b457fd7fd8c27e5b3b12b668e42","propaddr":"TTrDdHETnTWUuHhfbzvzAvHHDixLJyiqWb","units":1}}]}'

After using signtx and sendtx the tx confirmed. I used printassets and confirmed I have the rights:

Djqd8nCQfJVEMVwNU2VRLwLV4WKedKSDWA:
097105a64a2391557055c94becfd41654a63d8a0adddaabccd8b4765cbf5f372: (id c6682b554c0ae8cbcec5bbe25dd0acf2a796aff9ba5a53c23852454a8219f615) [1716] RightsProp 0ce5cb2613cc8e51c800d3a13d5108a2e4a80b457fd7fd8c27e5b3b12b668e42 1

It was unfortunate that the publishdraft command still said that the rights were not balanced.

After rethinking this I decided to try to use creategeneraltx to change the policy so that it is free to use instead:

creategeneraltx '{"vin":[{"address":"TTrDdHETnTWUuHhfbzvzAvHHDixLJyiqWb","assetid":"f4b3f23c4dd0a0cbf04c807f768151f5a9781a9b533b1faed9a6453b5bc51f3f"},{"address":"TNTkvDF3auHaBj4p3ZrXLB5vESPw151sqi","assetid":"11cdbea54fe838c804587fa56134371a3cfc24552255a74d1a1df28937b726f3"},{"address":"Db32coZtGdFYFpTVjpzqMGqpqAfk1rhun3","assetid":"f31f2cc5b21df1d2d0d2f2c8a235c741930e9b553a382b6b82e77e8c24d92a30"}],"vout":[{"address":"TTrDdHETnTWUuHhfbzvzAvHHDixLJyiqWb","obligation":{"type":"obligation","lockaddress":"DghQ5ELMWmuZ2kSdcpFtKCrGxJcnrooW4W","lockheight":0,"reward":false},"preasset":{"type":"preasset","preassettype":"ownsprop","propid":"0ce5cb2613cc8e51c800d3a13d5108a2e4a80b457fd7fd8c27e5b3b12b668e42","propaddr":"TTrDdHETnTWUuHhfbzvzAvHHDixLJyiqWb","owneraddress":"DsXfRh8gFjJri1re8CPMhtiT96DirXQdwU","royalty":{"cants":0}}},{"address":"TNTkvDF3auHaBj4p3ZrXLB5vESPw151sqi","obligation":{"type":"obligation","lockaddress":"DghQ5ELMWmuZ2kSdcpFtKCrGxJcnrooW4W","lockheight":0,"reward":false},"preasset":{"type":"preasset","preassettype":"ownsprop","propid":"b1cac0bee122b6229783c01c2831d67ee9d76746b39dec98d98272e04510d583","propaddr":"TNTkvDF3auHaBj4p3ZrXLB5vESPw151sqi","owneraddress":"DsXfRh8gFjJri1re8CPMhtiT96DirXQdwU","royalty":{"cants":0}}},{"address":"Db32coZtGdFYFpTVjpzqMGqpqAfk1rhun3","preasset":{"type":"preasset","preassettype":"currency","val":{"fraenks":"14.9962412"}}}]}'

In this fortunate case after the tx confirmed "publishdraft" worked. Here is the document with "Known Proposition 0" used:

https://dalilcoin.com/proofexplorer/que … dac388f20a

This took a lot of trying and failing to do, and at the end I can only say I avoided the problem of needing to use rights. How should it have been done instead?

Re: How are "rights" working?

No replies? Is there anyone here to answer this?

Re: How are "rights" working?

Just a quick reply to let you know I've seen and read your post. It will take some time look into the details.

It does sound like you were treating rights correctly. The problem might have been that you really needed rights to use two different versions of the proposition. Every proposition can be owned in two forms: the "pure" form (the proposition independent of the theory it is proven in) and the "theory" form (specific to the theory). You probably got ownership of both the pure and theory forms and required 5 fraenks to use the proposition for each form. This means you would need to buy two rights: 5 fraenks for the right to use the pure form and another 5 fraenks for the right to use the theory form. It sounds like you only bought rights for one of them.

Re: How are "rights" working?

OK. I didn't know there were two kinds of rights like this. Thanks for explaining.

Re: How are "rights" working?

Looking more closely into the issue, I think there is really a problem with the code for publishdraft. I can't find a place where it actually spends the rights or adds an output to buy the rights. I will try to reproduce the problem and hopefully fix it.