Lemma to_affine_add proof looks weird

[briansmith]

I see this fragment:

      (* zero + P = P   -- cases for x and y *)
      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.

      (* P  + zero = P   -- cases for x and y *)
      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.

Notice that the comments mention both x and y but the assert statements only mention X1 twice and X2 twice, never mentioning Y1 or Y2 at all. It looks like copy-pasta gone wrong.

[briansmith]

Notice in particular that the first two assertions are exactly the same and are thus redundant (IIUC), and the last two assertions are exactly the same and likewise redundant (IIUC).

[andres-erbsen]

I agree it looks counter-intuitive. What is going on is that there are actually four goals left behind by the earlier script, and each assert...fsatz sequence solves one of them, causing the next goal to become active. And assertions proven in one goal do not carry over to the next. Not putting { and } around the each of the four cases is nothing but subpar coding style on my part. Once coq ships a release that includes coq/coq#6944 we can make this kind of spaghetti code cause a compilation error.

(if #457 fails to build, then the above explanation is mistaken)

[briansmith]

Thanks for the explanation. That makes perfect sense!