diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-07-20 15:38:44 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-07-20 15:38:44 +0200 |
| commit | c8a696682fcbdc720d67eb8d93f2c0c5b5c03548 (patch) | |
| tree | 0f152937cc283e28f14f4208a4ad2bc96380bcc9 /src/bva/Bva_checker.v | |
| parent | 9c9faf18affce1c7b561b93584a779d8b6f36b2f (diff) | |
| download | smtcoq-c8a696682fcbdc720d67eb8d93f2c0c5b5c03548.tar.gz smtcoq-c8a696682fcbdc720d67eb8d93f2c0c5b5c03548.zip | |
Define substitution conformly to SMT-LIB
Diffstat (limited to 'src/bva/Bva_checker.v')
| -rw-r--r-- | src/bva/Bva_checker.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 20cc2cf..24cf620 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -1186,7 +1186,7 @@ Proof. intros f Heq2. case_eq (t_atom .[ f]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N|N| | | | ]; + intros [ | | | | | | |[ A B | A| | | |n]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a b Heq3. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros c Heq4. @@ -3215,7 +3215,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; + intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVand *) - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); @@ -4513,7 +4513,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres). case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | |n]|N|N|N|N|N|N|N|N|N| | | | ]; + intros [ | | | | | | | [ A B | A | | | |n]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a1' a2' Heq9. @@ -5168,7 +5168,7 @@ Proof. case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ]; + intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a1' a2' Heq9. @@ -5394,7 +5394,7 @@ Proof. case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). - intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; + intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq15; try (now apply C.interp_true). @@ -5805,7 +5805,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVadd *) @@ -6603,7 +6603,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVmult *) - case_eq ((a1 == a1') && (a2 == a2') (* || (a1 == a2') && (a2 == a1')*) ); simpl; intros Heq10; try (now apply C.interp_true). @@ -6911,7 +6911,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). (* BVconcat *) - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( @@ -8055,7 +8055,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2. case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc. (* BVshl *) @@ -8385,7 +8385,7 @@ Proof. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). - intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). + intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2. case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc. (* BVshr *) |