diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-26 10:08:16 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-26 10:08:44 +0100 |
| commit | 7eeb169b982af90fac9873956e70d2c471555c31 (patch) | |
| tree | 53a1a3a98bb5b1e38891ca77af17c10d852daea0 /src/hls/Predicate.v | |
| parent | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (diff) | |
| download | vericert-7eeb169b982af90fac9873956e70d2c471555c31.tar.gz vericert-7eeb169b982af90fac9873956e70d2c471555c31.zip | |
Finish some proofs and remove unnecessary Admitted
Diffstat (limited to 'src/hls/Predicate.v')
| -rw-r--r-- | src/hls/Predicate.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 99dfd77..86e992a 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -7,7 +7,7 @@ Require Import Coq.Logic.Decidable. Require Import vericert.common.Vericertlib. Require Import vericert.hls.Sat. -Require Import HashTree. +Require Import vericert.hls.HashTree. Declare Scope pred_op. @@ -603,7 +603,7 @@ Lemma stseytin_and_correct2 : sat_lit cur c <-> sat_lit p1 c /\ sat_lit p2 c. Proof. intros. split. intros. inv H1. unfold stseytin_and in *. - inv H0; try contradiction. Admitted. + inv H0; try contradiction. Abort. Lemma stseytin_or_correct : forall cur p1 p2 fm c, @@ -625,7 +625,7 @@ Lemma stseytin_or_correct2 : stseytin_or cur p1 p2 = fm -> sat_formula fm c -> sat_lit cur c <-> sat_lit p1 c \/ sat_lit p2 c. -Proof. Admitted. +Proof. Abort. Lemma xtseytin_correct : forall p next l n fm c, |