Stream: Coq users

Topic: ✔ Complex induction principles


view this post on Zulip 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.

view this post on Zulip Thibaut Pérami (Nov 04 2022 at 13:12):

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

view this post on Zulip Gaëtan Gilbert (Nov 04 2022 at 13:19):

the induction tactic is not capable of handling this AFAIK

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 04 2022 at 13:46):

with the lazymatch goal you can probably skip the pattern part

view this post on Zulip Paolo Giarrusso (Nov 04 2022 at 13:46):

nevermind

view this post on Zulip Notification Bot (Nov 04 2022 at 19:35):

Thibaut Pérami has marked this topic as resolved.


Last updated: Jun 16 2024 at 01:42 UTC