diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-30 16:24:37 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-30 16:24:37 +0100 |
| commit | cf2f99c93deadfa7aa0f3f77d6a77ab8ce7a7950 (patch) | |
| tree | 75015244ce02c5872836dde2a269e7b8dc015d6e | |
| parent | 4da92e9d5d9896645909656705f4ab78cdcb029d (diff) | |
| download | vericert-cf2f99c93deadfa7aa0f3f77d6a77ab8ce7a7950.tar.gz vericert-cf2f99c93deadfa7aa0f3f77d6a77ab8ce7a7950.zip | |
Finish second flap2 proof
| -rw-r--r-- | src/hls/AbstrSemIdent.v | 10 |
1 files changed, 9 insertions, 1 deletions
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) |