From 651a3f29878214e9c33ce8bb103dc8c40191c950 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 24 Apr 2023 19:01:22 +0100 Subject: Added lemmas about decidability of Sat --- src/hls/GiblePargenproof.v | 21 --------------------- 1 file changed, 21 deletions(-) (limited to 'src/hls/GiblePargenproof.v') 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) -> -- cgit