diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-12-07 19:05:34 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-12-07 19:05:34 +0100 |
| commit | 6941dd2ec8349b78c8622ac136d4617f6c26b9c6 (patch) | |
| tree | 24b2f0a25f5c887f1aa13c9b205c26428a1d17ab /unit-tests | |
| parent | eee17f377679c7bdcee82807e720a6e5cabfe408 (diff) | |
| parent | 50e3798575aa7ff0a13a483af23a384dee3d8bb7 (diff) | |
| download | smtcoq-6941dd2ec8349b78c8622ac136d4617f6c26b9c6.tar.gz smtcoq-6941dd2ec8349b78c8622ac136d4617f6c26b9c6.zip | |
Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit_tactics.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index ce530bd..1bbf484 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1475,3 +1475,26 @@ Section QInstAnd. Proof. verit. Qed. End QInstAnd. + + +Section OCamlCompDec. + Variable A : Type. + Variable HA : CompDec A. + Variable H2 : forall (h : A) (l x : list A), (h :: l) ++ x = h :: l ++ x. + Variable H4 : forall x : list A, nil ++ x = x. + Variable H5 : forall (x : A) (x0 : list A), nil = x :: x0 -> False. + Variable H6 : forall (x : list A) (x0 : list (list A)), nil = x :: x0 -> False. + Variable H8 : forall (x x0 : list A) (x1 x2 : list (list A)), x :: x1 = x0 :: x2 -> x = x0 /\ x1 = x2. + Variable proj_list : forall A : Type, list A -> list A -> list A. + Variable H0 : forall (H : list A) (H0 : A) (H1 : list A), proj_list A H (H0 :: H1) = H1. + Variable H10 : forall (H : list (list A)) (H0 : list A) (H1 : list (list A)), + proj_list (list A) H (H0 :: H1) = H1. + Variable proj_list0 : forall A : Type, A -> list A -> A. + Variable H9 : forall (H H0 : A) (H1 : list A), proj_list0 A H (H0 :: H1) = H0. + Variable H12 : forall (H H0 : list A) (H1 : list (list A)), proj_list0 (list A) H (H0 :: H1) = H0. + Variable H11 : forall (x : A) (x0 x1 : list A), x1 = nil \/ x1 = proj_list0 A x x1 :: proj_list A x0 x1. + + Goal forall (x y : list A) (a0 : A), + x ++ y = a0::nil -> x = nil /\ y = a0::nil \/ x = a0::nil /\ y = nil. + Proof. verit_no_check. Qed. +End OCamlCompDec. |