diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-16 12:43:57 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-16 12:43:57 +0000 |
| commit | 08638488c2fb68b6d1b6992f46b03963e96315cc (patch) | |
| tree | b54c3378d7cb93110374796e1e43914fe2ba21b3 | |
| parent | 9be7092870eeaf2024768acb15a0eff02de61c91 (diff) | |
| download | vericert-08638488c2fb68b6d1b6992f46b03963e96315cc.tar.gz vericert-08638488c2fb68b6d1b6992f46b03963e96315cc.zip | |
Greatly simplify proof
| -rw-r--r-- | src/hls/Memorygen.v | 67 |
1 files changed, 23 insertions, 44 deletions
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 8c6c2a3..e7a1138 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -479,50 +479,29 @@ Lemma transf_fold_not_changed : c!i = Some c_s -> d'!i = Some d_s /\ c'!i = Some c_s). Proof. - induction l as [| a l IHl]; crush. - - repeat match goal with H: context[a :: l] |- _ => inv H end. - destruct (Pos.eq_dec a i); subst; - remember (fold_right (transf_maps state ram) (n, d, c) l); - repeat destruct p; symmetry in Heqp. - match goal with - | H: forall e1 e2 r, _ <> Vnonblock (Vvari _ _) _ |- _ ! _ = Some _ => - let H13 := fresh "H" in - pose proof H as H13; eapply IHl in H13; eauto; inv H13 - end. - match goal with - | [ H: forall e1 e2 r, _ <> Vnonblock (Vvari _ _) _ |- _] => - let H12 := fresh "H" in - pose proof H as H12; eapply transf_not_changed in H12; eauto - end. - match goal with - | [ H: transf_maps _ _ _ _ = _, H2: transf_maps _ _ _ _ = _ |- _ ] => - rewrite H in H2; inv H2; auto - end. - match goal with - | H: transf_maps _ _ _ _ = _ |- _ => - let H12 := fresh "H" in - pose proof H as H12; eapply transf_not_changed_neq in H12; eauto; inv H12; eauto - end; - match goal with - | H: fold_right _ _ _ = _ |- _ ! _ = Some _ => - eapply IHl in H; auto; inv H; eauto - | H: fold_right _ _ _ = _ |- _ <> _ => - apply transf_fold_gteq in H; lia - end. - - inv H0; inv H1; - destruct (Pos.eq_dec a i); subst; - remember (fold_right (transf_maps state ram) (n, d, c) l); - repeat destruct p; symmetry in Heqp. - pose proof H3 as H12. - pose proof H3 as H13. - eapply IHl in H13; eauto. - inv H13. eapply transf_not_changed in H12; eauto. - rewrite H12 in H. inv H. auto. - pose proof H as H12. - eapply transf_not_changed_neq in H12; eauto. inv H12. - eauto. eapply IHl in Heqp; auto. inv Heqp. eauto. auto. auto. eauto. - eapply IHl in Heqp; auto. inv Heqp. eauto. auto. auto. eauto. - apply transf_fold_gteq in Heqp. lia. + induction l as [| a l IHl]; crush; + repeat match goal with H: context[a :: l] |- _ => inv H end; + destruct (Pos.eq_dec a i); subst; + remember (fold_right (transf_maps state ram) (n, d, c) l); + repeat destruct p; symmetry in Heqp; + repeat match goal with + | H: forall e1 e2 r, _ <> Vnonblock (Vvari _ _) _ |- _ => + let H12 := fresh "H" in + let H13 := fresh "H" in + pose proof H as H12; + learn H as H13; + eapply IHl in H13; eauto; inv H13; + eapply transf_not_changed in H12; eauto + | [ H: transf_maps _ _ _ _ = _, H2: transf_maps _ _ _ _ = _ |- _ ] => + rewrite H in H2; inv H2; solve [auto] + | Hneq: a <> ?i, H: transf_maps _ _ _ _ = _ |- _ => + let H12 := fresh "H" in + learn H as H12; eapply transf_not_changed_neq in H12; inv H12; eauto + | Hneq: a <> ?i, H: fold_right _ _ _ = _ |- _ ! _ = Some _ => + eapply IHl in H; inv H; solve [eauto] + | Hneq: a <> ?i, H: fold_right _ _ _ = _ |- _ <> _ => + apply transf_fold_gteq in H; lia + end. Qed. Lemma transf_store : |