diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-05 16:07:47 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-05 16:07:47 +0200 |
commit | 9d45fd745ecfd02cb21b3f0e93566b6ee864db38 (patch) | |
tree | f358d6a1ca84dd2d71c8dddc20bdfa2444427190 /unit-tests | |
parent | 64517cd829de743338ee3df7e94ecd262dc51505 (diff) | |
parent | 907cb562f511e3bbd3f84011e5d3e101f00c4252 (diff) | |
download | smtcoq-9d45fd745ecfd02cb21b3f0e93566b6ee864db38.tar.gz smtcoq-9d45fd745ecfd02cb21b3f0e93566b6ee864db38.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 | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 7701753..bd4082f 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1263,3 +1263,34 @@ Section UnknowUnderForall. Goal forall (l : list Z) (x : Z), hd_error l = Some x -> l <> nil. Proof. verit. Qed. End UnknowUnderForall. + + +Section CompDecHypotheses. + Variable A : Type. + Variable H : CompDec A. + Variable x : A. + Variable l2 : list A. + Hypothesis H1 : forall (x y : A) (x0 y0 : list A), + x :: x0 = y :: y0 -> y = x /\ y0 = x0. + Hypothesis H2 : forall (H : A) (H0 : list A), nil = H :: H0 -> False. + Hypothesis H7_bool : forall (H : bool) (H0 H1 : list bool), + ((H :: H0) ++ H1)%list = H :: H0 ++ H1. + Hypothesis H7_A : forall (H : A) (H0 H1 : list A), + ((H :: H0) ++ H1)%list = H :: H0 ++ H1. + Hypothesis H6_bool : forall H : list bool, (nil ++ H)%list = H. + Hypothesis H6_A : forall H : list A, (nil ++ H)%list = H. + Variable search : forall {A : Type} {H: CompDec A}, A -> list A -> bool. + Arguments search {_ _} _ _. + Hypothesis H5_bool : forall (H : CompDec bool) (H0 H1 : bool) (H2 : list bool), + search H0 (H1 :: H2) = + (if eqb_of_compdec H H0 H1 then true else search H0 H2). + Hypothesis H5_A : forall (H : CompDec A) (H0 H1 : A) (H2 : list A), + search H0 (H1 :: H2) = + (if eqb_of_compdec H H0 H1 then true else search H0 H2). + Hypothesis H4_bool : forall (H : CompDec bool) (H0 : bool), search H0 nil = false. + Hypothesis H4_A : forall (H : CompDec A) (H0 : A), search H0 nil = false. + + Goal search x l2 = search x l2. + Proof. verit. Qed. + +End CompDecHypotheses. |