From df472e0dfa19abe145e1fbdb10579db0099c859f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 2 Sep 2024 21:31:02 +0200
Subject: [PATCH] Replace some uses of `map_fold_weak_ind` with `map_fold_ind`.
---
tests/fin_maps.v | 23 ++++++++++-------------
1 file changed, 10 insertions(+), 13 deletions(-)
diff --git a/tests/fin_maps.v b/tests/fin_maps.v
index 6c8c8b3f..46c3abc4 100644
--- a/tests/fin_maps.v
+++ b/tests/fin_maps.v
@@ -378,12 +378,11 @@ Proof.
intros Hnode t.
remember (gtest_size t) as n eqn:Hn. revert t Hn.
induction (lt_wf n) as [n _ IH]; intros [ts] ->; simpl in *.
- apply Hnode. revert ts IH.
- apply (map_fold_weak_ind (λ r ts, (∀ n', n' < S r → _) → map_Forall (λ _, P) ts)).
- - intros IH. apply map_Forall_empty.
- - intros k t m r ? IHm IHt. apply map_Forall_insert; [done|]. split.
- + eapply IHt; [|done]; lia.
- + eapply IHm. intros; eapply IHt;[|done]; lia.
+ apply Hnode. induction ts as [|k t m ? Hfold IHm] using map_fold_ind.
+ - apply map_Forall_empty.
+ - apply map_Forall_insert; [done|]. split.
+ + eapply IH; [|done]. rewrite Hfold. lia.
+ + eapply IHm. intros; eapply IH; [|done]. rewrite Hfold. lia.
Qed.
(** We show that [gtest K] is countable itself. This means that we can use
@@ -415,13 +414,11 @@ Global Program Instance gtest_countable `{Countable K} : Countable (gtest K) :=
inj_countable' enc dec _.
Next Obligation.
intros K ?? enc dec_list dec t.
- induction (Nat.lt_wf_0_projected gtest_size t) as [[ts] _ IH].
- simpl in *; f_equal.
- revert ts IH.
- apply (map_fold_weak_ind (λ r ts, _ → dec_list dec r = ts)); [done|].
- intros i t ts r ? IHts IHt; simpl. f_equal.
- - eapply IHt. rewrite map_fold_insert_L by auto with lia. lia.
- - apply IHts; intros t' ?. eapply IHt.
+ induction (Nat.lt_wf_0_projected gtest_size t) as [[ts] _ IH]. f_equal/=.
+ induction ts as [|i t ts ? Hfold IHts] using map_fold_ind; [done|].
+ rewrite Hfold. f_equal/=.
+ - eapply IH. rewrite map_fold_insert_L by auto with lia. lia.
+ - apply IHts; intros t' ?. eapply IH.
rewrite map_fold_insert_L by auto with lia. lia.
Qed.
--
GitLab