diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-09-20 18:10:13 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-09-20 18:10:13 +0200 |
| commit | f8faf0c9395047032e6fe9d0db5f45205cd4da06 (patch) | |
| tree | 3d0069c9190b8fed1e5ce81e633cd12377ca984c /unit-tests | |
| parent | c5db7f8dcf98fc354737ad15dc783c2e9241efb5 (diff) | |
| download | smtcoq-f8faf0c9395047032e6fe9d0db5f45205cd4da06.tar.gz smtcoq-f8faf0c9395047032e6fe9d0db5f45205cd4da06.zip | |
vauto is now complete w.r.t. symmetry of equality (but may be exponential in some cases)
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. |