From dabf8fc1b57c0966e085c900f169dc9454d60923 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 16:09:44 +0200
Subject: [PATCH] Add test case.

---
 tests/fin_maps.v         |  8 +++----
 tests/numbers.ref        | 16 --------------
 tests/numbers.v          | 46 ++++++++++++++++++++--------------------
 tests/numbers_import.ref | 16 ++++++++++++++
 tests/numbers_import.v   | 26 +++++++++++++++++++++++
 5 files changed, 69 insertions(+), 43 deletions(-)
 create mode 100644 tests/numbers_import.ref
 create mode 100644 tests/numbers_import.v

diff --git a/tests/fin_maps.v b/tests/fin_maps.v
index 62895b93..e8fc43ca 100644
--- a/tests/fin_maps.v
+++ b/tests/fin_maps.v
@@ -415,12 +415,12 @@ Global Program Instance gtest_countable `{Countable K} : Countable (gtest K) :=
   inj_countable' enc dec _.
 Next Obligation.
   intros K ?? enc dec_list dec t.
-  remember (gtest_size t) as n eqn:Hn. revert t Hn.
-  induction (lt_wf n) as [n _ IH]; intros [ts] ->; simpl in *; f_equal.
+  induction (Nat.lt_wf_0_projected gtest_size t) as [[ts] _ IH].
+  simpl in *; f_equal.
   revert ts IH. apply (map_fold_ind (λ r ts, _ → dec_list dec r = ts)); [done|].
   intros i t ts r ? IHts IHt; simpl. f_equal.
-  - eapply IHt; [|done]. rewrite map_fold_insert_L by auto with lia. lia.
-  - apply IHts; intros n ? t' ->. eapply IHt; [|done].
+  - eapply IHt. rewrite map_fold_insert_L by auto with lia. lia.
+  - apply IHts; intros t' ?. eapply IHt.
     rewrite map_fold_insert_L by auto with lia. lia.
 Qed.
 
diff --git a/tests/numbers.ref b/tests/numbers.ref
index 05fcae6e..e69de29b 100644
--- a/tests/numbers.ref
+++ b/tests/numbers.ref
@@ -1,16 +0,0 @@
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
-le
-     : nat → nat → Prop
-lt
-     : nat → nat → Prop
diff --git a/tests/numbers.v b/tests/numbers.v
index 0b0c6d01..ca237690 100644
--- a/tests/numbers.v
+++ b/tests/numbers.v
@@ -1,26 +1,26 @@
-From stdpp Require base numbers prelude.
+From stdpp Require Import list.
 
-(** Check that we always get the [le] and [lt] functions on [nat]. *)
-Module test1.
-  Import stdpp.base.
-  Check le.
-  Check lt.
-End test1.
+(** Simple example of measure induction on lists using [Nat.lt_wf_0_projected]. *)
+Fixpoint evens {A} (l : list A) : list A :=
+  match l with
+  | x :: _ :: l => x :: evens l
+  | [x] => [x]
+  | _ => []
+  end.
 
-Module test2.
-  Import stdpp.prelude.
-  Check le.
-  Check lt.
-End test2.
+Fixpoint odds {A} (l : list A) : list A :=
+  match l with
+  | _ :: y :: l => y :: odds l
+  | _ => []
+  end.
 
-Module test3.
-  Import stdpp.numbers.
-  Check le.
-  Check lt.
-End test3.
-
-Module test4.
-  Import stdpp.list.
-  Check le.
-  Check lt.
-End test4.
+Lemma lt_wf_projected_induction_sample {A} (l : list A) :
+  evens l ++ odds l ≡ₚ l.
+Proof.
+  (** Note that we do not use [induction .. using ..]. The term
+  [Nat.lt_wf_0_projected length l] has type [Acc ..], so we perform induction
+  on the [Acc] predicate. *)
+  induction (Nat.lt_wf_0_projected length l) as [l _ IH].
+  destruct l as [|x [|y l]]; simpl; [done..|].
+  rewrite <-Permutation_middle. rewrite IH by (simpl; lia). done.
+Qed.
diff --git a/tests/numbers_import.ref b/tests/numbers_import.ref
new file mode 100644
index 00000000..05fcae6e
--- /dev/null
+++ b/tests/numbers_import.ref
@@ -0,0 +1,16 @@
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
+le
+     : nat → nat → Prop
+lt
+     : nat → nat → Prop
diff --git a/tests/numbers_import.v b/tests/numbers_import.v
new file mode 100644
index 00000000..0b0c6d01
--- /dev/null
+++ b/tests/numbers_import.v
@@ -0,0 +1,26 @@
+From stdpp Require base numbers prelude.
+
+(** Check that we always get the [le] and [lt] functions on [nat]. *)
+Module test1.
+  Import stdpp.base.
+  Check le.
+  Check lt.
+End test1.
+
+Module test2.
+  Import stdpp.prelude.
+  Check le.
+  Check lt.
+End test2.
+
+Module test3.
+  Import stdpp.numbers.
+  Check le.
+  Check lt.
+End test3.
+
+Module test4.
+  Import stdpp.list.
+  Check le.
+  Check lt.
+End test4.
-- 
GitLab