From 2974901b1761995d3b1e5f65959ee7c6afd4f7d6 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 3 Dec 2023 18:10:11 -0800
Subject: [PATCH] Factor ZRange Proper proof (#1764)

For https://github.com/mit-plv/fiat-crypto/pull/1761
---
 src/AbstractInterpretation/Wf.v               | 37 ++---------
 .../ZRangeCommonProofs.v                      | 63 +++++++++++++++++++
 2 files changed, 67 insertions(+), 33 deletions(-)
 create mode 100644 src/AbstractInterpretation/ZRangeCommonProofs.v

diff --git a/src/AbstractInterpretation/Wf.v b/src/AbstractInterpretation/Wf.v
index 87942c42c09..fb1c30b3b4e 100644
--- a/src/AbstractInterpretation/Wf.v
+++ b/src/AbstractInterpretation/Wf.v
@@ -25,7 +25,9 @@ Require Import Rewriter.Language.Inversion.
 Require Import Crypto.Language.InversionExtra.
 Require Import Rewriter.Language.Wf.
 Require Import Rewriter.Language.UnderLetsProofs.
+Require Import Rewriter.Util.Decidable.
 Require Import Crypto.AbstractInterpretation.AbstractInterpretation.
+Require Import Crypto.AbstractInterpretation.ZRangeCommonProofs.
 Import Coq.Lists.List.
 
 Import EqNotations.
@@ -33,6 +35,7 @@ Module Compilers.
   Import Language.Compilers.
   Import UnderLets.Compilers.
   Import AbstractInterpretation.Compilers.
+  Import AbstractInterpretation.ZRangeCommonProofs.Compilers.
   Import Language.Inversion.Compilers.
   Import Language.InversionExtra.Compilers.
   Import Language.Wf.Compilers.
@@ -852,39 +855,7 @@ Module Compilers.
 
       Global Instance abstract_interp_ident_Proper {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t}
         : Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident assume_cast_truncates t).
-      Proof using Type.
-        cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc;
-          repeat first [ reflexivity
-                       | progress subst
-                       | progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Crypto.Util.Option.bind] in *
-                       | progress cbv [Crypto.Util.Option.bind]
-                       | intro
-                       | progress destruct_head'_prod
-                       | progress destruct_head'_bool
-                       | progress destruct_head' option
-                       | progress inversion_option
-                       | discriminate
-                       | solve [ eauto ]
-                       | apply NatUtil.nat_rect_Proper_nondep
-                       | apply ListUtil.list_rect_Proper
-                       | apply ListUtil.list_rect_arrow_Proper
-                       | apply ListUtil.list_case_Proper
-                       | apply ListUtil.pointwise_map
-                       | apply ListUtil.fold_right_Proper
-                       | apply ListUtil.update_nth_Proper
-                       | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
-                       | cbn; apply (f_equal (@Some _))
-                       | progress cbn [ZRange.ident.option.interp]
-                       | progress cbv [zrange_rect]
-                       | apply (f_equal2 pair)
-                       | break_innermost_match_step
-                       | match goal with
-                         | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
-                         | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
-                         | [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
-                           => specialize (H y); rewrite H1, H2 in H
-                         end ].
-      Qed.
+      Proof using Type. apply ZRange.ident.option.interp_Proper. Qed.
 
       Global Instance extract_list_state_Proper {t}
         : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t)))
diff --git a/src/AbstractInterpretation/ZRangeCommonProofs.v b/src/AbstractInterpretation/ZRangeCommonProofs.v
new file mode 100644
index 00000000000..1a6992810b7
--- /dev/null
+++ b/src/AbstractInterpretation/ZRangeCommonProofs.v
@@ -0,0 +1,63 @@
+(* Proofs shared by Wf and Proofs *)
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relations.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.FoldBool.
+Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.AbstractInterpretation.ZRange.
+
+Module Compilers.
+  Import AbstractInterpretation.ZRange.Compilers.
+  Export ZRange.Settings.
+
+  Module ZRange.
+    Module ident.
+      Module option.
+        Section interp_related.
+          Context {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+                  (assume_cast_truncates : bool).
+          Global Instance interp_Proper {t} : Proper (eq ==> @type.eqv t) (ZRange.ident.option.interp assume_cast_truncates).
+          Proof using Type.
+            intros idc idc' ?; subst idc'.
+            cbv [type.related respectful type.interp]; destruct idc;
+              repeat first [ reflexivity
+                           | progress subst
+                           | progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Crypto.Util.Option.bind] in *
+                           | progress cbv [Crypto.Util.Option.bind]
+                           | intro
+                           | progress destruct_head'_prod
+                           | progress destruct_head'_bool
+                           | progress destruct_head' option
+                           | progress inversion_option
+                           | discriminate
+                           | solve [ eauto ]
+                           | apply NatUtil.nat_rect_Proper_nondep
+                           | apply ListUtil.list_rect_Proper
+                           | apply ListUtil.list_rect_arrow_Proper
+                           | apply ListUtil.list_case_Proper
+                           | apply ListUtil.pointwise_map
+                           | apply ListUtil.fold_right_Proper
+                           | apply ListUtil.update_nth_Proper
+                           | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
+                           | cbn; apply (f_equal (@Some _))
+                           | progress cbn [ZRange.ident.option.interp]
+                           | progress cbv [zrange_rect]
+                           | apply (f_equal2 pair)
+                           | break_innermost_match_step
+                           | match goal with
+                             | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
+                             | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
+                             | [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
+                               => specialize (H y); rewrite H1, H2 in H
+                             end ].
+          Qed.
+        End interp_related.
+      End option.
+    End ident.
+  End ZRange.
+End Compilers.