diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-09-20 18:15:07 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-09-20 18:15:07 +0200 |
| commit | e227540a5ceb1ceaab80b71e25cfb91e8cf2d83f (patch) | |
| tree | 4ea35fd99d42bcb2071c324e6837fd6da8256543 /unit-tests | |
| parent | df070a02f2e11dcb142debf46fe3027941d0b4e0 (diff) | |
| parent | f8faf0c9395047032e6fe9d0db5f45205cd4da06 (diff) | |
| download | smtcoq-e227540a5ceb1ceaab80b71e25cfb91e8cf2d83f.tar.gz smtcoq-e227540a5ceb1ceaab80b71e25cfb91e8cf2d83f.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 | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 34b5dfd..2bdc520 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1369,3 +1369,40 @@ Section PropToBool. Goal (forall (x x0 : bool) (x1 x2 : list bool), x :: x1 = x0 :: x2 -> x = x0) -> true. Proof. verit. Qed. End PropToBool. + + +Section EqSym. + Variable A : Type. + Variable HA : CompDec A. + Variable H8 : forall (h : list A) (l : list (list A)), tl (h :: l) = l. + Variable H12_A : forall (h : A) (l : list A), tl (h :: l) = l. + Variable H9 : forall (h : option A) (l : list (option A)), tl (h :: l) = l. + Variable H12 : @tl (list A) nil = nil. + Variable H13_A : @tl A nil = nil. + Variable H14 : @tl (option A) nil = nil. + Variable H13 : forall (h : list A) (l : list (list A)), hd_error (h :: l) = Some h. + Variable H10_A : forall (h : A) (l : list A), hd_error (h :: l) = Some h. + Variable H15 : forall (h : option A) (l : list (option A)), hd_error (h :: l) = Some h. + Variable H10 : @hd_error (list A) nil = None. + Variable H11_A : @hd_error A nil = None. + Variable H16 : @hd_error (option A) nil = None. + Variable H11 : forall x : list A, Some x = None -> False. + Variable H7_A : forall x : A, Some x = None -> False. + Variable H17 : forall x : option A, Some x = None -> False. + Variable H7 : forall x x0 : list A, Some x = Some x0 -> x = x0. + Variable H6_A : forall x x0 : A, Some x = Some x0 -> x = x0. + Variable H18 : forall x x0 : option A, Some x = Some x0 -> x = x0. + Variable H4 : forall (x : list A) (x0 : list (list A)), nil = x :: x0 -> False. + Variable H3_A : forall (x : A) (x0 : list A), nil = x :: x0 -> False. + Variable H5 : forall (x : option A) (x0 : list (option A)), nil = x :: x0 -> False. + Variable H3 : forall (x x0 : list A) (x1 x2 : list (list A)), x :: x1 = x0 :: x2 -> x = x0. + Variable H2_A : forall (x x0 : A) (x1 x2 : list A), x :: x1 = x0 :: x2 -> x = x0. + Variable H6 : forall (x x0 : option A) (x1 x2 : list (option A)), x :: x1 = x0 :: x2 -> x = x0. + Variable x : A. + Variable xs : list A. + Variable a : A. + Variable r : list A. + + Goal hd_error (x :: xs) = Some a /\ tl (x :: xs) = r <-> x :: xs = a :: r. + Proof. verit. Qed. +End EqSym. |