diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-03-12 14:45:27 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-03-12 14:45:27 +0000 |
| commit | b4258bda8e35603bbb3989c6469b7803d149ba91 (patch) | |
| tree | 89cbfd3664884e250f1c5bd77bf56da50ef07218 | |
| parent | 76c1ea086f828a4488f4d4ed1f5df441e56fc969 (diff) | |
| download | vericert-b4258bda8e35603bbb3989c6469b7803d149ba91.tar.gz vericert-b4258bda8e35603bbb3989c6469b7803d149ba91.zip | |
Add temp files
| -rw-r--r-- | src/hls/Abstr.v | 10 | ||||
| -rw-r--r-- | src/hls/Sat.v | 24 |
2 files changed, 24 insertions, 10 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index f332905..2410b2a 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1611,10 +1611,12 @@ Lemma sem_expr_beq_correct : sem_pred_expr pt sem_value (mkctx i) b v. Proof. induction a. - - intros. inv H0. - unfold beq_pred_expr; intros. destruct_match; subst; auto. - repeat destruct_match. simplify. clear Heqs. clear n. - inv H0. + - intros. inv H0. unfold beq_pred_expr in *; intros. destruct_match; subst; auto. + + constructor; auto. + + repeat destruct_match. simplify. inv Heqp. clear Heqs. + admit. + - intros. +Admitted. Lemma sem_expr_beq_correct_mem : forall pt i a b v, diff --git a/src/hls/Sat.v b/src/hls/Sat.v index ae0a05c..960be8e 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -506,11 +506,10 @@ Lemma sat_measure_setClause' : Proof. induction cl; intros. { simpl in *. inv H. unfold not in *. intros. inv H. } - { simpl in H. - repeat (destruct_match; crush; []). destruct_match. - repeat (destruct_match; crush; []). inv H. eapply IHcl; eauto. - inv H. unfold not. intros. inv H. contradiction. eapply IHcl; eauto. - } + simpl in H. + repeat (destruct_match; crush; []). destruct_match. + repeat (destruct_match; crush; []). inv H. eapply IHcl; eauto. + inv H. unfold not. intros. inv H. contradiction. eapply IHcl; eauto. Qed. Lemma sat_measure_setClause'' : @@ -533,6 +532,19 @@ Proof. } Qed. +Lemma sat_measure_setClause2'' : + forall cl cl' l A, + setClause cl l = inleft (exist _ cl' A) -> + forall l', + l' <> snd l -> + In l' (map snd cl') -> + In l' (map snd cl). +Proof. + induction cl; intros. + { cbn in *. inv H. cbn in *. auto. } + exploit IHcl; eauto. + Admitted. + Lemma sat_measure_setClause : forall cl cl' l A, In (snd l) (map snd cl) -> @@ -540,7 +552,7 @@ Lemma sat_measure_setClause : NSet.cardinal (lit_set_cl cl') < NSet.cardinal (lit_set_cl cl). Proof. intros. pose proof H0. apply sat_measure_setClause' in H0. - pose proof (sat_measure_setClause'' _ _ _ _ H1). admit. + pose proof (sat_measure_setClause'' _ _ _ _ H1). Admitted. Definition InFm l (fm: formula) := exists cl, In cl fm /\ In l cl. |