diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-05 17:34:42 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-05 17:34:42 +0200 |
| commit | 1b658795c8e6f0edca2cee48e5f7d39c971e422b (patch) | |
| tree | 47d7c8b91471c0a2aaa176a62fcc4c6bb342fb05 /unit-tests | |
| parent | 9d45fd745ecfd02cb21b3f0e93566b6ee864db38 (diff) | |
| parent | fac9967dcfcfd771cbcf17b364b324bc19587159 (diff) | |
| download | smtcoq-1b658795c8e6f0edca2cee48e5f7d39c971e422b.tar.gz smtcoq-1b658795c8e6f0edca2cee48e5f7d39c971e422b.zip | |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit_tactics.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index bd4082f..daff848 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1294,3 +1294,38 @@ Section CompDecHypotheses. Proof. verit. Qed. End CompDecHypotheses. + + +Section CompDecOnInterpretedType. + Variable A : Type. + Variable H : CompDec A. + Variable x : A. + Variable l2 : list A. + Variable Hcompdec : CompDec (list A). + Variable H1 : (forall (H3 H4 : A) (H5 H6 : list A), + eqb_of_compdec Hcompdec (H3 :: H5) (H4 :: H6) ---> + eqb_of_compdec H H4 H3 && eqb_of_compdec Hcompdec H6 H5 = true). + Variable H2 : (forall (H3 : A) (H4 : list A), + eqb_of_compdec Hcompdec nil (H3 :: H4) ---> false = true). + Variable Hcompdec0 : CompDec (list bool). + Variable H7_bool : (forall (H3 : bool) (H4 H5 : list bool), + eqb_of_compdec Hcompdec0 ((H3 :: H4) ++ H5)%list (H3 :: H4 ++ H5) = true). + Variable H7_A : (forall (H3 : A) (H4 H5 : list A), + eqb_of_compdec Hcompdec ((H3 :: H4) ++ H5)%list (H3 :: H4 ++ H5) = true). + Variable H6_bool : (forall H3 : list bool, + eqb_of_compdec Hcompdec0 (nil ++ H3)%list H3 = true). + Variable H6_A : (forall H3 : list A, eqb_of_compdec Hcompdec (nil ++ H3)%list H3 = true). + Variable c : CompDec bool. + Variable search : forall {A : Type} {H: CompDec A}, A -> list A -> bool. + Arguments search {_ _} _ _. + Variable H5_bool : (forall (H3 H4 : bool) (H5 : list bool), + search H3 (H4 :: H5) <---> eqb_of_compdec c H3 H4 || search H3 H5 = true). + Variable H5_A : (forall (H3 H4 : A) (H5 : list A), + search H3 (H4 :: H5) <---> eqb_of_compdec H H3 H4 || search H3 H5 = true). + Variable H4_bool : (forall H3 : bool, search H3 nil <---> false = true). + Variable H4_A : (forall H3 : A, search H3 nil <---> false = true). + + Goal search x l2 <---> search x l2 = true. + Proof. verit. Qed. + +End CompDecOnInterpretedType. |