From 6b7d2c90c33ef2817746453a86057fc273e3c1bf Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Aug 2018 19:15:33 -0400 Subject: Add more operation-specific proofs --- .../NewPipeline/AbstractInterpretationProofs.v | 363 +----------------- .../AbstractInterpretationZRangeProofs.v | 422 +++++++++++++++++++++ 2 files changed, 426 insertions(+), 359 deletions(-) create mode 100644 src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v (limited to 'src') diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index ebc60d888..ecc3dcc7b 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -5,6 +5,7 @@ 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.ZRange.SplitBounds. Require Import Crypto.Util.Sum. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. @@ -20,6 +21,7 @@ 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.ZUtil.Tactics.ReplaceNegWithPos. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. @@ -34,6 +36,7 @@ Require Import Crypto.Experiments.NewPipeline.LanguageWf. Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs. Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. Require Import Crypto.Experiments.NewPipeline.AbstractInterpretationWf. +Require Import Crypto.Experiments.NewPipeline.AbstractInterpretationZRangeProofs. Module Compilers. Import Language.Compilers. @@ -43,6 +46,7 @@ Module Compilers. Import LanguageWf.Compilers. Import UnderLetsProofs.Compilers. Import AbstractInterpretationWf.Compilers. + Import AbstractInterpretationZRangeProofs.Compilers. Import AbstractInterpretationWf.Compilers.partial. Import invert_expr. @@ -53,365 +57,6 @@ Module Compilers. Local Notation related_bounded := (@type.related_hetero3 _ _ _ _ (fun t b v1 v2 => related_bounded' b v1 v2)). - 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) - : ZRange.type.option.is_bounded_by x v = true - -> type.related_hetero (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v. - Proof. induction t; cbn in *; intuition congruence. Qed. - End option. - End type. - - 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. diff --git a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v new file mode 100644 index 000000000..5998a95c5 --- /dev/null +++ b/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v @@ -0,0 +1,422 @@ +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +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.ZRange.SplitBounds. +Require Import Crypto.Util.Sum. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Prod. +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.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation. + +Module Compilers. + Import AbstractInterpretation.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) + : ZRange.type.option.is_bounded_by x v = true + -> type.related_hetero (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v. + Proof. induction t; cbn in *; intuition congruence. Qed. + End option. + End type. + + 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[Z.ltb ?a ?b = true] ] => rewrite !Z.ltb_lt + | [ |- 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[Z.ltb ?a ?b = true] |- _ ] => rewrite !Z.ltb_lt 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 handle_mod_bounds_t_step_fast := + first [ match goal with + | [ |- (0 <= _ mod _)%Z ] => apply Z.mod_pos_bound + | [ |- (_ mod ?m < ?m)%Z ] => apply Z.mod_pos_bound + | [ |- (?x mod ?m <= ?m - 1)%Z ] => cut (x mod m < m)%Z; [ clear; lia | ] + 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 + | handle_mod_bounds_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 ]. + + Local Lemma le_sub_1_eq x y : ((x <= y - 1) <-> (x < y))%Z. + Proof. lia. Qed. + + Local Lemma le_add_1_eq x y : ((x + 1 <= y) <-> (x < y))%Z. + Proof. lia. Qed. + + 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, Z.mod_pos_bound, Z.mod_neg_bound with zarith ] + | rewrite ZRange.is_bounded_by_bool_opp + | progress autorewrite with zsimplify_const + | rewrite le_sub_1_eq + | rewrite le_add_1_eq + | match goal with + | [ H : ?x = ?x |- _ ] => clear H + | [ |- andb (is_bounded_by_bool (_ mod ?m) (fst (Operations.ZRange.split_bounds _ ?m))) + (is_bounded_by_bool (_ / ?m) (snd (Operations.ZRange.split_bounds _ ?m))) = true ] + => apply ZRange.is_bounded_by_bool_split_bounds + | [ |- is_bounded_by_bool (_ mod _) r[_ ~> _] = true ] => cbv [is_bounded_by_bool]; rewrite Bool.andb_true_iff + end + | progress Z.ltb_to_lt + | 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. +End Compilers. -- cgit v1.2.3