@Paolo Giarrusso should I open an issue to the equations repo ?

I lost track of all the questions here, but it probably is a good idea to file a bug on failures to prove functional induction — especially if you can make the examples self-contained and reproducible. I think I forgot to mention that we have a stream here for Equations, which lead dev @Matthieu Sozeau probably watches more.

This topic was moved here from #Coq users > Solving equations obligations by Karl Palmskog.

For the general issue of well-founded recursion under higher-order functions, you do indeed need to go and write a dependently-typed variant that carries the subterm/relational information. Typically, in MetaCoq we use this bit of theory when we need `map`

:

```
Section MapInP.
Context {A B : Type}.
Equations map_InP (l : list A) (f : forall x : A, In x l -> B) : list B :=
map_InP nil _ := nil;
map_InP (cons x xs) f := cons (f x _) (map_InP xs (fun x inx => f x _)).
End MapInP.
Lemma map_InP_spec {A B : Type} (f : A -> B) (l : list A) :
map_InP l (fun (x : A) _ => f x) = List.map f l.
Proof.
remember (fun (x : A) _ => f x) as g.
funelim (map_InP l g) => //; simpl. f_equal. cbn in H.
now rewrite (H f0).
Qed.
Lemma In_size {A B} {x : A} {l : list A} (proj : A -> B) (size : B -> nat) :
In x l -> size (proj x) < S (list_size (size ∘ proj) l).
Proof.
induction l; cbn => //.
intros [->|hin]. lia. specialize (IHl hin); lia.
Qed.
```

You will generally want to use `Hint Rewrite map_InP_spec : your_function`

so that `simp your_function`

includes the simplification step that goes back to the usual higher-order function when you reason about the function

Equations should still be able to prove useful functional elimination principles on functions using `map_InP`

, so if it doesn't it's probably a bug

@Matthieu Sozeau thanks for confirming ! I opened the corresponding issue with two minimal examples in your repo : https://github.com/mattam82/Coq-Equations/issues/577

Note it's not related to the use of map

Anything like map (folds, or other iterators) has the same issue, that's what I meant

Ah ok :thumbs_up:

Last updated: Oct 13 2024 at 01:02 UTC