Do most of abs-int interp proofs

1 files changed, 655 insertions, 55 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 3e4631de8..ebc60d888 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -4,6 +4,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Classes.RelationPairs.
 Require Import Coq.Relations.Relations.
 Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.BasicLemmas.
 Require Import Crypto.Util.Sum.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Prod.
@@ -11,7 +12,14 @@ Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.ZUtil.AddGetCarry.
+Require Import Crypto.Util.ZUtil.AddModulo.
+Require Import Crypto.Util.ZUtil.CC.
+Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Rshi.
+Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
@@ -47,6 +55,13 @@ Module Compilers.
 
   Module ZRange.
     Module type.
+      Module base.
+        Module option.
+          Lemma is_bounded_by_None t v : ZRange.type.base.option.is_bounded_by (@ZRange.type.base.option.None t) v = true.
+          Proof. induction t; cbn; cbv [andb]; break_innermost_match; eauto. Qed.
+        End option.
+      End base.
+
       Module option.
         Lemma is_bounded_by_impl_related_hetero t
               (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
@@ -55,8 +70,348 @@ Module Compilers.
         Proof. induction t; cbn in *; intuition congruence. Qed.
       End option.
     End type.
-  End ZRange.
 
+    Module ident.
+      Module option.
+        (** First we prove relatedness for some particularly complicated identifiers separately *)
+        Section interp_related.
+          Context (cast_outside_of_range : zrange -> Z -> Z).
+
+          Local Notation interp_is_related idc
+            := (type.related_hetero
+                  (fun t st v => ZRange.type.base.option.is_bounded_by st v = true)
+                  (ZRange.ident.option.interp idc)
+                  (ident.gen_interp cast_outside_of_range idc)).
+
+          Local Ltac z_cast_t :=
+            cbn [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some];
+            cbv [ZRange.ident.option.interp_Z_cast ident.cast ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by is_tighter_than_bool respectful_hetero is_bounded_by_bool];
+            intros; break_innermost_match; trivial;
+            rewrite ?Bool.andb_true_iff, ?Bool.andb_false_iff in *; destruct_head'_and; destruct_head'_or; repeat apply conj; Z.ltb_to_lt;
+            try reflexivity; try lia.
+
+          Lemma interp_related_Z_cast r : interp_is_related (@ident.Z_cast r).
+          Proof. z_cast_t. Qed.
+
+          Lemma interp_related_Z_cast2 r : interp_is_related (@ident.Z_cast2 r).
+          Proof. z_cast_t. Qed.
+
+          Lemma interp_related_List_flat_map A B : interp_is_related (@ident.List_flat_map A B).
+          Proof.
+            cbn; cbv [respectful_hetero]; intros.
+            destruct_head' option; cbn in *; [ | reflexivity ].
+            break_match; cbn in *; [ | reflexivity ].
+            let v := (eval cbv [base.interp ZRange.type.base.option.interp ZRange.type.base.interp] in (@ZRange.type.base.option.interp)) in
+            progress change v with (@ZRange.type.base.option.interp) in *.
+            progress fold (@base.interp) in *.
+            rewrite FoldBool.fold_andb_map_iff in *.
+            rewrite OptionList.fold_right_option_seq in *.
+            destruct_head'_ex.
+            destruct_head'_and.
+            rewrite List.flat_map_concat_map, concat_fold_right_app.
+            subst.
+            lazymatch goal with
+            | [ H : List.map _ ?ls1 = List.map _ ?ls' |- length (List.fold_right _ _ ?ls1) = length (List.fold_right _ _ (List.map _ ?ls2)) /\ _ ]
+              => is_var ls1; is_var ls2; is_var ls';
+                   revert dependent ls'; intro ls'; revert dependent ls2; revert ls'; induction ls1 as [|? xs IHxs];
+                     intros [|? ls'] [|? ls2]; cbn [length] in *; intros; cbn in *;
+                     [ tauto | exfalso; discriminate.. | ]
+            end.
+            repeat first [ progress cbn in *
+                         | progress subst
+                         | discriminate
+                         | congruence
+                         | progress autorewrite with distr_length
+                         | progress destruct_head'_and
+                         | rewrite combine_app_samelength
+                         | rewrite FoldBool.fold_andb_map_iff in *
+                         | specialize (IHxs _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption))
+                         | match goal with
+                           | [ H : cons _ _ = cons _ _ |- _ ] => inversion H; clear H
+                           | [ H : S _ = S _ |- _ ] => inversion H; clear H
+                           | [ H : forall v, _ = v \/ _ -> _ |- _ ] => pose proof (H _ (or_introl eq_refl)); specialize (fun v pf => H v (or_intror pf))
+                           | [ H : forall x y, ?R x y = true -> match ?f x with Some _ => _ | None => _ end = true, H' : Some _ = ?f ?x' |- _ ]
+                             => specialize (H _ _ ltac:(eassumption)); rewrite <- H' in H
+                           | [ |- context[List.In _ (_ ++ _)] ] => setoid_rewrite List.in_app_iff
+                           end
+                         | solve [ intuition ] ].
+          Qed.
+
+          Lemma interp_related_List_partition A : interp_is_related (@ident.List_partition A).
+          Proof.
+            cbn; cbv [respectful_hetero]; intros.
+            destruct_head' option; cbn in *; [ | break_innermost_match; reflexivity ].
+            let v := (eval cbv [base.interp ZRange.type.base.option.interp ZRange.type.base.interp] in (@ZRange.type.base.option.interp)) in
+            progress change v with (@ZRange.type.base.option.interp) in *.
+            progress fold (@base.interp) in *.
+            rewrite FoldBool.fold_andb_map_iff in *.
+            destruct_head'_ex.
+            destruct_head'_and.
+            repeat break_match_step ltac:(fun v => let t := type of v in match (eval hnf in t) with prod _ _ => idtac end).
+            repeat match goal with H : option (list _) |- _ => revert dependent H end.
+            lazymatch goal with
+            | [ Heq : List.partition _ _ = (?l0, ?l1), H : length ?ls1 = length ?ls2 |- _ ]
+              => is_var ls1; is_var ls2; is_var l0; is_var l1;
+                   revert dependent l0; intro l0; revert dependent l1; intro l1;
+                     revert dependent ls2; intro ls2;
+                       revert ls2 l0 l1;
+                       induction ls1 as [|? xs IHxs]; intros [|? ls2]; cbn [length] in *; cbn in *;
+                         [ intros [|? ?] [|? ?]; cbn in *; intros; break_innermost_match; cbn in *;
+                           inversion_prod; inversion_option; subst..
+                         | ];
+                         [ tauto | exfalso; discriminate.. | intros ]
+            end.
+            repeat first [ progress cbn in *
+                         | progress subst
+                         | match goal with
+                           | [ H : S _ = S _ |- _ ] => inversion H; clear H
+                           end
+                         | discriminate
+                         | congruence
+                         | progress destruct_head'_and
+                         | progress inversion_prod
+                         | progress eta_expand
+                         | rewrite Bool.if_const
+                         | specialize (fun l0 l1 => IHxs _ l0 l1 ltac:(eassumption))
+                         | specialize (fun l0 l1 => IHxs l0 l1 ltac:(eassumption))
+                         | specialize (IHxs _ _ (@surjective_pairing _ _ _))
+                         | progress Bool.split_andb
+                         | match goal with
+                           | [ |- context[Option.bind ?x ?y] ] => destruct x eqn:?
+                           | [ H : bool_eq _ _ = true |- _ ] => apply bool_eq_ok in H
+                           | [ H : forall v, _ = v \/ _ -> _ |- _ ] => pose proof (H _ (or_introl eq_refl)); specialize (fun v pf => H v (or_intror pf))
+                           | [ |- context[match ?b with true => ?f ?x | false => ?f ?y end] ]
+                             => replace (match b with true => f x | false => f y end)
+                               with (f match b with true => x | false => y end)
+                                    by now case b
+                           | [ H : context[match ?b with true => ?f ?x | false => ?f ?y end] |- _ ]
+                             => replace (match b with true => f x | false => f y end)
+                               with (f match b with true => x | false => y end)
+                               in H
+                               by now case b
+                           | [ H : _ = (_, _) -> _ |- _ ] => specialize (fun pf1 pf2 => H (@path_prod _ _ _ _ pf1 pf2))
+                           | [ H : ?x = _, H' : context[?x] |- _ ] => rewrite H in H'
+                           | [ H : ?x = _ :> bool |- context[?x] ] => rewrite H
+                           | [ H : forall x y, ?R x y = true -> match ?f x with Some _ => _ | None => _ end _ = true, H' : ?f ?x' = Some _ |- _ ]
+                             => specialize (H _ _ ltac:(eassumption)); rewrite H' in H
+                           end
+                         | progress break_innermost_match_step ].
+          Qed.
+
+          Local Ltac handle_lt_le_t_step_fast :=
+            first [ match goal with
+                    | [ H : (?a <= ?b)%Z, H' : (?b <= ?a)%Z |- _ ]
+                      => pose proof (@Z.le_antisymm _ _ H H'); clear H H'
+                    | [ H : (?a <= ?b <= ?a)%Z |- _ ]
+                      => pose proof (@Z.le_antisymm _ _ (proj1 H) (proj2 H)); clear H
+                    end ].
+
+          Local Ltac handle_lt_le_t_step :=
+            first [ handle_lt_le_t_step_fast
+                  | match goal with
+                    | [ |- context[Z.leb ?a ?b = true] ] => rewrite !Z.leb_le
+                    | [ |- context[Nat.eqb ?a ?b = true] ] => rewrite !Nat.eqb_eq
+                    | [ |- context[Z.eqb ?a ?b = true] ] => rewrite !Z.eqb_eq
+                    | [ H : context[andb ?a ?b = true] |- _ ] => rewrite !Bool.andb_true_iff in H
+                    | [ H : context[Z.leb ?a ?b = true] |- _ ] => rewrite !Z.leb_le in H
+                    | [ H : context[Nat.eqb ?a ?b = true] |- _ ] => rewrite !Nat.eqb_eq in H
+                    | [ H : context[Z.eqb ?a ?b = true] |- _ ] => rewrite !Z.eqb_eq in H
+                    end ].
+
+          Local Ltac simplify_ranges_t_step_fast :=
+            first [ match goal with
+                    | [ H : ZRange.lower ?r = ZRange.upper ?r |- _ ]
+                      => is_var r; let x := fresh in destruct r as [r x]; cbn in H; subst x
+                    | [ H : context[ZRange.type.base.is_bounded_by r[_ ~> _]%zrange _] |- _ ]
+                      => progress cbn [ZRange.type.base.is_bounded_by] in H
+                    | [ H : context[is_bounded_by_bool _ r[_ ~> _]%zrange] |- _ ]
+                      => progress cbv [is_bounded_by_bool] in H
+                    end ].
+          Local Ltac simplify_ranges_t_step :=
+            first [ simplify_ranges_t_step_fast ].
+
+          Local Ltac non_arith_t :=
+            repeat first [ assumption
+                         | match goal with
+                           | [ |- ?R ?x ?x ] => reflexivity
+                           | [ H : forall x : unit, _ |- _ ] => specialize (H tt)
+                           | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
+                           | [ H : ?x = ?x |- _ ] => clear H
+                           | [ H : false = true |- _ ] => exfalso; clear -H; discriminate
+                           | [ H : ~?R ?x ?x |- _ ] => exfalso; apply H; reflexivity
+                           | [ |- ZRange.type.base.option.is_bounded_by ZRange.type.base.option.None _ = true ]
+                             => apply type.base.option.is_bounded_by_None
+                           | [ H : FoldBool.fold_andb_map _ ?l1 ?l2 = true |- length ?l1 = length ?l2 ]
+                             => eapply FoldBool.fold_andb_map_length, H
+                           | [ H : forall x y, Nat.eqb x y = true -> _ |- _ ] => specialize (fun x => H x x (@Nat.eqb_refl x))
+                           | [ H : forall x, true = true -> _ |- _ ] => specialize (fun x => H x eq_refl)
+                           | [ H : forall v, List.In v (List.combine ?ls1 ?ls2) -> ?R (fst v) (snd v) = true,
+                                 H1 : List.nth_error ?ls1 ?n = Some ?v1,
+                                 H2 : List.nth_error ?ls2 ?n = Some ?v2
+                                 |- ?R ?v1 ?v2 = true ]
+                             => apply (H (v1, v2)), (@nth_error_In _ _ n); clear -H1 H2
+                           | [ H : ?T, H' : ~?T |- _ ] => exfalso; solve [ apply H', H ]
+                           | [ H : List.nth_error ?ls ?n = Some _, H' : List.nth_error ?ls' ?n = None |- _ ]
+                             => let Hlen := fresh in
+                                assert (Hlen : length ls = length ls') by congruence;
+                                exfalso; clear -H H' Hlen;
+                                apply nth_error_value_length in H;
+                                apply nth_error_error_length in H';
+                                omega
+                           | [ |- (0 <= 1)%Z ] => clear; omega
+                           end
+                         | handle_lt_le_t_step_fast
+                         | simplify_ranges_t_step_fast
+                         | progress intros
+                         | progress subst
+                         | progress inversion_option
+                         | progress inversion_prod
+                         | progress destruct_head'_and
+                         | progress destruct_head'_unit
+                         | progress destruct_head'_prod
+                         | progress destruct_head'_ex
+                         | break_innermost_match_step
+                         | break_innermost_match_hyps_step
+                         | progress cbn [ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Option.bind FoldBool.fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In] in *
+                         | progress destruct_head'_bool
+                         | solve [ auto with nocore ]
+                         | progress fold (@base.interp) in *
+                         | let v := (eval cbv [base.interp ZRange.type.base.option.interp ZRange.type.base.interp] in (@ZRange.type.base.option.interp)) in
+                           progress change v with (@ZRange.type.base.option.interp) in *
+                         | handle_lt_le_t_step
+                         | simplify_ranges_t_step
+                         | match goal with
+                           | [ |- context[andb ?a ?b = true] ] => rewrite !Bool.andb_true_iff
+                           | [ H : FoldBool.fold_andb_map _ _ _ = true |- _ ] => rewrite FoldBool.fold_andb_map_iff in H
+                           | [ |- FoldBool.fold_andb_map _ _ _ = true ] => rewrite FoldBool.fold_andb_map_iff
+                           | [ H : forall (x : option _), _ |- _ ] => pose proof (H None); specialize (fun x => H (Some x))
+                           | [ H : forall x y z (w : option _), _ |- _ ] => pose proof (fun x y z => H x y z None); specialize (fun x y z w => H x y z (Some w))
+                           | [ H : forall v, _ = v \/ _ -> _ |- _ ] => pose proof (H _ (or_introl eq_refl)); specialize (fun v pf => H v (or_intror pf))
+                           | [ |- context[length ?x] ] => tryif is_var x then fail else (progress autorewrite with distr_length)
+                           | [ H : List.In _ (List.combine _ _) |- _ ] => apply List.In_nth_error in H
+                           | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H
+                           | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine
+                           | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
+                           | [ H : context[List.nth_error (List.seq _ _) _] |- _ ] => rewrite nth_error_seq in H
+                           | [ |- context[List.nth_error (List.seq _ _) _] ] => rewrite nth_error_seq
+                           | [ H : context[List.nth_error (List.firstn _ _) _] |- _ ] => rewrite nth_error_firstn in H
+                           | [ |- context[List.nth_error (List.firstn _ _) _] ] => rewrite nth_error_firstn
+                           | [ H : context[List.nth_error (List.skipn _ _) _] |- _ ] => rewrite nth_error_skipn in H
+                           | [ |- context[List.nth_error (List.skipn _ _) _] ] => rewrite nth_error_skipn
+                           | [ H : context[List.nth_error (update_nth _ _ _) _] |- _ ] => rewrite nth_update_nth in H
+                           | [ |- context[List.nth_error (update_nth _ _ _) _] ] => rewrite nth_update_nth
+                           | [ H : context[List.nth_error (List.app _ _) _] |- _ ] => rewrite nth_error_app in H
+                           | [ |- context[List.nth_error (List.app _ _) _] ] => rewrite nth_error_app
+                           | [ H : context[List.nth_error (List.rev _) _] |- _ ] => rewrite nth_error_rev in H
+                           | [ |- context[List.nth_error (List.rev _) _] ] => rewrite nth_error_rev
+                           | [ H : List.nth_error (Lists.List.repeat _ _) _ = Some _ |- _ ] => apply nth_error_repeat in H
+                           | [ H : List.nth_error (repeat _ _) _ = Some _ |- _ ] => apply nth_error_repeat in H
+                           | [ H : length ?l1 = length ?l2 |- context[length ?l1] ] => rewrite H
+                           | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H'
+                           | [ |- context[List.flat_map _ _] ] => rewrite List.flat_map_concat_map, concat_fold_right_app
+                           | [ H : S _ = S _ |- _ ] => inversion H; clear H
+                           | [ H : List.fold_right (fun x y => x <- x; y <- y; Some _)%option (Some ?init) ?ls = Some ?v |- _]
+                             => rewrite OptionList.fold_right_option_seq in H
+                           | [ |- and _ _ ] => apply conj
+                           end
+                         | progress cbv [bool_eq option_map List.nth_default Definitions.Z.bneg is_bounded_by_bool] in *
+                         | match goal with
+                           | [ |- ?R (nat_rect ?P ?O ?S ?n) (nat_rect ?P' ?O' ?S' ?n) = true ]
+                             => is_var n; induction n; cbn [nat_rect];
+                                generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
+                                intros
+                           | [ |- ?R (nat_rect ?P ?O ?S ?n ?x) (nat_rect ?P' ?O' ?S' ?n ?y) = true ]
+                             => is_var n; is_var x; is_var y;
+                                revert dependent x; revert dependent y; induction n; cbn [nat_rect];
+                                generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
+                                intros
+                           | [ H : length ?ls = length ?ls' |- ?R (List.fold_right ?f ?x ?ls) (List.fold_right ?f' ?x' ?ls') = true ]
+                             => is_var ls; is_var ls';
+                                let IH := fresh "IH" in
+                                revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; cbn [List.fold_right length] in *;
+                                [
+                                 | exfalso; clear -H; discriminate | exfalso; clear -H; discriminate
+                                 | specialize (IH ls');
+                                   generalize dependent (List.fold_right f x); generalize dependent (List.fold_right f' x') ];
+                                intros
+                           | [ H : length ?ls = length ?ls' |- ?R (List.fold_right ?f ?x ?ls) (List.fold_right ?f' ?x' ?ls') = true ]
+                             => is_var ls; is_var ls';
+                                let IH := fresh "IH" in
+                                revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [List.fold_right length] in *;
+                                [
+                                 | exfalso; discriminate | exfalso; discriminate
+                                 | specialize (IH ls');
+                                   generalize dependent (List.fold_right f x); generalize dependent (List.fold_right f' x') ];
+                                intros
+                           | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls) (list_rect ?P' ?N' ?C' ?ls') = true ]
+                             => is_var ls; is_var ls';
+                                let IH := fresh "IH" in
+                                revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *;
+                                [
+                                 | exfalso; discriminate | exfalso; discriminate
+                                 | specialize (IH ls');
+                                   generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
+                                intros
+                           | [ H : forall a b, ?R a b = true -> ?R' (?f a) (?g b) = true |- ?R' (?f _) (?g _) = true ] => apply H; clear H
+                           | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> ?R'' (?f a c) (?g b d) = true |- ?R'' (?f _ _) (?g _ _) = true ]
+                             => apply H; clear H
+                           | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> forall e f, ?R'' e f = true -> ?R''' (?F _ _ _) (?G _ _ _) = true |- ?R''' (?F _ _ _) (?G _ _ _) = true ]
+                             => apply H; clear H
+                           end ].
+
+          Axiom proof_admitted : False.
+          Notation admit := (match proof_admitted with end).
+
+          Lemma interp_related {t} (idc : ident t) : interp_is_related idc.
+          Proof.
+            destruct idc.
+            all: lazymatch goal with
+                 | [ |- context[ident.Z_cast] ] => apply interp_related_Z_cast
+                 | [ |- context[ident.Z_cast2] ] => apply interp_related_Z_cast2
+                 | [ |- context[ident.List_flat_map] ] => apply interp_related_List_flat_map
+                 | [ |- context[ident.List_partition] ] => apply interp_related_List_partition
+                 | _ => idtac
+                 end.
+            all: cbn [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some ZRange.ident.option.of_literal].
+            all: cbv [respectful_hetero option_map list_case].
+            all: intros.
+            all: destruct_head_hnf' prod.
+            all: destruct_head_hnf' option.
+            Time all: try solve [ non_arith_t ].
+            all: cbn [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by Option.bind ZRange.ident.option.to_literal ident.fancy.interp invert_Some ident.to_fancy ident.fancy.interp_with_wordmax] in *.
+            all: break_innermost_match; try reflexivity.
+            Time all: try solve [ non_arith_t ].
+            all: repeat first [ progress subst
+                              | progress inversion_prod
+                              | progress inversion_option
+                              | progress destruct_head'_and
+                              | progress cbn [ZRange.type.base.option.is_tighter_than lower upper fst snd Option.bind] in *
+                              | progress cbv [Definitions.Z.lnot_modulo Definitions.Z.add_with_carry] in *
+                              | handle_lt_le_t_step
+                              | simplify_ranges_t_step
+                              | discriminate
+                              | solve [ auto using ZRange.is_bounded_by_bool_Proper_if_sumbool_union ]
+                              | match goal with
+                                | [ H : ?x = ?x |- _ ] => clear H
+                                end
+                              | progress rewrite ?Z.mul_split_div, ?Z.mul_split_mod, ?Z.add_get_carry_full_div, ?Z.add_get_carry_full_mod, ?Z.add_with_get_carry_full_div, ?Z.add_with_get_carry_full_mod, ?Z.sub_get_borrow_full_div, ?Z.sub_get_borrow_full_mod, ?Z.sub_with_get_borrow_full_div, ?Z.sub_with_get_borrow_full_mod, ?Z.zselect_correct, ?Z.add_modulo_correct ].
+            all: clear cast_outside_of_range.
+            all: repeat match goal with
+                        | [ H : ?T |- _ ]
+                          => lazymatch T with
+                            | Z => clear H
+                            | zrange => clear H
+                            | _ = true => revert H
+                            | _ = false => revert H
+                            | _ => fail 10 T
+                            end
+                        end.
+            all: exact admit.
+          Qed.
+        End interp_related.
+      End option.
+    End ident.
+  End ZRange.
   Module Import partial.
     Import AbstractInterpretation.Compilers.partial.
     Import NewPipeline.UnderLets.Compilers.UnderLets.
@@ -73,7 +428,11 @@ Module Compilers.
               (bottom' : forall A, abstract_domain' A)
               (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v)
               (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
-              (ident_interp_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (ident_interp t idc)).
+              (ident_interp_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (ident_interp t idc))
+              (ident_interp_Proper' : forall t, Proper (eq ==> type.eqv) (ident_interp t))
+              (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop)
+              (abstraction_relation'_Proper : forall t, Proper (abstract_domain'_R t ==> eq ==> Basics.impl) (abstraction_relation' t))
+              (abstract_domain'_R_Reflexive : forall t, Reflexive (abstract_domain'_R t)).
       Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
       Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop
         := type.related_hetero (@abstraction_relation').
@@ -99,6 +458,14 @@ Module Compilers.
       Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract).
       Local Notation reify := (@reify base_type ident _ abstract_domain' annotate bottom').
       Local Notation reflect := (@reflect base_type ident _ abstract_domain' annotate bottom').
+      Local Notation interp := (@interp base_type ident var abstract_domain' annotate bottom' interp_ident).
+
+      Lemma bottom_related t v : @abstraction_relation t bottom v.
+      Proof using bottom'_related. cbv [abstraction_relation]; induction t; cbn; cbv [respectful_hetero]; eauto. Qed.
+
+      Lemma bottom_for_each_lhs_of_arrow_related t v : type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v.
+      Proof using bottom'_related. induction t; cbn; eauto using bottom_related. Qed.
+
       (*
       Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom').
       Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom').
@@ -145,7 +512,104 @@ Module Compilers.
            | type.base t => fun '(st, v) => st
            | type.arrow s d => fun '(st, v) => st
            end.
+ *)
+
+      Fixpoint related_bounded_value {t} : abstract_domain t -> value t -> type.interp base_interp t -> Prop
+        := match t return abstract_domain t -> value t -> type.interp base_interp t -> Prop with
+           | type.base t
+             => fun st '(e_st, e) v
+                => abstract_domain'_R t st e_st
+                   /\ expr.interp ident_interp e = v
+                   /\ abstraction_relation' t st v
+           | type.arrow s d
+             => fun st '(e_st, e) v
+                => (** XXX FIXME: DO WE NEED TO DO ANYTHING WITH e_st? *)
+                  forall st_s e_s v_s,
+                    @related_bounded_value s st_s e_s v_s
+                    -> @related_bounded_value d (st st_s) (UnderLets.interp ident_interp (e e_s)) (v v_s)
+           end.
+      Definition related_bounded_value_with_lets {t} : abstract_domain t -> value_with_lets t -> type.interp base_interp t -> Prop
+        := fun st e v => related_bounded_value st (UnderLets.interp ident_interp e) v.
+
+      Axiom proof_admitted : False.
+      Notation admit := (match proof_admitted with end).
 
+      Fixpoint interp_reify
+               is_let_bound {t} st e v b_in
+               (H : related_bounded_value st e v) {struct t}
+        : (forall arg1 arg2
+                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                  (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
+              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify is_let_bound t e b_in))) arg1
+              = type.app_curried v arg2)
+          /\ (forall arg1
+                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1)
+                     (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
+                 abstraction_relation'
+                   _
+                   (type.app_curried st b_in)
+                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify is_let_bound t e b_in))) arg1))
+      with interp_reflect
+             {t} st e v
+             (H_val : expr.interp ident_interp e == v)
+             (Hst : abstraction_relation st (expr.interp ident_interp e))
+             {struct t}
+           : related_bounded_value
+               st
+               (@reflect t e st)
+               v.
+      Proof using interp_annotate abstraction_relation'_Proper abstract_domain'_R_Reflexive bottom'_related.
+        all: destruct t as [t|s d];
+          [ clear interp_reify interp_reflect
+          | pose proof (fun is_let_bound => interp_reify is_let_bound s) as interp_reify_s;
+            pose proof (fun is_let_bound => interp_reify is_let_bound d) as interp_reify_d;
+            pose proof (interp_reflect s) as interp_reflect_s;
+            pose proof (interp_reflect d) as interp_reflect_d;
+            clear interp_reify interp_reflect ].
+        all: cbn [reify reflect]; fold (@reify) (@reflect).
+        all: repeat first [ reflexivity
+                          | progress eta_expand
+                          | progress cbn [related_bounded_value UnderLets.interp expr.interp type.final_codomain type.related] in *
+                          | progress fold (@type.interp)
+                          | progress destruct_head'_and
+                          | progress destruct_head_hnf' and
+                          | progress destruct_head_hnf' unit
+                          | progress split_and
+                          | rewrite UnderLets.interp_splice
+                          | rewrite UnderLets.interp_to_expr
+                          | rewrite interp_annotate
+                          | solve [ cbv [Proper respectful Basics.impl] in *; eauto ]
+                          | progress (repeat apply conj; intros * )
+                          | progress subst
+                          | progress cbn [type.app_curried type.and_for_each_lhs_of_arrow] in *
+                          | progress intros ].
+        replace (state_of_value e_s) with st_s.
+        eapply interp_reflect_d.
+        all: eauto.
+        all: cbn [expr.interp].
+        move e at bottom.
+        eapply H_val.
+        all: cbv [respectful] in *.
+        all: cbv [abstraction_relation] in *.
+        all: cbn [type.related_hetero] in *.
+        2:eapply Hst.
+        all: eauto.
+        rewrite type.related_iff_app_curried.
+        intros.
+        eapply H1.
+        eauto.
+        eauto.
+        apply bottom_for_each_lhs_of_arrow_related.
+        rewrite type.related_hetero_iff_app_curried.
+        intros.
+        replace x with (@bottom_for_each_lhs_of_arrow s).
+        eapply H2.
+        all: eauto using bottom_for_each_lhs_of_arrow_related.
+        exact admit.
+        exact admit.
+        exact admit.
+      Qed.
+      (*
       Fixpoint reify (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t)
         := match t return value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) with
            | type.base t
@@ -170,29 +634,49 @@ Module Compilers.
                            (rv <-- (@reify false s v bottom_for_each_lhs_of_arrow);
                               Base (@reflect d (e @ rv) (absf stv))%expr)))
               end%under_lets.
+       *)
 
-      (* N.B. Because the [App] case only looks at the second argument
-              of arrow-values, we are free to set the state of [Abs]
-              nodes to [bottom], because for any [Abs] nodes which are
-              actually applied (here and in places where we don't
-              rewrite), we just drop it. *)
-      Fixpoint interp {t} (e : @expr value_with_lets t) : value_with_lets t
-        := match e in expr.expr t return value_with_lets t with
-           | expr.Ident t idc => interp_ident _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*)
-           | expr.Var t v => v
-           | expr.Abs s d f => Base (bottom, fun x => @interp d (f (Base x)))
-           | expr.App s d f x
-             => (x' <-- @interp s x;
-                   f' <-- @interp (s -> d)%etype f;
-                   snd f' x')
-           | expr.LetIn (type.arrow _ _) B x f
-             => (x' <-- @interp _ x;
-                   @interp _ (f (Base x')))
-           | expr.LetIn (type.base A) B x f
-             => (x' <-- @interp _ x;
-                   x'' <-- reify true (* this forces a let-binder here *) x' tt;
-                   @interp _ (f (Base (reflect x'' (state_of_value x')))))
-           end%under_lets.
+      Context (interp_ident_Proper
+               : forall t idc,
+                  related_bounded_value (ident_extract t idc) (UnderLets.interp ident_interp (interp_ident t idc)) (ident_interp t idc)).
+
+      Lemma interp_interp
+            G {t} (e_st e1 e2 : expr t)
+            (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G
+                                     -> related_bounded_value_with_lets v1 v2 v3)
+            (Hwf : expr.wf3 G e_st e1 e2)
+        : related_bounded_value_with_lets
+            (extract' e_st)
+            (interp e1)
+            (expr.interp (@ident_interp) e2).
+      Proof using interp_ident_Proper interp_annotate abstraction_relation'_Proper.
+        cbv [related_bounded_value_with_lets] in *;
+          induction Hwf; cbn [extract' interp expr.interp related_bounded_value UnderLets.interp List.In] in *.
+        all: repeat first [ progress intros
+                          | progress subst
+                          | progress inversion_sigma
+                          | progress inversion_prod
+                          | progress destruct_head'_and
+                          | progress destruct_head'_or
+                          | progress eta_expand
+                          | progress cbn [UnderLets.interp List.In eq_rect fst snd projT1 projT2] in *
+                          | rewrite UnderLets.interp_splice
+                          | rewrite interp_annotate
+                          | solve [ cbv [Proper respectful Basics.impl] in *; eauto ]
+                          | progress specialize_by_assumption
+                          | progress cbv [Let_In extract'] in *
+                          | progress cbn [reify reflect state_of_value related_bounded_value] in *
+                          | match goal with
+                            | [ H : _ |- _ ] => tryif constr_eq H HG then fail else (apply H; clear H)
+                            end
+                          | break_innermost_match_step
+                          | apply conj
+                          | match goal with
+                            | [ H : _ = _ |- _ ] => rewrite H
+                            end ].
+      Qed.
+
+      (*
 
       Definition eval_with_bound' {t} (e : @expr value_with_lets t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)
@@ -255,15 +739,18 @@ Module Compilers.
               type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1
               = type.app_curried (expr.interp ident_interp e2) arg2)
           /\ (forall arg1
-                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
+                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1)
+                     (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
                  abstraction_relation'
                    _
                    (extract_gen e_st st)
                    (type.app_curried (expr.interp ident_interp (eval_with_bound' e1 st)) arg1)).
-      Proof using interp_annotate.
+      Proof using interp_annotate abstraction_relation'_Proper abstract_domain'_R_Reflexive bottom'_related interp_ident_Proper.
         cbv [extract_gen extract' eval_with_bound'].
         split; intros; rewrite UnderLets.interp_to_expr, UnderLets.interp_splice.
-      Admitted.
+        all: eapply interp_reify; eauto.
+        all: eapply interp_interp; eauto; wf_t.
+      Qed.
 
       Lemma interp_eta_expand_with_bound'
             {t} (e1 e2 : expr t)
@@ -273,12 +760,13 @@ Module Compilers.
             (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
             (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
           type.app_curried (expr.interp ident_interp (eta_expand_with_bound' e1 b_in)) arg1 = type.app_curried (expr.interp ident_interp e2) arg2.
-      Proof using interp_annotate.
+      Proof using interp_annotate ident_interp_Proper' bottom'_related abstraction_relation'_Proper abstract_domain'_R_Reflexive.
         cbv [eta_expand_with_bound'].
         intros; rewrite UnderLets.interp_to_expr.
-      Admitted.
-
-
+        eapply interp_reify; eauto.
+        eapply interp_reflect; eauto using bottom_related.
+        eapply @expr.wf_interp_Proper_gen; auto using Hwf.
+      Qed.
 
   (*
       Definition eval_with_bound' {t} (e : @expr value_with_lets t)
@@ -310,10 +798,16 @@ Module Compilers.
                 (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool)
                 (is_annotation : forall t, ident t -> bool)
                 (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop)
+                (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop)
+                (abstraction_relation'_Proper : forall t, Proper (abstract_domain'_R t ==> eq ==> Basics.impl) (abstraction_relation' t))
+                (abstract_domain'_R_Reflexive : forall t, Reflexive (abstract_domain'_R t))
+                (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v)
                 (cast_outside_of_range : zrange -> Z -> Z).
         Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation').
         Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
-        Context (interp_annotate_ident
+        Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R).
+        Context {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}
+                (interp_annotate_ident
                  : forall t st idc,
                     annotate_ident t st = Some idc
                     -> forall v, abstraction_relation' _ st v
@@ -331,15 +825,28 @@ Module Compilers.
                     is_annotation (type.base t -> type.base t) cst0 = true ->
                     annotate_ident t (abstract_interp_ident (type.base t -> type.base t) cst0 st) = Some cst1 ->
                     abstraction_relation' t st (ident_interp cst0 v) -> ident_interp cst1 v = ident_interp cst0 v)*)
-                (abstract_interp_ident_Proper
-                 : forall t idc, is_annotation _ idc = false -> type.related_hetero (@abstraction_relation') (abstract_interp_ident t idc) (ident_interp idc))
-                (fst_is_not_annotation : forall A B, is_annotation _ (@ident.fst A B) = false)
-                (snd_is_not_annotation : forall A B, is_annotation _ (@ident.snd A B) = false).
+                (abstract_interp_ident_Proper'
+                 : forall t idc, type.related_hetero (@abstraction_relation') (abstract_interp_ident t idc) (ident_interp idc))
+                (extract_list_state_related
+                 : forall t st ls v st' v',
+                    extract_list_state t st = Some ls
+                    -> abstraction_relation' _ st v
+                    -> List.In (st', v') (List.combine ls v)
+                    -> abstraction_relation' t st' v')
+                (extract_list_state_length_good
+                 : forall t st ls v,
+                    extract_list_state t st = Some ls
+                    -> abstraction_relation' _ st v
+                    -> length ls = length v).
 
         Local Notation update_annotation := (@ident.update_annotation _ abstract_domain' annotate_ident is_annotated_for).
         Local Notation annotate_with_ident := (@ident.annotate_with_ident _ abstract_domain' annotate_ident is_annotated_for).
         Local Notation annotate_base := (@ident.annotate_base _ abstract_domain' annotate_ident update_literal_with_state is_annotated_for).
         Local Notation annotate := (@ident.annotate _ abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+        Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for).
+        Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' abstract_domain'_R).
+        Local Notation reify := (@reify base.type ident _ abstract_domain' annotate bottom').
+        Local Notation reflect := (@reflect base.type ident _ abstract_domain' annotate bottom').
 
         Lemma interp_update_annotation t st e
               (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
@@ -381,33 +888,124 @@ Module Compilers.
               (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
           : expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate is_let_bound t st e))
             = expr.interp (@ident_interp) e.
-        Proof.
+        Proof using interp_update_literal_with_state interp_annotate_ident abstract_interp_ident_Proper' extract_list_state_related extract_list_state_length_good.
           induction t; cbn [annotate]; auto using interp_annotate_base.
           all: repeat first [ reflexivity
+                            | progress subst
+                            | progress inversion_option
+                            | progress inversion_prod
+                            | progress destruct_head'_ex
+                            | progress destruct_head'_and
                             | progress break_innermost_match
+                            | progress break_innermost_match_hyps
                             | progress expr.invert_subst
-                            | progress cbn [fst snd UnderLets.interp expr.interp ident_interp] in *
+                            | progress cbn [fst snd UnderLets.interp expr.interp ident_interp Nat.add] in *
                             | rewrite !UnderLets.interp_splice
                             | rewrite !UnderLets.interp_splice_list
                             | rewrite !List.map_map
                             | rewrite expr.interp_reify_list
+                            | rewrite nth_error_combine
                             | apply interp_annotate_with_ident; assumption
+                            | progress fold (@base.interp) in *
                             | progress intros
+                            | pose proof (@extract_list_state_length_good _ _ _ _ ltac:(eassumption) ltac:(eassumption)); clear extract_list_state_length_good
                             | match goal with
                               | [ H : context[expr.interp _ (reify_list _)] |- _ ] => rewrite expr.interp_reify_list in H
                               | [ H : abstraction_relation' (_ * _) _ (_, _) |- _ ]
-                                => pose proof (abstract_interp_ident_Proper _ ident.fst ltac:(auto) _ _ H);
-                                  pose proof (abstract_interp_ident_Proper _ ident.snd ltac:(auto)_ _ H);
+                                => pose proof (abstract_interp_ident_Proper' _ ident.fst _ _ H);
+                                  pose proof (abstract_interp_ident_Proper' _ ident.snd _ _ H);
                                   clear H
                               | [ H : context[_ = _] |- _ = _ ] => rewrite H by assumption
                               | [ |- List.map ?f (List.combine ?l1 ?l2) = List.map ?g ?l2 ]
                                 => transitivity (List.map g (List.map (@snd _ _) (List.combine l1 l2)));
                                   [ rewrite List.map_map; apply List.map_ext_in
                                   | rewrite map_snd_combine, List.firstn_all2; [ reflexivity | ] ]
+                              | [ Hls : extract_list_state ?t ?st = Some ?ls, He : abstraction_relation' _ ?st ?v |- abstraction_relation' _ _ _ ]
+                                => apply (fun st' v' => extract_list_state_related t st ls v st' v' Hls He)
+                              | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H
+                              | [ H : List.In _ (List.combine _ _) |- _ ] => apply List.In_nth_error in H
+                              | [ |- List.In _ (List.combine _ _) ] => eapply nth_error_In
+                              | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H'
+                              | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
+                              | [ H : List.nth_error _ _ = None |- _ ] => rewrite List.nth_error_None in H
+                              | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H)
+                              | [ |- context[length ?ls] ] => tryif is_var ls then fail else (progress autorewrite with distr_length)
+                              | [ H : List.nth_error ?ls ?n = Some _, H' : length ?ls <= ?n |- _ ]
+                                => apply nth_error_value_length in H; exfalso; clear -H H'; lia
+                              | [ H : List.nth_error ?l ?n = _, H' : List.nth_error ?l ?n' = _ |- _ ]
+                                => unify n n'; rewrite H in H'
+                              | [ Hls : extract_list_state ?t ?st = Some ?ls, He : abstraction_relation' _ ?st ?v |- _ ]
+                                => pose proof (fun st' v' => extract_list_state_related t st ls v st' v' Hls He); clear extract_list_state_related
+                              | [ IH : forall st e, _ -> expr.interp _ (UnderLets.interp _ (annotate _ _ _)) = _ |- List.map (fun x => expr.interp _ _) (List.combine _ _) = expr.interp _ _ ]
+                                => erewrite List.map_ext_in;
+                                   [
+                                   | intros; eta_expand; rewrite IH; cbn [expr.interp ident_interp ident.smart_Literal]; [ reflexivity | ] ]
+                              | [ H : abstraction_relation' _ ?st (List.map (expr.interp _) ?ls), H' : forall st' v', List.In _ (List.combine _ _) -> abstraction_relation' _ _ _, H'' : List.nth_error ?ls _ = Some ?e |- abstraction_relation' _ _ (expr.interp _ ?e) ]
+                                => apply H'
+                              | [ H : context[List.nth_error (List.seq _ _) _] |- _ ] => rewrite nth_error_seq in H
+                              end
+                            | apply Nat.eq_le_incl
+                            | rewrite <- List.map_map with (f:=fst), map_fst_combine
+                            | rewrite Lists.List.firstn_all2 by distr_length
+                            | apply map_nth_default_seq
+                            | match goal with
+                              | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] => apply H; clear H
+                              | [ H : forall st' v', List.In _ (List.combine _ _) -> abstraction_relation' _ _ _ |- abstraction_relation' _ _ _ ]
+                                => apply H; clear H; cbv [List.nth_default]
+                              | [ |- None = Some _ ] => exfalso; lia
                               end ].
-          apply IHt.
-        Admitted.
+        Qed.
+
+        Lemma interp_ident_Proper_not_nth_default t idc
+          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (Base (reflect (expr.Ident idc) (abstract_interp_ident _ idc)))) (ident_interp idc).
+        Proof using abstract_domain'_R_Reflexive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related interp_annotate_ident interp_update_literal_with_state.
+          cbn [UnderLets.interp].
+          eapply interp_reflect;
+            try first [ apply ident.gen_interp_Proper
+                      | apply abstract_interp_ident_Proper'
+                      | apply interp_annotate ];
+            eauto.
+        Qed.
+
+        Lemma interp_ident_Proper_nth_default T (idc:=@ident.List_nth_default T)
+          : related_bounded_value (abstract_interp_ident _ idc) (UnderLets.interp (@ident_interp) (interp_ident idc)) (ident_interp idc).
+        Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related interp_annotate_ident interp_update_literal_with_state.
+          subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value abstract_domain value].
+          cbv [abstract_domain]; cbn [type.interp bottom_for_each_lhs_of_arrow state_of_value fst snd].
+          repeat first [ progress intros
+                       | progress cbn [UnderLets.interp fst snd expr.interp ident_interp] in *
+                       | progress destruct_head'_prod
+                       | progress destruct_head'_and
+                       | progress subst
+                       | progress eta_expand
+                       | rewrite UnderLets.interp_splice
+                       | progress expr.invert_subst
+                       | break_innermost_match_step
+                       | progress cbn [type.interp base.interp base.base_interp] in *
+                       | rewrite interp_annotate
+                       | solve [ cbv [Proper respectful Basics.impl] in *; eauto ]
+                       | split; [ apply (@abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl) | ]
+                       | split; [ reflexivity | ]
+                       | apply (@abstract_interp_ident_Proper' _ (@ident.List_nth_default T))
+                       | apply conj
+                       | rewrite map_nth_default_always
+                       | match goal with
+                         | [ H : context[expr.interp _ (UnderLets.interp _ (annotate _ _ _))] |- _ ]
+                           => rewrite interp_annotate in H
+                         | [ H : context[expr.interp _ (reify_list _)] |- _ ]
+                           => rewrite expr.interp_reify_list in H
+                         | [ H : _ = reify_list _ |- _ ] => apply (f_equal (expr.interp (@ident_interp))) in H
+                         | [ H : expr.interp _ ?x = _ |- context[expr.interp _ ?x] ] => rewrite H
+                         end ].
+        Qed.
 
+        Lemma interp_ident_Proper t idc
+          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (interp_ident idc)) (ident_interp idc).
+        Proof.
+          pose idc as idc'.
+          destruct idc; first [ refine (@interp_ident_Proper_not_nth_default _ idc')
+                              | refine (@interp_ident_Proper_nth_default _) ].
+        Qed.
 
         (*Context {annotate_ident_Proper : forall t, Proper (abstract_domain'_R t ==> eq) (annotate_ident t)}
                 {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}
@@ -430,12 +1028,13 @@ Module Compilers.
                 type.app_curried (expr.interp (@ident_interp) (eval_with_bound e1 st)) arg1
                 = type.app_curried (expr.interp (@ident_interp) e2) arg2)
             /\ (forall arg1
-                       (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
+                       (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1)
+                       (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
                    abstraction_relation'
                      _
                      (extract e_st st)
                      (type.app_curried (expr.interp (@ident_interp) (eval_with_bound e1 st)) arg1)).
-        Proof. cbv [extract eval_with_bound]; apply interp_eval_with_bound'; auto using interp_annotate. Qed.
+        Proof. cbv [extract eval_with_bound]; apply @interp_eval_with_bound' with (abstract_domain'_R:=abstract_domain'_R); auto using interp_annotate, interp_ident_Proper. Qed.
 
         Lemma interp_eta_expand_with_bound
               {t} (e1 e2 : expr t)
@@ -445,7 +1044,7 @@ Module Compilers.
                    (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                    (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
             type.app_curried (expr.interp (@ident_interp) (eta_expand_with_bound e1 b_in)) arg1 = type.app_curried (expr.interp (@ident_interp) e2) arg2.
-        Proof. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using interp_annotate. Qed.
+        Proof. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using interp_annotate, ident.gen_interp_Proper. Qed.
 
 (*
         Definition eval {t} (e : @expr value_with_lets t) : @expr var t
@@ -507,12 +1106,8 @@ Module Compilers.
       Proof. destruct idc; cbn [is_annotation]; try discriminate; eauto. Qed.
 
       Lemma abstract_interp_ident_related cast_outside_of_range {t} (idc : ident t)
-            (not_cast : is_annotation _ idc = false)
         : type.related_hetero (@abstraction_relation') (@abstract_interp_ident t idc) (@ident.gen_interp cast_outside_of_range _ idc).
-      Proof.
-        destruct idc; cbv [abstract_interp_ident abstraction_relation']; cbn [is_annotation] in *; try discriminate.
-        all: cbv [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some].
-      Admitted.
+      Proof. apply ZRange.ident.option.interp_related. Qed.
 
       Lemma interp_update_literal_with_state {t : base.type.base} st v
         : @abstraction_relation' t st v -> @update_literal_with_state t st v = v.
@@ -576,16 +1171,18 @@ Module Compilers.
               type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1
               = type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e2) arg2)
           /\ (forall arg1
-                  (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
+                     (Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
+                     (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
                  abstraction_relation'
                    (extract e_st st)
                    (type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) (eval_with_bound e1 st)) arg1)).
       Proof using Type.
         cbv [eval_with_bound]; split;
           [ intros arg1 arg2 Harg12 Harg1
-          | intros arg1 Harg1 ].
+          | intros arg1 Harg11 Harg1 ].
         all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ].
-        all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation'); eauto.
+        all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom with typeclass_instances.
+        all: intros; eapply extract_list_state_related; eassumption.
       Qed.
 
       Lemma interp_eta_expand_with_bound
@@ -599,7 +1196,8 @@ Module Compilers.
       Proof.
         cbv [partial.eta_expand_with_bound]; intros arg1 arg2 Harg12 Harg1.
         eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1.
-        { apply ident.interp_eta_expand_with_bound with (is_annotation:=is_annotation) (abstraction_relation':=@abstraction_relation'); eauto. }
+        { apply ident.interp_eta_expand_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom with typeclass_instances.
+          all: intros; eapply extract_list_state_related; eassumption. }
         { apply ZRange.type.option.is_bounded_by_impl_related_hetero. }
       Qed.
 
@@ -614,6 +1212,7 @@ Module Compilers.
               type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (EvalWithBound e st)) arg1
               = type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) e) arg2)
           /\ (forall arg1
+                     (Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
                      (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
                  abstraction_relation'
                    (Extract e st)
@@ -819,7 +1418,8 @@ Module Compilers.
         (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
         {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R _ _ (fun _ => eq))) b_in}
     : forall arg1
-        (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
+             (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1)
+             (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
       ZRange.type.base.option.is_bounded_by
         (partial.Extract E b_in)
         (type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1)