diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:00:58 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:00:58 +0200 |
| commit | 13d2c8be2ffb84bc8d40064b223562832e5a5a7e (patch) | |
| tree | 8e9b4c8b8c31ee95bcd7eeffaacf72b40215adb3 /examples | |
| parent | 0955c9b404b2bebbe76a15daaad09c03670e849e (diff) | |
| parent | 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 (diff) | |
| download | smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.tar.gz smtcoq-13d2c8be2ffb84bc8d40064b223562832e5a5a7e.zip | |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/examples/Example.v b/examples/Example.v index a088d96..952f91c 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -375,11 +375,11 @@ Section Group. Lemma simplification_right x1 x2 y: op x1 y ==? op x2 y -> x1 ==? x2. - Proof. intro H. smt_no_check H inverse'. Qed. + Proof. intro H. smt_no_check (H, inverse'). Qed. Lemma simplification_left x1 x2 y: op y x1 ==? op y x2 -> x1 ==? x2. - Proof. intro H. smt_no_check H inverse'. Qed. + Proof. intro H. smt_no_check (H, inverse'). Qed. Clear_lemmas. End Group. @@ -393,7 +393,6 @@ Section CompCert. Variable block : Set. Hypothesis eq_block : CompDec block. - Local Notation "a ==? b" := (@eqb_of_compdec block eq_block a b) (at level 60). Variable mem: Set. Hypothesis dec_mem : CompDec mem. @@ -403,11 +402,11 @@ Section CompCert. Hypothesis alloc_valid_block_1: forall m lo hi b, - valid_block (alloc_mem m lo hi) b ---> ((b ==? (alloc_block m lo hi)) || valid_block m b). + valid_block (alloc_mem m lo hi) b -> ((b = (alloc_block m lo hi)) \/ valid_block m b). Hypothesis alloc_valid_block_2: forall m lo hi b, - ((b ==? (alloc_block m lo hi)) || valid_block m b) ---> valid_block (alloc_mem m lo hi) b. + ((b = (alloc_block m lo hi)) \/ valid_block m b) -> (valid_block (alloc_mem m lo hi) b). Hypothesis alloc_not_valid_block: forall m lo hi, @@ -416,13 +415,13 @@ Section CompCert. Lemma alloc_valid_block_inv m lo hi b : valid_block m b -> valid_block (alloc_mem m lo hi) b. Proof. - intro H. verit alloc_valid_block_2 H. + intro H. verit (alloc_valid_block_2, H). Qed. Lemma alloc_not_valid_block_2 m lo hi b' : - valid_block m b' -> b' ==? (alloc_block m lo hi) = false. + valid_block m b' -> b' <> (alloc_block m lo hi). Proof. - intro H. verit alloc_not_valid_block H. + intro H. verit (alloc_not_valid_block, H). Qed. End CompCert. |