diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-10-30 14:55:51 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-30 14:56:54 +0100 |
| commit | 64a7fd889491bedffa3e3bcf130599c841c7008e (patch) | |
| tree | d44e90c7aa37d74b41f48e237b46dad2aee67959 /src/hls/Predicate.v | |
| parent | 9db69b471864cb9e3868dd2c82bc0e2df3955b51 (diff) | |
| download | vericert-64a7fd889491bedffa3e3bcf130599c841c7008e.tar.gz vericert-64a7fd889491bedffa3e3bcf130599c841c7008e.zip | |
Changed and proved some more theorems
Diffstat (limited to 'src/hls/Predicate.v')
| -rw-r--r-- | src/hls/Predicate.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 7786c5d..8ff61e7 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -672,6 +672,32 @@ Fixpoint max_predicate (p: pred_op) : positive := | Por a b => Pos.max (max_predicate a) (max_predicate b) end. + Lemma max_predicate_deep_simplify' : + forall peq curr r, + (r <= max_predicate (deep_simplify' peq curr))%positive -> + (r <= max_predicate curr)%positive. + Proof. + destruct curr; cbn -[deep_simplify']; auto. + - intros. unfold deep_simplify' in H. + destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia. + - intros. unfold deep_simplify' in H. + destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia. + Qed. + + Lemma max_predicate_deep_simplify : + forall peq curr r, + (r <= max_predicate (deep_simplify peq curr))%positive -> + (r <= max_predicate curr)%positive. + Proof. + induction curr; try solve [cbn; auto]; cbn -[deep_simplify'] in *. + - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *. + assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia. + inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia. + - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *. + assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia. + inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia. + Qed. + Definition tseytin (p: pred_op) : {fm: formula | forall a, sat_predicate p a = true <-> sat_formula fm a}. |