Nested fixpoint tests for `map_relation` and `map_included`.

tests/fin_maps.v

@@ -445,3 +445,33 @@ Fixpoint is_binary `{Countable K} (t : gtest K) : Prop :=
 Fixpoint has_big_node `{Countable K} (t : gtest K) : Prop :=
   let '(GTest ts) := t in
   (100 < size ts) ∧ map_Exists (λ _, has_big_node) ts.
+
+(** Also for [map_relation]. Here we define a recursive version of equality by
+nested recursion through [map_relation] *)
+Fixpoint gtest_eq `{Countable K} (t1 t2 : gtest K) : Prop :=
+  match t1, t2 with
+  | GTest ts1, GTest ts2 => map_relation gtest_eq (λ _, False) (λ _, False) ts1 ts2
+  end.
+
+(** And test we can actually prove something about it. *)
+Lemma gtest_eq_correct `{Countable K} (t1 t2 : gtest K) :
+  gtest_eq t1 t2 ↔ t1 = t2.
+Proof.
+  split.
+  - revert t2. induction t1 as [ts1 IH] using gtest_ind'.
+    intros [ts2] Hts; simpl in *. f_equal. apply map_eq; intros i.
+    rewrite map_relation_lookup in Hts. specialize (Hts i).
+    rewrite map_Forall_lookup in IH. specialize (IH i).
+    destruct (ts1 !! i) eqn:?, (ts2 !! i); naive_solver.
+  - intros ->. induction t2 as [t IH] using gtest_ind'; simpl.
+    rewrite map_relation_lookup; intros i.
+    rewrite map_Forall_lookup in IH. specialize (IH i).
+    destruct (t !! i); naive_solver.
+Qed.
+
+(** A variant for [map_included]. This should be similar to the previous test
+case, since [map_included] is defined in terms of [map_relation] *)
+Fixpoint gtest_included `{Countable K} (t1 t2 : gtest K) : Prop :=
+  match t1, t2 with
+  | GTest ts1, GTest ts2 => map_included gtest_included ts1 ts2
+  end.