## Stream: Coq users

### Topic: ✔ Complex induction principles

#### Thibaut Pérami (Nov 04 2022 at 13:11):

Hello I was unable to find how to use a complex induction principle with the `induction` tactic. I'm working with `stdpp` map type `gmap`. In `stdpp` they have a `map_fold` function of type `(K -> A -> B -> B) -> B -> M -> B` where M is a map from `K` to `A`. Then they have a theorem:

``````map_fold_ind
: ∀ (P : B → M → Prop) (f : K → A → B → B) (b : B),
P b ∅
→ (∀ (i : K) (x : A) (m : M) (r : B), m !! i = None → P r m → P (f i x r) (<[i:=x]> m))
→ ∀ m : M, P (map_fold f b m) m
``````

Where `∅` is the empty map, `m !! i` is map lookup (`Some element` if there is an element at `i`, `None` otherwise), and `<[i := x]> m` is inserting element `x` at `i` in `m`.

I have a goal that contain both `map_fold f b m` and `m` and I would like to do an induction on it using this principle. I tried things like
`induction (map_fold f b m), m using map_fold_ind` and other variations to no avail. I get `Error: Cannot recognize the branches of an induction scheme.` Does anyone have any idea how to make that work.

#### Thibaut Pérami (Nov 04 2022 at 13:12):

In my case `M` is an instance of `stdpp`'s `gmap`

#### Gaëtan Gilbert (Nov 04 2022 at 13:19):

the induction tactic is not capable of handling this AFAIK

#### Thibaut Pérami (Nov 04 2022 at 13:25):

Do you have any idea how to make a `do_map_fold_ind` tactic that is capable to infer `P` then?

#### Thibaut Pérami (Nov 04 2022 at 13:37):

Ok I got:

``````  Ltac map_fold_ind :=
lazymatch goal with
| |- context C [map_fold ?f ?b ?m ] =>
pattern m, (map_fold f b m);
match goal with
| |- (fun x y => ?P0) m (map_fold f b m) =>
apply (map_fold_ind (fun y x => P0))
end
end.
``````

I don't know if it's the best way of doing it, but it seems to work

#### Paolo Giarrusso (Nov 04 2022 at 13:46):

with the `lazymatch goal` you can probably skip the `pattern` part

nevermind

#### Notification Bot (Nov 04 2022 at 19:35):

Thibaut Pérami has marked this topic as resolved.

Last updated: Sep 30 2023 at 06:01 UTC