wrap nsatz with dropRingSyntax; port CompleteEdwardsCurveTheorems to super_nsatz #16
Conversation
| bash_step. | ||
| bash_step. | ||
| bash_step. | ||
| { conservative_common_denominator. |
There was a problem hiding this comment.
@JasonGross : Is conservative_common_denominator intended to be idempotent?
There was a problem hiding this comment.
Yes. It should leave the primary goal with no divisions in it, and should fail when there is no division. Does it currently do wacky things with the side-conditions? If so, we should guard it with a check that the goal is a field equality.
There was a problem hiding this comment.
Oh, oops, it doesn't work with fractions in denominators yet. I'll fix that.
There was a problem hiding this comment.
Should be fixed by b707a30 (haven't tested it on this example, though)
This should deal with #16 / #16 (comment)
This should handle #16 / #16 (comment)
| { conservative_common_denominator_all. (* FIXME: doesn't do anything *) | ||
| common_denominator_all. nsatz. auto using a_d_y2_nonzero. } | ||
| unfold solve_for_x2; simpl; split; intros; | ||
| (conservative_common_denominator_all; [nsatz | eapply a_d_y2_nonzero; eauto]). |
There was a problem hiding this comment.
conservative_common_denominator_all generates a goal False here, probably by doing something equivalent to unfold not; intro. It would be nice if it left goals of the form _ <> 0.
We no longer try to predict field_simplify_eq. This results in better behavior and less code which is more modular. In particular, the tactic responsible for hiding non-fraction pieces from field_simplify_eq no longer tries to preemptively assert that denominators are nonzero. This improvement is a result of @andres-erbsen's point in #16, #16 (comment) , that we were generating too many side-conditions.
| @@ -633,6 +633,16 @@ Module Field. | |||
| End Homomorphism. | |||
| End Field. | |||
|
|
|||
| (*** Tactics *) | |||
|
|
|||
| Module Import Algebra_syntax_Nsatz. | |||
There was a problem hiding this comment.
What's the reason to do it like this? If you replace
Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.with
Ltac nsatz := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.
Tactic Notation "nsatz" := nsatz.(assuming I haven't messed up my Ltac parsing; if I have, you'll need to do
Ltac nsatz_power n :=
let nn := (eval compute in (BinNat.N.of_nat n)) in
nsatz_sugar_power BinInt.Z0 nn.
Ltac nsatz := nsatz_power 1%nat || nsatz_power 2%nat || nsatz_power 3%nat || nsatz_power 4%nat || nsatz_power 5%nat.
Tactic Notation "nsatz" := nsatz.
Tactic Notation "nsatz" constr(n) := nsatz_power n.), then you can just do Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax, which I think is slightly nicer.
|
What's the status of this PR? |
See #15.