Skip to content

Commit 8d5e487

Browse files
JasonGrossJasonGross
committed
Factor ZRange Proper proof
For #1761
1 parent 1ac47ca commit 8d5e487

2 files changed

Lines changed: 67 additions & 33 deletions

File tree

‎src/AbstractInterpretation/Wf.v‎

Lines changed: 4 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -25,14 +25,17 @@ Require Import Rewriter.Language.Inversion.
2525
Require Import Crypto.Language.InversionExtra.
2626
Require Import Rewriter.Language.Wf.
2727
Require Import Rewriter.Language.UnderLetsProofs.
28+
Require Import Rewriter.Util.Decidable.
2829
Require Import Crypto.AbstractInterpretation.AbstractInterpretation.
30+
Require Import Crypto.AbstractInterpretation.ZRangeCommonProofs.
2931
Import Coq.Lists.List.
3032

3133
Import EqNotations.
3234
Module Compilers.
3335
Import Language.Compilers.
3436
Import UnderLets.Compilers.
3537
Import AbstractInterpretation.Compilers.
38+
Import AbstractInterpretation.ZRangeCommonProofs.Compilers.
3639
Import Language.Inversion.Compilers.
3740
Import Language.InversionExtra.Compilers.
3841
Import Language.Wf.Compilers.
@@ -852,39 +855,7 @@ Module Compilers.
852855

853856
Global Instance abstract_interp_ident_Proper {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t}
854857
: Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident assume_cast_truncates t).
855-
Proof using Type.
856-
cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc;
857-
repeat first [ reflexivity
858-
| progress subst
859-
| progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Crypto.Util.Option.bind] in *
860-
| progress cbv [Crypto.Util.Option.bind]
861-
| intro
862-
| progress destruct_head'_prod
863-
| progress destruct_head'_bool
864-
| progress destruct_head' option
865-
| progress inversion_option
866-
| discriminate
867-
| solve [ eauto ]
868-
| apply NatUtil.nat_rect_Proper_nondep
869-
| apply ListUtil.list_rect_Proper
870-
| apply ListUtil.list_rect_arrow_Proper
871-
| apply ListUtil.list_case_Proper
872-
| apply ListUtil.pointwise_map
873-
| apply ListUtil.fold_right_Proper
874-
| apply ListUtil.update_nth_Proper
875-
| apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
876-
| cbn; apply (f_equal (@Some _))
877-
| progress cbn [ZRange.ident.option.interp]
878-
| progress cbv [zrange_rect]
879-
| apply (f_equal2 pair)
880-
| break_innermost_match_step
881-
| match goal with
882-
| [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
883-
| [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
884-
| [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
885-
=> specialize (H y); rewrite H1, H2 in H
886-
end ].
887-
Qed.
858+
Proof using Type. apply ZRange.ident.option.interp_Proper. Qed.
888859

889860
Global Instance extract_list_state_Proper {t}
890861
: Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t)))

‎src/AbstractInterpretation/ZRangeCommonProofs.v‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
(* Proofs shared by Wf and Proofs *)
2+
Require Import Coq.Classes.Morphisms.
3+
Require Import Coq.Relations.Relations.
4+
Require Import Crypto.Util.ZRange.
5+
Require Import Crypto.Util.Option.
6+
Require Import Crypto.Util.ListUtil.
7+
Require Import Crypto.Util.ListUtil.FoldBool.
8+
Require Import Crypto.Util.NatUtil.
9+
Require Import Crypto.Util.ZUtil.Morphisms.
10+
Require Import Crypto.Util.Tactics.BreakMatch.
11+
Require Import Crypto.Util.Tactics.DestructHead.
12+
Require Import Crypto.AbstractInterpretation.ZRange.
13+
14+
Module Compilers.
15+
Import AbstractInterpretation.ZRange.Compilers.
16+
Export ZRange.Settings.
17+
18+
Module ZRange.
19+
Module ident.
20+
Module option.
21+
Section interp_related.
22+
Context {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
23+
(assume_cast_truncates : bool).
24+
Global Instance interp_Proper {t} : Proper (eq ==> @type.eqv t) (ZRange.ident.option.interp assume_cast_truncates).
25+
Proof using Type.
26+
intros idc idc' ?; subst idc'.
27+
cbv [type.related respectful type.interp]; destruct idc;
28+
repeat first [ reflexivity
29+
| progress subst
30+
| progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Crypto.Util.Option.bind] in *
31+
| progress cbv [Crypto.Util.Option.bind]
32+
| intro
33+
| progress destruct_head'_prod
34+
| progress destruct_head'_bool
35+
| progress destruct_head' option
36+
| progress inversion_option
37+
| discriminate
38+
| solve [ eauto ]
39+
| apply NatUtil.nat_rect_Proper_nondep
40+
| apply ListUtil.list_rect_Proper
41+
| apply ListUtil.list_rect_arrow_Proper
42+
| apply ListUtil.list_case_Proper
43+
| apply ListUtil.pointwise_map
44+
| apply ListUtil.fold_right_Proper
45+
| apply ListUtil.update_nth_Proper
46+
| apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
47+
| cbn; apply (f_equal (@Some _))
48+
| progress cbn [ZRange.ident.option.interp]
49+
| progress cbv [zrange_rect]
50+
| apply (f_equal2 pair)
51+
| break_innermost_match_step
52+
| match goal with
53+
| [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
54+
| [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
55+
| [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
56+
=> specialize (H y); rewrite H1, H2 in H
57+
end ].
58+
Qed.
59+
End interp_related.
60+
End option.
61+
End ident.
62+
End ZRange.
63+
End Compilers.

0 commit comments

Comments
 (0)