1 files changed, 35 insertions, 0 deletions
diff --git a/src/Compilers/Z/RewriteAddToAdcWf.v b/src/Compilers/Z/RewriteAddToAdcWf.v
new file mode 100644
index 000000000..3b9fb1ff5
--- /dev/null
+++ b/src/Compilers/Z/RewriteAddToAdcWf.v
@@ -0,0 +1,35 @@
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.InterpretToPHOASWf.
+Require Import Crypto.Compilers.Named.CompileWf.
+Require Import Crypto.Compilers.Named.WfFromUnit.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.RewriteAddToAdc.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Bool.
+
+Section language.
+  Local Hint Resolve internal_base_type_dec_lb internal_base_type_dec_lb dec_rel_of_bool_dec_rel : typeclass_instances.
+
+  Lemma Wf_RewriteAdc {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : Wf (RewriteAdc e).
+  Proof.
+    unfold RewriteAdc, option_map; break_innermost_match;
+      [ .. | solve [ intros var1 var2; destruct (Hwf var1 var2); auto with wf ] ];
+      repeat first [ eapply @Wf_InterpToPHOAS with (t:=Arrow _ _)
+                   | progress split_andb
+                   | congruence
+                   | intros; eapply @PositiveContextOk
+                   | solve [ auto | eapply @BinPos.Pos.eqb_eq ]
+                   | eapply @Wf_from_unit
+                   | eapply @dec_rel_of_bool_dec_rel
+                   | eapply @internal_base_type_dec_lb
+                   | eapply @internal_base_type_dec_bl
+                   | intros var1 var2; specialize (Hwf var1 var2); destruct Hwf;
+                     constructor; assumption ].
+  Qed.
+End language.
+
+Hint Resolve Wf_RewriteAdc : wf.