Update the proofs for Coq 8.13 and ssreflect 1.12.0

[yiyunliu]

A summary of what I did:

• The redefined gather_atoms isn't used for some reason even though ett_ind is required and imported. I included an extra import at the bottom of the import/require block for each file that uses pick fresh to prevent the definition from being overridden.
• The eauto tactic now seems smarter than it used to be. Sometimes it discharges the proof completely and I had to comment out the manual proof that follows.
• omega -> lia
• Fixed the proofs from fc_dec_fun.v. I honestly have no idea what is going on in this file. I added a few more hacky cases and used clear dependent fuel to help some of the proofs go through.

[sweirich]

Some of these changes don't work with Coq 8.10, which is the version of Coq I have installed on my machine. Is it possible to make them more flexible so they work on both versions? For example, here is what I did to make congruence.v work on my machine:

@@ -156,9 +156,7 @@ Proof.
   - (* app rel *) intros G b a B A H K1 K2 K3 G1 G2 x A1 a1 a2 D H1 H2 H3.
     subst. simpl.
     rewrite tm_subst_tm_tm_open_tm_wrt_tm.
-    eapply E_AppCong; eauto 2.
-
-    (* eapply K1; eauto 2. *)
+    eapply E_AppCong; try eapply K1; eauto 2.
     eapply (Typing_lc H2).
   - (* app irrel case *)
     intros G b B a A K0 K1 K2 K3 G1 G2 x A1 a1 a2 D H2 H3 H4. subst.

Overall, looking at these proofs --- they are themselves really bad and not very maintainable. So it would be good to clean them up a bit if you are interested. We can talk about that on Friday.

[yiyunliu]

Let's talk about this on Friday. I didn't maintain backward compatibility when I was updating the code but that's definitely something that I should have kept in mind.

There are proofs that look like:

eauto 2. (* ... followed by eapply ... *)

and it's unclear to me why instead of using eauto with a bigger depth the proof is restricting the depth while adding a manually written eapply. I can imagine it's either because the computer was slow or eauto had issues figuring out simple applications in older versions (I can try it out by installing 8.10). The eauto in 8.13 discharges the case completely and the extra eapply would cause an error. I'm not sure what is the optimal way of fixing it. An ad-hoc fix would simply require a try in front of the eapply but maybe there's a better and cleaner way.

I don't know why fc_fun_dec.v has so many failed obligations in 8.13 (and the extra manual proofs I added would naturally cause things to fail in 8.10). I did get tons of warnings about the tactic language. We can look into this issue together since I'm not confident with debugging tactics at the moment (it might have been an import issue similar to the one with gather_atoms).

[sweirich]

Yes, let's talk about this tomorrow. I wish Coq tactics were a little bit more specified and a little bit more consistent between versions. However, it may be that if we want more robust proof scripts, we'll need to make a lot of changes to the development.

On Oct 20, 2021, at 4:25 PM, Yiyun Liu @.***> wrote:

Let's talk about this on Friday. I didn't maintain backward compatibility when I was updating the code but that's definitely something that I should have kept in mind.

There are proofs that look like:

eauto 2. (* ... followed by eapply ... *) and it's unclear to me why instead of using eauto with a bigger depth the proof is restricting the depth while adding a manually written eapply. I can imagine it's either because the computer was slow or eauto had issues figuring out simple applications in older versions (I can try it out by installing 8.10). The eauto in 8.13 discharges the case completely and the extra eapply would cause an error. I'm not sure what is the optimal way of fixing it. An ad-hoc fix would simply require a try in front of the eapply but maybe there's a better and cleaner way.

I don't know why fc_fun_dec.v has so many failed obligations in 8.13 (and the extra manual proofs I added would naturally cause things to fail in 8.10). I did get tons of warnings about the tactic language. We can look into this issue together since I'm not confident with debugging tactics at the moment (it might have been an import issue similar to the one with gather_atoms).

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/sweirich/corespec/pull/2*issuecomment-948009465__;Iw!!IBzWLUs!CXt9IJLqpSFcm2USS-6xu1NGKviqFpQdHTImX-SLudz_7KZzjtBdqW88DSvyS1oBfbX8$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAQBS5TNPBPHHXOTOC6R5QTUH4QSNANCNFSM5GEKGD5A__;!!IBzWLUs!CXt9IJLqpSFcm2USS-6xu1NGKviqFpQdHTImX-SLudz_7KZzjtBdqW88DSvyS2zU7TGr$.