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/Predicate.v | |
| parent | 0c5c896490ee0d4b553f26d00b2ad2a971d25d4f (diff) | |
| download | vericert-c10635f9e6890a6171c5c1cc8eb6e3298d2006b1.tar.gz vericert-c10635f9e6890a6171c5c1cc8eb6e3298d2006b1.zip | |
Prove more admitted theorems
Diffstat (limited to 'src/hls/Predicate.v')
| -rw-r--r-- | src/hls/Predicate.v | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 92ad03f..99dfd77 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -386,11 +386,11 @@ Proof. solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto]. Qed. +Local Opaque simplify'. 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) @@ -400,7 +400,29 @@ Proof. with (sat_predicate (simplify h1) a || sat_predicate (simplify h2) a) by crush. rewrite simplify'_correct. crush. - Local Transparent simplify'. +Qed. +Local Transparent simplify'. + +Lemma Plit_inj : + forall A (a b: bool * A), Plit a = Plit b -> a = b. +Proof. now inversion 1. Qed. + +Lemma deep_simplify'_correct : + forall peq h a, + sat_predicate (deep_simplify' peq h) a = sat_predicate h a. +Proof. + destruct h; auto; cbn in *; + destruct h1; destruct h2; intuition auto with *; destruct_match; auto; + clear Heqs; inv e; solve [now rewrite andb_diag | now rewrite orb_diag]. +Qed. + +Lemma deep_simplify_correct : + forall peq h a, + sat_predicate (deep_simplify peq h) a = sat_predicate h a. +Proof. + induction h; auto; + intros; cbn -[deep_simplify']; rewrite deep_simplify'_correct; + cbn; rewrite IHh1; now rewrite IHh2. Qed. Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) := |