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/common/NonEmpty.v | 21 +++++++ src/hls/AbstrSemIdent.v | 126 ++++++++++++++++++++++++++++++++------ src/hls/Gible.v | 10 +++ src/hls/GiblePargenproofEquiv.v | 30 ++++----- src/hls/GiblePargenproofForward.v | 24 ++++---- src/hls/Predicate.v | 26 +++++++- 6 files changed, 190 insertions(+), 47 deletions(-) diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 2c3ae94..7b10ee0 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -305,3 +305,24 @@ Proof. + constructor. eapply H. constructor; tauto. eapply IHl. intros. eapply H. constructor; tauto. Qed. + +Lemma filter_None : + forall A f (x: non_empty A), + filter f x = None -> + Forall (fun x => f x = false) x. +Proof. + induction x; cbn; intros. + - constructor. destruct_match; now auto. + - constructor. destruct_match; auto. destruct_match; try discriminate. + destruct_match; eauto. now destruct_match. +Qed. + +Lemma In_map : + forall A B (f: A -> B) n (x: A), + In x n -> + In (f x) (map f n). +Proof. + induction n; inversion 1; subst; cbn in *. + - constructor. + - clear H. inv H1; intuition (constructor; auto). +Qed. diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index 1499ea9..909a1a1 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -125,21 +125,74 @@ Proof. Qed. Lemma sem_pred_expr_prune_predicated : - forall f_p y x v, + forall f_p ps x y v, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> sem_pred_expr f_p a_sem ctx x v -> prune_predicated x = Some y -> sem_pred_expr f_p a_sem ctx y v. Proof. - intros * SEM PRUNE. unfold prune_predicated in *. Admitted. + induction x. + - cbn in *; intros * HPREDSEM **. repeat destr. + inv H0. inv H. constructor; auto; cbn in *. + eapply sem_pexpr_eval; [eassumption|]. + eapply sem_pexpr_eval_inv in H1; [|eassumption]. + now rewrite eval_predf_deep_simplify. + - cbn in *; intros * HPREDSEM **. destruct_match; repeat destr. + 2: { clear Heqb. inv H; cbn in *. + eapply sem_pexpr_eval_inv in H4; [|eassumption]. + rewrite <- 2 eval_predf_deep_simplify with (peq:=peq) in H4. + setoid_rewrite Heqp in H4. now cbn in H4. + eauto. } + destruct_match. + + inv H0. inv H. + * constructor; auto. eapply sem_pexpr_eval; [eassumption|]. + eapply sem_pexpr_eval_inv in H3; [|eassumption]. + now rewrite eval_predf_deep_simplify. + * eapply sem_pred_expr_cons_false; eauto. + eapply sem_pexpr_eval; [eassumption|]. + eapply sem_pexpr_eval_inv in H3; [|eassumption]. + now rewrite eval_predf_deep_simplify. + + inv H0. inv H. + * constructor; auto. + eapply sem_pexpr_eval; [eassumption|]. + eapply sem_pexpr_eval_inv in H3; [|eassumption]. + now rewrite eval_predf_deep_simplify. + * cbn in *. exploit NE.filter_None. eapply Heqo. cbn. intros. + exploit sem_pred_expr_in_true. eapply H5. intros [p_true [e_true [HIN [HSEMP HASEM]]]]. + pose proof (NE.In_map _ _ (fun x : Predicate.pred_op * A => (deep_simplify peq (fst x), snd x)) _ _ HIN). + cbn in *. eapply NE.Forall_forall in H; [|eassumption]. + destr. clear H. cbn in *. + eapply sem_pexpr_eval_inv in HSEMP; [|eassumption]. + rewrite <- 2 eval_predf_deep_simplify with (peq:=peq) in HSEMP. + setoid_rewrite Heqp in HSEMP. now cbn in HSEMP. +Qed. Lemma sem_pred_expr_prune_predicated2 : - forall f_p y x v, + forall f_p ps x y v, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> sem_pred_expr f_p a_sem ctx y v -> prune_predicated x = Some y -> sem_pred_expr f_p a_sem ctx x v. Proof. - intros * SEM PRUNE. unfold prune_predicated in *. - Admitted. + induction x; intros * SEMPRED SEM PRUNE. unfold prune_predicated in *. + - cbn in *. destr. inv PRUNE. inv SEM. + destruct a; constructor; auto. + eapply sem_pexpr_eval_inv in H2; eauto. + eapply sem_pexpr_eval; eauto. + rewrite eval_predf_deep_simplify in H2; auto. + - cbn in *. destruct_match. + 2: { destr. destruct a. eapply sem_pred_expr_cons_false; eauto. + eapply sem_pexpr_eval; eauto. + rewrite <- 2 eval_predf_deep_simplify with (peq:=peq). now setoid_rewrite Heqp. + } + destruct_match. + + inv PRUNE. destruct a; inv SEM; [constructor|eapply sem_pred_expr_cons_false]; eauto; + eapply sem_pexpr_eval; eauto; rewrite <- eval_predf_deep_simplify with (peq:=peq); + eapply sem_pexpr_eval_inv in H4; eauto. + + inv PRUNE. inv SEM. destruct a. constructor; auto. + eapply sem_pexpr_eval; eauto. eapply sem_pexpr_eval_inv in H2; eauto. + now rewrite <- eval_predf_deep_simplify with (peq:=peq). +Qed. Lemma sem_pred_expr_pred_ret : forall (i: A) ps, @@ -181,6 +234,23 @@ Proof. intros. eapply H0. constructor; tauto. Qed. +Lemma sem_pred_expr_NEapp6 : + forall f_p a b v ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + (forall x, NE.In x a -> eval_predf ps (fst x) = false) -> + sem_pred_expr f_p a_sem ctx (NE.app a b) v -> + sem_pred_expr f_p a_sem ctx b v. +Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + inv H1; auto. eapply H0 in IN. eapply sem_pexpr_eval_inv in H5; eauto. + now setoid_rewrite H5 in IN. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + eapply H0 in H2. destruct a. inv H1. + + eapply sem_pexpr_eval_inv in H8; eauto. now setoid_rewrite H8 in H2. + + eapply IHa; eauto. intros. eapply H0. constructor; tauto. +Qed. + Lemma sem_pred_expr_NEapp3 : forall f_p ctx a b v, (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) -> @@ -283,6 +353,29 @@ Proof. eapply sem_pexpr_eval; eauto. eauto. Qed. +Lemma sem_pred_expr_map_Pand2 : + forall f_p ps x v p, + (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + eval_predf ps p = true -> + sem_pred_expr f_p a_sem ctx + (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v -> + sem_pred_expr f_p a_sem ctx x v. +Proof. + induction x; crush. + - inv H1. destruct a; constructor; auto. eapply sem_pexpr_eval; eauto. + eapply sem_pexpr_eval_inv in H5; eauto. rewrite eval_predf_Pand in H5. + now rewrite H0 in H5. + - inv H1. + + destruct a; constructor; auto. eapply sem_pexpr_eval; eauto. + eapply sem_pexpr_eval_inv in H7; eauto. rewrite eval_predf_Pand in H7. + now rewrite H0 in H7. + + destruct a; eapply sem_pred_expr_cons_false; eauto. + eapply sem_pexpr_eval; eauto. + eapply sem_pexpr_eval_inv in H7; eauto. + rewrite eval_predf_Pand in H7. + now rewrite H0 in H7. +Qed. + Lemma sem_pred_expr_app_predicated : forall f_p y x v p ps, sem_pred_expr f_p a_sem ctx x v -> @@ -303,7 +396,13 @@ Lemma sem_pred_expr_app_predicated2 : (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> eval_predf ps p = true -> sem_pred_expr f_p a_sem ctx x v. -Proof. Admitted. +Proof. + intros * SEM PS EVAL. unfold app_predicated in *. + eapply sem_pred_expr_NEapp6 in SEM; eauto. + - eapply sem_pred_expr_map_Pand2; eauto. + - intros. eapply sem_pred_expr_map_not; [|eassumption]. + rewrite eval_predf_negate. now rewrite EVAL. +Qed. Lemma sem_pred_expr_ident : forall ps l l_, @@ -465,18 +564,9 @@ Proof. inv H3. inv H1. eapply sem_pexpr_det in H0; try eassumption. discriminate. apply similar_refl. split; auto. apply sem_pred_expr_cons_false; auto. - - destruct x in *; cbn in *. - rewrite NE.app_NEmap in H0. - generalize dependent b; induction b; intros. - + cbn in *; repeat destr. inv Heqp0. inv H0. - * inv H6. inv H7. solve [repeat constructor; auto]. - * inv H6. inv H1. - -- exploit IHa; eauto; intros. inv H1. split; auto. - apply sem_pred_expr_cons_false; eauto. - -- exploit IHa; eauto; intros. inv H1. inv H3. - eapply sem_pexpr_det in H0; try eassumption. discriminate. - apply similar_refl. - + Admitted. + - destruct x; cbn [fst snd] in *. + unfold predicated_prod in H0. cbn in H0. + rewrite NE.app_NEmap in H0. Lemma sem_pred_expr_seq_app : forall A B (f: predicated (A -> B)) ps l f_ l_, diff --git a/src/hls/Gible.v b/src/hls/Gible.v index d7b0e66..cb080c5 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -192,6 +192,16 @@ Lemma eval_predf_Por : eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'. Proof. unfold eval_predf; split; simplify; auto with bool. Qed. +Lemma eval_predf_simplify : + forall ps p, + eval_predf ps (simplify p) = eval_predf ps p. +Proof. unfold eval_predf; intros. now rewrite simplify_correct. Qed. + +Lemma eval_predf_deep_simplify : + forall peq ps p, + eval_predf ps (deep_simplify peq p) = eval_predf ps p. +Proof. unfold eval_predf; intros. now rewrite deep_simplify_correct. Qed. + Lemma eval_predf_pr_equiv : forall p ps ps', (forall x, ps !! x = ps' !! x) -> diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index c2cebdc..d3cc280 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -1023,6 +1023,21 @@ Section SEM_PRED_EXEC. eapply sem_pexpr_eval; eauto. Qed. + Lemma sem_pred_expr_in_true : + forall pe v, + sem_pred_expr f a_sem ctx pe v -> + exists p e, NE.In (p, e) pe + /\ sem_pexpr ctx (from_pred_op f p) true + /\ a_sem ctx e v. + Proof. + induction pe; crush. + - inv H. do 2 eexists; split; try split; eauto. constructor. + - inv H. + + do 2 eexists; split; try split; eauto. constructor; tauto. + + exploit IHpe; eauto. simplify. + do 2 eexists; split; try split; eauto. constructor; tauto. + Qed. + End SEM_PRED_EXEC. Module HashExprNorm(HS: Hashable). @@ -1221,21 +1236,6 @@ Module HashExprNorm(HS: Hashable). eapply H.wf_hash_table_distr; eauto. eauto. Qed. - Lemma sem_pred_expr_in_true : - forall pe v, - sem_pred_expr f a_sem ctx pe v -> - exists p e, NE.In (p, e) pe - /\ sem_pexpr ctx (from_pred_op f p) true - /\ a_sem ctx e v. - Proof. - induction pe; crush. - - inv H. do 2 eexists; split; try split; eauto. constructor. - - inv H. - + do 2 eexists; split; try split; eauto. constructor; tauto. - + exploit IHpe; eauto. simplify. - do 2 eexists; split; try split; eauto. constructor; tauto. - Qed. - Definition pred_Ht_dec : forall x y: pred_op * HS.t, {x = y} + {x <> y}. Proof. 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 *. diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 92ad03f..99dfd77 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -386,11 +386,11 @@ Proof. solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto]. Qed. +Local Opaque simplify'. Lemma simplify_correct : forall h a, sat_predicate (simplify h) a = sat_predicate h a. Proof. - Local Opaque simplify'. induction h; crush. - replace (sat_predicate h1 a && sat_predicate h2 a) with (sat_predicate (simplify h1) a && sat_predicate (simplify h2) a) @@ -400,7 +400,29 @@ Proof. with (sat_predicate (simplify h1) a || sat_predicate (simplify h2) a) by crush. rewrite simplify'_correct. crush. - Local Transparent simplify'. +Qed. +Local Transparent simplify'. + +Lemma Plit_inj : + forall A (a b: bool * A), Plit a = Plit b -> a = b. +Proof. now inversion 1. Qed. + +Lemma deep_simplify'_correct : + forall peq h a, + sat_predicate (deep_simplify' peq h) a = sat_predicate h a. +Proof. + destruct h; auto; cbn in *; + destruct h1; destruct h2; intuition auto with *; destruct_match; auto; + clear Heqs; inv e; solve [now rewrite andb_diag | now rewrite orb_diag]. +Qed. + +Lemma deep_simplify_correct : + forall peq h a, + sat_predicate (deep_simplify peq h) a = sat_predicate h a. +Proof. + induction h; auto; + intros; cbn -[deep_simplify']; rewrite deep_simplify'_correct; + cbn; rewrite IHh1; now rewrite IHh2. Qed. Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := -- cgit