diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-28 18:59:21 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-28 18:59:21 +0100 |
| commit | bd5a14e5b807c18142fb20bb0552dc0dbc92e40f (patch) | |
| tree | 97bd3367230d6a90139c786b6e6d5af89b2e8d94 /src/hls/GiblePargenproofEquiv.v | |
| parent | 4917816d72d131cc0c3a10c00648a5df354e7500 (diff) | |
| download | vericert-bd5a14e5b807c18142fb20bb0552dc0dbc92e40f.tar.gz vericert-bd5a14e5b807c18142fb20bb0552dc0dbc92e40f.zip | |
Finish proofs in GiblePargenproofForward.v
Diffstat (limited to 'src/hls/GiblePargenproofEquiv.v')
| -rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index b63f2fd..c2cebdc 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -1738,12 +1738,14 @@ Context (ictx: @ctx FUN) (octx: @ctx TFUN) (HSIM: similar ictx octx). Lemma abstr_check_correct : forall i' a b cf, - (exists ps, forall x, sem_pexpr ictx (get_forest_p' x (forest_preds a)) ps !! x) -> check a b = true -> sem ictx a (i', cf) -> exists ti', sem octx b (ti', cf) /\ match_states i' ti'. Proof. - intros * EVALUABLE **. unfold check in H. simplify. + intros. + assert (EVALUABLE: (exists ps, forall x, sem_pexpr ictx (get_forest_p' x (forest_preds a)) ps !! x)). + { inv H0. inv H4. eauto. } + unfold check in H. simplify. inv H0. inv H10. inv H11. eexists; split; constructor; auto. - constructor. intros. |