diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-04-24 19:01:22 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-04-24 19:01:22 +0100 |
| commit | 651a3f29878214e9c33ce8bb103dc8c40191c950 (patch) | |
| tree | 1eb4a91c716184e9a8d8b7ddf9fb448fdcd457db /src/hls/GiblePargenproof.v | |
| parent | b4258bda8e35603bbb3989c6469b7803d149ba91 (diff) | |
| download | vericert-651a3f29878214e9c33ce8bb103dc8c40191c950.tar.gz vericert-651a3f29878214e9c33ce8bb103dc8c40191c950.zip | |
Added lemmas about decidability of Sat
Diffstat (limited to 'src/hls/GiblePargenproof.v')
| -rw-r--r-- | src/hls/GiblePargenproof.v | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 9c85d54..1bcc352 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -552,27 +552,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite eval_predf_negate. rewrite H0. auto. Qed. - Lemma sem_pexpr_negate : - forall A ctx p b, - sem_pexpr ctx p b -> - @sem_pexpr A ctx (¬ p) (negb b). - Proof. - induction p; crush. - - destruct_match. destruct b0; crush. inv Heqp0. - constructor. inv H. rewrite negb_involutive. auto. - constructor. inv H. auto. - - inv H. constructor. - - inv H. constructor. - - inv H. inv H3. - + apply IHp1 in H. solve [constructor; auto]. - + apply IHp2 in H. solve [constructor; auto]. - + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. - - inv H. inv H3. - + apply IHp1 in H. solve [constructor; auto]. - + apply IHp2 in H. solve [constructor; auto]. - + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. - Qed. - Lemma sem_pexpr_evaluable : forall A ctx f_p ps, (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> |