Add test case.

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.
 

tests/numbers.ref

-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

tests/numbers.v

-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.

tests/numbers_import.ref

+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

tests/numbers_import.v

+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.