diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-28 17:35:38 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-28 17:35:38 +0100 |
| commit | 4917816d72d131cc0c3a10c00648a5df354e7500 (patch) | |
| tree | d89e4b4e18e797e9a794a34f76349992974db2e5 /src/hls/GiblePargenproofCommon.v | |
| parent | 3cca0fa62b1b78ca0df38b539d88704b26b21645 (diff) | |
| download | vericert-4917816d72d131cc0c3a10c00648a5df354e7500.tar.gz vericert-4917816d72d131cc0c3a10c00648a5df354e7500.zip | |
Work on forward proofs
Diffstat (limited to 'src/hls/GiblePargenproofCommon.v')
| -rw-r--r-- | src/hls/GiblePargenproofCommon.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 22b5978..2dbdf12 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -221,6 +221,21 @@ Proof. unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto. Qed. +Lemma predicated_not_inP_equiv : + forall A (a: predicated A) p, + predicated_not_in p a = true -> predicated_not_inP p a. +Proof. + induction a. + - intros. cbn in *. unfold predicated_not_inP; intros. + unfold not; intros. inv H0. cbn in *. + destruct (predin peq p op) eqn:?; try discriminate. eapply predin_PredIn in H1. + rewrite H1 in Heqb. discriminate. + - intros. cbn in H. eapply andb_prop in H. inv H. eapply IHa in H0. + unfold predicated_not_inP in *; intros. inv H. inv H3; cbn in *; eauto. + unfold not; intros. eapply predin_PredIn in H. now rewrite H in H1. +Qed. + + Lemma truthy_dec: forall ps a, truthy ps a \/ falsy ps a. Proof. |