diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/hls/Predicate.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index d8de758..68a0927 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -161,6 +161,15 @@ Section PRED_DEFINITION. - intros. cbn in *. apply orb_prop in H. constructor. tauto. Qed. + Definition eq_dec: forall a b: pred_op, + {a = b} + {a <> b}. + Proof. + pose proof bool_eq_dec. + assert (forall a b: bool * predicate, {a = b} + {a <> b}) + by decide equality. + induction a; destruct b; decide equality. + Defined. + End DEEP_SIMPLIFY. End PRED_DEFINITION. @@ -863,3 +872,23 @@ Proof. inv H1. specialize (IHop1 H H2). specialize (IHop2 H H3). cbn. rewrite IHop1. rewrite IHop2. auto. Qed. + +Lemma sat_predicateP_det : + forall a p b b', + sat_predicateP a p b -> + sat_predicateP a p b' -> + b = b'. +Proof. induction p; crush; inv H; inv H0; auto. Qed. + +Lemma equiv_sat_predicate_sat_predicateP : + forall p p' a b, + p == p' -> + sat_predicateP a p b -> + sat_predicateP a p' b. +Proof. + intros. + pose proof (sat_pred_equiv_sat_predicateP a p). + pose proof (sat_pred_equiv_sat_predicateP a p'). + pose proof (sat_predicateP_det a p _ _ H1 H0). + rewrite H in H3. now rewrite H3 in H2. +Qed. |