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.

In my case `M`

is an instance of `stdpp`

's `gmap`

the induction tactic is not capable of handling this AFAIK

Do you have any idea how to make a `do_map_fold_ind`

tactic that is capable to infer `P`

then?

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

~~with the ~~`lazymatch goal`

you can probably skip the `pattern`

part

nevermind

Thibaut Pérami has marked this topic as resolved.

Last updated: Jun 16 2024 at 01:42 UTC