diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-11-11 12:29:50 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-11 12:29:50 +0000 |
commit | 9434e9223a67ce2d38e1f1de4e3d8129552ce4cc (patch) | |
tree | 2bd765fb5fbbacd524ed78252fc2d4d91f192ac2 /src/hls/Predicate.v | |
parent | 8909d8e8f49cecc1eda24dab8578186f96563d0b (diff) | |
download | vericert-9434e9223a67ce2d38e1f1de4e3d8129552ce4cc.tar.gz vericert-9434e9223a67ce2d38e1f1de4e3d8129552ce4cc.zip |
Add simplify operation and simplify IfConversion
Diffstat (limited to 'src/hls/Predicate.v')
-rw-r--r-- | src/hls/Predicate.v | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index dc70010..a2b5400 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -443,3 +443,61 @@ Proof. simplify. repeat rewrite negate_correct. rewrite H0. rewrite H. auto. Qed. + +Definition simplify' (p: pred_op) := + match p with + | A ∧ T => A + | T ∧ A => A + | _ ∧ ⟂ => ⟂ + | ⟂ ∧ _ => ⟂ + | _ ∨ T => T + | T ∨ _ => T + | A ∨ ⟂ => A + | ⟂ ∨ A => A + | A => A + end. + +Lemma pred_op_dec : + forall p1 p2: pred_op, + { p1 = p2 } + { p1 <> p2 }. +Proof. pose proof Pos.eq_dec. repeat decide equality. Qed. + +Fixpoint simplify (p: pred_op) := + match p with + | A ∧ B => + let A' := simplify A in + let B' := simplify B in + simplify' (A' ∧ B') + | A ∨ B => + let A' := simplify A in + let B' := simplify B in + simplify' (A' ∨ B') + | T => T + | ⟂ => ⟂ + | Plit a => Plit a + end. + +Lemma simplify'_correct : + forall h a, + sat_predicate (simplify' h) a = sat_predicate h a. +Proof. + destruct h; crush; repeat destruct_match; crush; + solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto]. +Qed. + +Lemma simplify_correct : + forall h a, + sat_predicate (simplify h) a = sat_predicate h a. +Proof. + Local Opaque simplify'. + induction h; crush. + - replace (sat_predicate h1 a && sat_predicate h2 a) + with (sat_predicate (simplify h1) a && sat_predicate (simplify h2) a) + by crush. + rewrite simplify'_correct. crush. + - replace (sat_predicate h1 a || sat_predicate h2 a) + with (sat_predicate (simplify h1) a || sat_predicate (simplify h2) a) + by crush. + rewrite simplify'_correct. crush. + Local Transparent simplify'. +Qed. |