Merge pull request #1481 from GaloisInc/saw-core-coq/fix-universe-constraints

[saw-core-coq] Fix weird universe constraints generated in SAWCorePreludeExtra

Author: mergify[bot]

saw-core-coq/coq/_CoqProject

@@ -13,3 +13,5 @@ handwritten/CryptolToCoq/SAWCorePrelude_proofs.v
 handwritten/CryptolToCoq/SAWCorePreludeExtra.v
 handwritten/CryptolToCoq/SAWCoreScaffolding.v
 handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+
+handwritten/CryptolToCoq/Everything.v

saw-core-coq/coq/handwritten/CryptolToCoq/Everything.v

@@ -0,0 +1,17 @@
+(* This file imports everything together in order to make sure
+   that there are no universe inconsistencies *)
+
+(* generated *)
+From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
+From CryptolToCoq Require Import SAWCorePrelude.
+
+(* handwritten *)
+From CryptolToCoq Require Import CompM.
+From CryptolToCoq Require Import CompMExtra.
+From CryptolToCoq Require Import CoqVectorsExtra.
+From CryptolToCoq Require Import CryptolPrimitivesForSAWCoreExtra.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+From CryptolToCoq Require Import SAWCorePrelude_proofs.
+From CryptolToCoq Require Import SAWCorePreludeExtra.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v

@@ -72,7 +72,13 @@ Qed.
 
 Theorem unfold_fold_IRT As Ds D : forall u, unfoldIRT As Ds D (foldIRT As Ds D u) = u.
 Proof.
-  revert Ds; induction D; try destruct u; simpl; f_equal; try easy.
+  revert Ds; induction D; intros; try destruct u; simpl(*; f_equal; try easy*).
+  (* For some reason using `f_equal` above generates universe constraints like
+     `prod.u0 < eq.u0` which cause problems later on when it is assumed that
+     `eq.u0 = Coq.Relations.Relation_Definitions.1 <= prod.u0` by
+     `returnM_injective`. The easiest solution is just to not use `f_equal`
+     here, and rewrite by the relevant induction hypotheses instead. *)
+  all: try rewrite IHD; try rewrite IHD1; try rewrite IHD2; try rewrite H; try easy.
   (* All that remains is the IRT_BVVec case, which requires functional extensionality
      and the fact that genBVVec and atBVVec define an isomorphism *)
   intros; rewrite <- (gen_at_BVVec _ _ _ u).