diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-12-07 19:01:16 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-12-07 19:01:16 +0100 |
| commit | 96cd98b3e04aba915cb36cba39e15a39422ab628 (patch) | |
| tree | 099efa22abad84f3fa6028dfe7310cd96efd73d0 /unit-tests | |
| parent | 349815b8f98c548d9054efad176e3894a37a3957 (diff) | |
| parent | 01900662373ca1b72d9c78171bcc21133cec3bf4 (diff) | |
| download | smtcoq-96cd98b3e04aba915cb36cba39e15a39422ab628.tar.gz smtcoq-96cd98b3e04aba915cb36cba39e15a39422ab628.zip | |
Merge remote-tracking branch 'origin/coq-8.10' into coq-8.11
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. |