diff options
Diffstat (limited to 'src/hls/GiblePargenproofCommon.v')
-rw-r--r-- | src/hls/GiblePargenproofCommon.v | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 345836f..9254a3b 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -210,31 +210,6 @@ Proof. econstructor. split. constructor. right. eauto. auto. Qed. -Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) := - forall op e, NE.In (op, e) l -> ~ PredIn p op. - -Lemma predicated_not_inP_cons : - forall A p (a: (pred_op * A)) l, - predicated_not_inP p (NE.cons a l) -> - predicated_not_inP p l. -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. |