Enhance proportionality #47
Conversation
…itted as they are proven with alternate methods in feature-permutations
|
Also please run static validation and fix issues |
|
CI is currently failing because the Qlib version bump hasn't gone into opam yet. Once it does, the CI will start failing because SQIR doesn't work with the new Qlib, until the SQIR PR with the fixes is merged. |
src/CoreData/Proportional.v
Outdated
|
|
||
|
|
||
|
|
||
| Declare Custom Entry rwlist. |
There was a problem hiding this comment.
Genuine question: What's the benefit of this over notations?
There was a problem hiding this comment.
It's quite similar to just notations, but restricted to a specific domain so that we don't pollute or compete with the rest of the term grammar. I was also attempting to get these things to not evaluate too much too soon, but that wasn't successful (in Ltac1). Moreover, I don't know how to (ergonomically) use an Ltac2-based solution without switching over to Ltac2 completely within a proof, which is not infeasible or necessarily too much work, but it has bad version compatibility and has lots of little incompatibilities. Finally, since the final zxrewrite tactic is only used in a handful of places, I didn't optimize for making it particularly powerful.
src/CoreData/Proportional.v
Outdated
|
|
||
|
|
||
|
|
||
| Ltac tac_iter_simpl lst := |
There was a problem hiding this comment.
Could you explain/comment what is happening in L440-L590?
There was a problem hiding this comment.
Much of this is an attempt to do a general rewrite tactic (allowing modifiers like multiple rewriting, direction changing, etc.) in Ltac1, when Ltac2 is really needed for a lot of that functionality. I'll remove what isn't used and comment what is.
| @@ -1,485 +1,55 @@ | |||
| From QuantumLib Require Import Matrix. | |||
There was a problem hiding this comment.
Thanks for moving this to QLib!
| simpl. | ||
| apply Z_0_is_wire. | ||
| Qed. | ||
|
|
||
| Lemma stack_nwire_distribute_r : forall {n m o p} (zx0 : ZX n m) (zx1 : ZX m o), |
There was a problem hiding this comment.
I think we want to keep this diagrammatic
There was a problem hiding this comment.
Good catch; I'll revert.
Add notions of semantic equality and of proportionality up to a designated constant, along with tactic support for both. Also prove soundness of proportionality / reconstruction of constants, leading ultimately also the the decidability of proportionality (though this is highly inefficient, and in fact ineffective due to an opaque definition in QuantumLib).
Note: This PR is incomplete. It needs further description and several main theorems are
Admitted.