diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-29 16:13:24 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-29 16:13:24 +0100 |
| commit | c10635f9e6890a6171c5c1cc8eb6e3298d2006b1 (patch) | |
| tree | a5f0e39431138796d297913b37578f758a45257f /src/hls/GiblePargenproofEquiv.v | |
| parent | 0c5c896490ee0d4b553f26d00b2ad2a971d25d4f (diff) | |
| download | vericert-c10635f9e6890a6171c5c1cc8eb6e3298d2006b1.tar.gz vericert-c10635f9e6890a6171c5c1cc8eb6e3298d2006b1.zip | |
Prove more admitted theorems
Diffstat (limited to 'src/hls/GiblePargenproofEquiv.v')
| -rw-r--r-- | src/hls/GiblePargenproofEquiv.v | 30 |
1 files changed, 15 insertions, 15 deletions
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. |