diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-04 22:23:39 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-04 22:23:39 +0100 |
commit | f7566f5880d7b41e22468c77d61983c556014bd4 (patch) | |
tree | f95fa236386d2893d2af09dd4454b0e5076cc01a /src/hls/Predicate.v | |
parent | 2c74f5a4a9499d5f511089000421ca20fc2049d5 (diff) | |
download | vericert-f7566f5880d7b41e22468c77d61983c556014bd4.tar.gz vericert-f7566f5880d7b41e22468c77d61983c556014bd4.zip |
Continue proofs about Abstr.v
Diffstat (limited to 'src/hls/Predicate.v')
-rw-r--r-- | src/hls/Predicate.v | 49 |
1 files changed, 18 insertions, 31 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 68a0927..f99fa4f 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -53,14 +53,6 @@ Section PRED_DEFINITION. Definition simplify' (p: pred_op) := match p with - (* | (Plit (b1, a)) ∧ (Plit (b2, b)) as p' => *) - (* if Pos.eqb a b then *) - (* if negb (xorb b1 b2) then Plit (b1, a) else ⟂ *) - (* else p' *) - (* | (Plit (b1, a)) ∨ (Plit (b2, b)) as p' => *) - (* if Pos.eqb a b then *) - (* if negb (xorb b1 b2) then Plit (b1, a) else T *) - (* else p' *) | Pand A Ptrue => A | Pand Ptrue A => A | Pand _ Pfalse => Pfalse @@ -100,6 +92,15 @@ Section PRED_DEFINITION. Context (eqd: forall a b: A, {a = b} + {a <> b}). + 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. + Definition deep_simplify' (p: pred_op) := match p with | Pand A Ptrue => A @@ -111,18 +112,13 @@ Section PRED_DEFINITION. | Por A Pfalse => A | Por Pfalse A => A - | Pand (Plit (b1, a)) (Plit (b2, b)) => - if eqd a b then - if bool_eqdec b1 b2 then - Plit (b1, a) - else Pfalse - else Pand (Plit (b1, a)) (Plit (b2, b)) - | Por (Plit (b1, a)) (Plit (b2, b)) => - if eqd a b then - if bool_eqdec b1 b2 then - Plit (b1, a) - else Ptrue - else Por (Plit (b1, a)) (Plit (b2, b)) + | Pand A B => + if eq_dec A B then A + else Pand A B + + | Por A B => + if eq_dec A B then A + else Por A B | A => A end. @@ -161,15 +157,6 @@ 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. @@ -395,9 +382,9 @@ Lemma simplify'_correct : forall h a, sat_predicate (simplify' h) a = sat_predicate h a. Proof. -(*destruct h; crush; repeat destruct_match; crush; + destruct h; crush; repeat destruct_match; crush; solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto]. -Qed.*) Admitted. +Qed. Lemma simplify_correct : forall h a, |