From cf2f99c93deadfa7aa0f3f77d6a77ab8ce7a7950 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 30 May 2023 16:24:37 +0100 Subject: Finish second flap2 proof --- src/hls/AbstrSemIdent.v | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src/hls/AbstrSemIdent.v') diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v index e1bf89a..30b287d 100644 --- a/src/hls/AbstrSemIdent.v +++ b/src/hls/AbstrSemIdent.v @@ -745,7 +745,15 @@ Lemma sem_pred_expr_flap2_2 : forall A B C (f: predicated (A -> B -> C)) ps l1 l2 x, sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) x -> exists f_, sem_pred_expr ps sem_ident ctx f f_ /\ f_ l1 l2 = x. -Proof. Admitted. +Proof. + induction f; cbn; intros. + - inv H; destruct a; cbn in *. inv H5. eexists; split; eauto. + constructor; auto. constructor. + - destruct a. cbn [fst snd] in *. inv H. + + inv H6. eexists; split; eauto. constructor; auto. constructor. + + exploit IHf; eauto; simplify. + eexists; split; eauto. eapply sem_pred_expr_cons_false; eauto. +Qed. Lemma sem_pred_expr_seq_app_val : forall A B V (s: @Abstr.ctx G -> B -> V -> Prop) -- cgit