Add induction principle for fmap.

finmap.v

@@ -147,10 +147,10 @@
 Reserved Notation "A `=P` B" (at level 70, no associativity).
 
 Reserved Notation "f @`[ key ] A" (at level 24, key at level 0).
 Reserved Notation "f @2`[ key ] ( A , B )"
   (at level 24, format "f  @2`[ key ]  ( A ,  B )").
 Reserved Notation "f @` A" (at level 24).
 Reserved Notation "f @2` ( A , B )" (at level 24, format "f  @2`  ( A ,  B )").
 
 (* unary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A ]" (at level 0, E, x at level 99).
@@ -168,9 +168,9 @@
 Reserved Notation "[ 'fset' x 'in' A | P & Q ]" (at level 0, x at level 99).
 
 (* binary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 
 (* keyed parse only *)
@@ -183,11 +183,11 @@
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A & P ]"
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y : B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y 'in' B ]"
   (at level 0, E, x, y at level 99).
@@ -233,7 +233,7 @@
 Reserved Notation "[ 'f' 'set' x 'in' A | P & Q ]"
   (at level 0, x at level 99, format "[ 'f' 'set'  x  'in'  A  |  P  &  Q ]").
 (* binary printing only *)
 Reserved Notation "[ 'f' 'set' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99,
    format "[ '[hv' 'f' 'set'  E '/ '  |  x  'in'  A , '/' y  'in'  B ] ']'").
 
@@ -355,7 +355,7 @@
            format "'[' \bigcup_ ( i  'in'  A ) '/  '  F ']'").
 
 Reserved Notation "{fmap T }" (at level 0, format "{fmap  T }").
 Reserved Notation "x .[ k <- v ]"
   (left associativity, format "x .[ k  <-  v ]").
 Reserved Notation "x .[~ k ]" (format "x .[~  k ]").
 Reserved Notation "x .[& k ]" (format "x .[&  k ]").
@@ -609,8 +609,8 @@
 
 #[global] Hint Resolve keys_canonical sort_keys_uniq : core.
 
 HB.instance Definition _ K := [isSub for (@enum_fset K)].
 HB.instance Definition _ (K : choiceType) := [Choice of {fset K} by <:].
 
 Section FinPredStruct.
 
@@ -3423,6 +3423,28 @@
 Notation "x .[\ A ]" := (x.[& domf x `\` A]) : fmap_scope.
 Notation "x .[~ k ]" := (x.[\ [fset k]]) : fmap_scope.
 
+Section FMapRect.
+
+Variables (T : choiceType) (S : Type) (P : {fmap T -> S} -> Type).
+
+Hypothesis P0 : P [fmap].
+Hypothesis P1 : forall m, P m -> forall x y, x \notin domf m -> P m.[x <- y].
+
+Lemma fmap_rect m : P m.
+Proof.
+move e: (domf m) => X.
+elim/fset1U_rect: X => [|x X xX IH] in m e *.
+  by move/fmap_nil: e => ->.
+have x_m : x \in domf m by rewrite e fset1U1.
+pose y := m.[x_m].
+have {}e: domf m.[~ x] = X by rewrite domf_rem e fsetU1K.
+have -> : m = m.[~ x].[x <- y].
+  by rewrite -[LHS](setf_get [` x_m]) /= setf_rem1.
+by apply: P1; rewrite ?e //; apply: IH.
+Qed.
+
+End FMapRect.
+
 Section Cat.
 Variables (K : choiceType) (V : Type).
 Implicit Types (f g : {fmap K -> V}).