Clean and grind
Clean has a really unwieldy Subcircuit type, which carries custom Spec / Assumptions statements that are designed to "replace" the constraints of a subcircuit during soundness and completeness proofs, respectively.
Often, replacing things can be done by simp: If simp can find a equality or iff lemma about a particular type of Subcircuit, such as (FormalCircuit.toSubcircuit ...).Constraints ↔ TARGET, then simp can rewrite the term to TARGET. This is easy and does not need TARGET to be a prop on Subcircuit.
The problem for clean used to be that we wanted it to automatically replace statements with strictly weaker versions. E.g., if a hypothesis had (FormalCircuit.toSubcircuit ...).Constraints, and we know the implication:
(FormalCircuit.toSubcircuit ...).Constraints → TARGET
Then we want clean to replace the hypothesis with TARGET, even though it nominally makes the statement to prove stronger. Why? Because TARGET is hiding subcircuit details with a high-level statement (the Spec), and therefore the rewrite actually makes the proof easier even though "logically" the proof gets harder.
simp is fundamentally unable to perform such rewrites that are not equalities / equivalences. This is why we put the TARGETs on the Subcircuit type itself, and accepted many complications just to get those nicer statements!
Meanwhile, grind does have annotations like @[grind →] to signal that the lemma should be used in forward reasoning. Can it solve the problem more elegantly?
I think no, because grind only works if it can close the goal. For a usual circuit, we'd expect to do useful rewrites without closing the goal. So in fact, for a general circuit proof tactic, we still need something custom. Now that I thought it through, it doesn't seem very hard anymore, using metaprogramming.
Clean and
grindClean has a really unwieldy
Subcircuittype, which carries customSpec/Assumptionsstatements that are designed to "replace" the constraints of a subcircuit during soundness and completeness proofs, respectively.Often, replacing things can be done by simp: If simp can find a equality or iff lemma about a particular type of Subcircuit, such as
(FormalCircuit.toSubcircuit ...).Constraints ↔ TARGET, then simp can rewrite the term to TARGET. This is easy and does not need TARGET to be a prop on Subcircuit.The problem for clean used to be that we wanted it to automatically replace statements with strictly weaker versions. E.g., if a hypothesis had
(FormalCircuit.toSubcircuit ...).Constraints, and we know the implication:Then we want clean to replace the hypothesis with TARGET, even though it nominally makes the statement to prove stronger. Why? Because TARGET is hiding subcircuit details with a high-level statement (the
Spec), and therefore the rewrite actually makes the proof easier even though "logically" the proof gets harder.simpis fundamentally unable to perform such rewrites that are not equalities / equivalences. This is why we put the TARGETs on the Subcircuit type itself, and accepted many complications just to get those nicer statements!Meanwhile,
grinddoes have annotations like@[grind →]to signal that the lemma should be used in forward reasoning. Can it solve the problem more elegantly?I think no, because
grindonly works if it can close the goal. For a usual circuit, we'd expect to do useful rewrites without closing the goal. So in fact, for a general circuit proof tactic, we still need something custom. Now that I thought it through, it doesn't seem very hard anymore, using metaprogramming.