Build in 8.6, build PRF_Encryption_IND_CPA.v

[andres-erbsen]

In the main repo:

• automated the proofs that were broken in 8.6
  • [ ] there is no issue with using the ring and nia tactics, right?
• moved some nested lemmas out of theorems when it was potentially causing breakage

In PRF_Encryption_IND_CPA.v:

• re-posed some section-defined lemmas to keep make them remain accessible after fcf tactic invocations (no idea why they become inaccessible)

[adampetcher]

Merged. Thanks.

In the future, please update the copyright statement at the top of any file that you modify to ensure that it is still accurate.. The easiest way to do this is to remove the first line of the header (which is what I plan to do to all files in the future, anyway). I have already fixed the copyright header in the files you modified.

I have no problem with the ring and nia tactics. Any tactic that doesn't introduce assumptions is fine with me. You probably no better than I do which tactics should be avoided for maintainability reasons.

The issue with disappearing hypotheses (and other variables) seems to be caused by the intuition tactic, which is used by many of the FCF tactics. It clears unused variables from the scope, which is problematic because they may be needed later. This problem happened sometimes in 8.5, but it seems to be more frequent in 8.6.

[andres-erbsen]

Ok.