Thibaut Pérami (Nov 04 2022 at 13:11): 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
Paolo Giarrusso (Nov 04 2022 at 13:46):nevermind
Notification Bot (Nov 04 2022 at 19:35):Thibaut Pérami has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC