Refinement types

Stream: new members

[Jared green]

I am trying to prove a proposition by defining an algorithm(using refinement types) that, if it is correct, proves the proposition. However there are places where the propositional portion of the outputs is not trivial to prove. Do i have to do that proving myself? And if so, how and where do i do that?
The relevant subconclusion is that this algorithm, which is an optimizer, splits its function to a sum of convex pieces, then does a form of gradient ascent on each piece, then finds a global maximum based on that, all in a certain number of iterations of the ascent being performed on all the pieces at once. The complicating factor is that the form of the pieces changes on each iteration.

[Mario Carneiro]

Most likely, you will have to prove it yourself, although the proof might just be stringing tactics together if you are lucky. A #mwe would be helpful, as this is not a common application so I would like to see how you've set things up

[Jared green]

Truth be told, what i have isn’t even in lean yet, it is in liquidhaskell form. I cannot check it in that form, so I plan on porting it. It is 500 lines in length. How would you like to see it?

[Jared green]

Once i port what i have, where do i place the proofs for the propositional parts of the functions’ outputs?

[Mario Carneiro]

You can post a gist if you want to share the whole 500 lines, or you can focus on a part in a code block here

[Mario Carneiro]

It's possible to write refinement types in lean using subtypes {x // p x}, but it's usually a better idea to define the algorithm separately from the proofs

[Jared green]

The proposition that i am trying to prove is: P=NP. The algorithm I’m designing solves instances of a modified form of SAT.
The representation is a network of nodes, one type representing bits that can be connected to any number of the other type, gatenodes, each one representing a reversible logic gate with a certain number of bidirectional ports, where information goes both ways. Each bit has a weight for how likely it is to be its current value.
For each gatenode, the algorithm selects a possible state that maximises the total amount of weight, with 1-(currentweight) fo a bit flip, independently.
Then the bitnodes take on the Boolean value given more weight everywhere it is connected, and its new weight = proportion of total weight for that value.
If nothing changes the least certain bit (if any are uncertain at all) is flipped, though I’m not sure if that breaks it.
Repeat until either the iteration cap is reached or everything is certain.
Return the result.

[Scott Morrison]

Might I suggest that you first get some experience with formal proofs by trying to prove something that is more likely to be true?

[Scott Morrison]

Don't get me wrong, P \ne NP is a fine problem, and I'm glad that people with ideas on it try to formalize them, but learning to use an ITP and tackling problems like this are both ambitious, and probably best done sequentially rather than concurrently.