diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-12-07 18:59:03 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-12-07 18:59:03 +0100 |
| commit | 01900662373ca1b72d9c78171bcc21133cec3bf4 (patch) | |
| tree | 0cecbb37aa04ba65907178c711ac743333b1996a /unit-tests | |
| parent | f6e575e0736a80b4c253be48b3c4c58cc5101137 (diff) | |
| parent | bd346e44c8993b758013d98855b71404e4d0ad7f (diff) | |
| download | smtcoq-01900662373ca1b72d9c78171bcc21133cec3bf4.tar.gz smtcoq-01900662373ca1b72d9c78171bcc21133cec3bf4.zip | |
Merge remote-tracking branch 'origin/master' into coq-8.10
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. |