From c10635f9e6890a6171c5c1cc8eb6e3298d2006b1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 29 May 2023 16:13:24 +0100 Subject: Prove more admitted theorems --- src/hls/GiblePargenproofForward.v | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'src/hls/GiblePargenproofForward.v') diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 1051fe5..d340477 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -177,7 +177,7 @@ all be evaluable. destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *. destruct (peq x res); subst. * rewrite forest_reg_gss in *. rewrite Regmap.gss in *. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv PRED; eassumption. eapply sem_pred_expr_app_predicated; [| |eauto]. replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto. eapply sem_update_Iop; eauto. cbn in *. @@ -215,7 +215,7 @@ all be evaluable. destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *. destruct (peq x res); subst. * rewrite forest_reg_gss in *. rewrite Regmap.gss in *. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv PRED; eassumption. eapply sem_pred_expr_app_predicated; [| |eauto]. replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto. eapply sem_update_Iload; eauto. @@ -260,7 +260,7 @@ all be evaluable. apply exists_sem_pred in H. inversion_clear H as [r' [HNE HVAL]]. exploit sem_merge_list. eapply SEM2. instantiate (2 := args). intro HSPE. eapply sem_pred_expr_ident2 in HSPE. inversion_clear HSPE as [l_ [HSPE1 HSPE2]]. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv PRED; eassumption. eapply sem_pred_expr_app_predicated. eapply sem_pred_expr_seq_app_val; [solve [eauto]| |]. eapply sem_pred_expr_seq_app; [solve [eauto]|]. @@ -473,7 +473,7 @@ all be evaluable. constructor. * constructor. intros. destruct (peq x res); subst. rewrite forest_reg_gss. cbn. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv H3; inv H9; eassumption. eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto. inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto. @@ -486,7 +486,7 @@ all be evaluable. constructor. * constructor. intros. destruct (peq x dst); subst. rewrite forest_reg_gss. cbn. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv H3; inv H9; eassumption. eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto. inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto. @@ -499,7 +499,7 @@ all be evaluable. constructor. * constructor. intros. rewrite forest_reg_gso by discriminate. inv H3. inv H8. auto. * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto. - * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto. + * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto. inv H3; inv H9; eassumption. eapply sem_pred_expr_app_predicated_false. inv H3. auto. inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto. * inv H3. auto. @@ -528,7 +528,7 @@ all be evaluable. * constructor. inv H8. auto. * constructor. intros. inv H9. eauto. * auto. - * cbn. eapply sem_pred_expr_prune_predicated; [|eauto]. + * cbn. eapply sem_pred_expr_prune_predicated; [| |eauto]. inv H9; eassumption. eapply sem_pred_expr_app_predicated_false; auto. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto. @@ -548,7 +548,7 @@ all be evaluable. constructor. * constructor. intros. destruct (peq x r); subst. rewrite forest_reg_gss. cbn. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv H1; inv H8; eassumption. eapply sem_pred_expr_app_predicated_false. inv H1. inv H7. auto. inv H1. inv H8. eauto. rewrite eval_predf_Pand. rewrite H. eauto with bool. @@ -561,7 +561,7 @@ all be evaluable. constructor. * constructor. intros. destruct (peq x r); subst. rewrite forest_reg_gss. cbn. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv H1; inv H8; eassumption. eapply sem_pred_expr_app_predicated_false. inv H1. inv H7. auto. inv H1. inv H8. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool. @@ -574,7 +574,7 @@ all be evaluable. constructor. * constructor. intros. rewrite forest_reg_gso by discriminate. inv H1. inv H7. auto. * constructor; intros. rewrite forest_reg_pred. inv H1. inv H8. auto. - * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto. + * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto. inv H1; inv H8; eassumption. eapply sem_pred_expr_app_predicated_false. inv H1. auto. inv H1. inv H8. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool. * inv H1. auto. @@ -604,7 +604,7 @@ all be evaluable. * constructor. inv H7. auto. * constructor. intros. inv H8. eauto. * auto. - * cbn. eapply sem_pred_expr_prune_predicated; [|eauto]. + * cbn. eapply sem_pred_expr_prune_predicated; [| |eauto]. inv H8; eassumption. eapply sem_pred_expr_app_predicated_false; auto. inv H8. eauto. rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool. @@ -675,7 +675,7 @@ all be evaluable. constructor. inv H9. intros. cbn. eauto. inv H10. constructor; intros. eauto. cbn. - eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_prune_predicated; eauto. inv H10; eassumption. eapply sem_pred_expr_app_predicated. constructor. constructor. constructor. inv H10. eauto. cbn -[eval_predf] in *. -- cgit