diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 11:44:58 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 11:45:05 +0100 |
| commit | 405e822a4e769969ef01a683d486accee0d71da2 (patch) | |
| tree | 986d3e660f621e9d17c621e3c5d3924de1c942cb /src/hls/GiblePargenproof.v | |
| parent | a04e972f3dcc94459399e4d4168b8d26d32e1fae (diff) | |
| download | vericert-405e822a4e769969ef01a683d486accee0d71da2.tar.gz vericert-405e822a4e769969ef01a683d486accee0d71da2.zip | |
Change nat to positive in Sat proof
Diffstat (limited to 'src/hls/GiblePargenproof.v')
| -rw-r--r-- | src/hls/GiblePargenproof.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 1bcc352..6bfc654 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -576,13 +576,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. induction p; crush. - destruct_match. inv Heqp0. destruct b. - + cbn in H0. rewrite <- H0. - rewrite Pos2Nat.id. eauto. + + cbn in H0. rewrite <- H0. eauto. + replace false with (negb true) by auto. apply sem_pexpr_negate. cbn in H0. apply negb_true_iff in H0. rewrite negb_involutive in H0. - rewrite <- H0. rewrite Pos2Nat.id. - eauto. + rewrite <- H0. eauto. - constructor. - rewrite eval_predf_Pand in H0. apply andb_false_iff in H0. inv H0. eapply IHp1 in H1. @@ -611,13 +609,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. induction p; crush. - destruct_match. inv Heqp0. destruct b. - + cbn in H0. rewrite <- H0. - rewrite Pos2Nat.id. eauto. + + cbn in H0. rewrite <- H0. eauto. + replace true with (negb false) by auto. apply sem_pexpr_negate. cbn in H0. apply negb_true_iff in H0. - rewrite <- H0. rewrite Pos2Nat.id. - eauto. + rewrite <- H0. eauto. - constructor. - rewrite eval_predf_Pand in H0. apply andb_true_iff in H0. inv H0. |