From 195c8282275fd4ad4f93050d1ffeed3c323a45ea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 13:57:50 +0200
Subject: [PATCH] Add tests for `simpl` on `last`.
---
tests/list.ref | 22 ++++++++++++++++++++++
tests/list.v | 17 +++++++++++++++++
2 files changed, 39 insertions(+)
create mode 100644 tests/list.ref
create mode 100644 tests/list.v
diff --git a/tests/list.ref b/tests/list.ref
new file mode 100644
index 00000000..ac5cc48d
--- /dev/null
+++ b/tests/list.ref
@@ -0,0 +1,22 @@
+1 goal
+
+ ============================
+ None = None
+1 goal
+
+ ============================
+ Some 10 = Some 10
+1 goal
+
+ ============================
+ Some 11 = Some 11
+1 goal
+
+ l : list nat
+ ============================
+ last (11 :: l) = last (11 :: l)
+1 goal
+
+ l : list nat
+ ============================
+ last (10 :: l) = last (10 :: l)
diff --git a/tests/list.v b/tests/list.v
new file mode 100644
index 00000000..dd1d58fb
--- /dev/null
+++ b/tests/list.v
@@ -0,0 +1,17 @@
+From stdpp Require Import list.
+
+Lemma last_simpl_test_nil : last [] =@{option nat} None.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_singleton : last [10] = Some 10.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_double : last [10; 11] = Some 11.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_cons_cons l : last (10 :: 11 :: l) = last (11 :: l).
+Proof. simpl. Show. done. Qed.
+
+(* The following should not [simpl] and result in a [match]. *)
+Lemma last_simpl_test_cons l : last (10 :: l) = last (10 :: l).
+Proof. simpl. Show. done. Qed.
--
GitLab