From 51d25ab7feeaca959d35fbd4fa905f8ce003e07b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 16 May 2021 11:35:31 +0100 Subject: Minimise the proof a bit --- src/hls/RTLPargenproof.v | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 8ecaba2..9cfee3a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -284,25 +284,19 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl. - { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } - { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). } - { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). - eapply eval_builtin_args_eq. eapply REG. - eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. - eauto. - (econstructor; eauto with rtlgp). - intros. - unfold regmap_setres. destruct res. - destruct (Pos.eq_dec x0 x); subst. - repeat rewrite Regmap.gss; auto. - repeat rewrite Regmap.gso; auto. - eapply REG. eapply REG. + induction 1; repeat semantics_simpl; + try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. + { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + eapply eval_builtin_args_eq. eapply REG. + eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. + eauto. + intros. + unfold regmap_setres. destruct res. + destruct (Pos.eq_dec x0 x); subst. + repeat rewrite Regmap.gss; auto. + repeat rewrite Regmap.gso; auto. + eapply REG. eapply REG. } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } - { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). } { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. constructor; eauto. -- cgit