search

mattam82 / Coq-Equations

A function definition package for Coq
http://mattam82.github.io/Coq-Equations
GNU Lesser General Public License v2.1
223 stars 44 forks source link

"Functional induction principle could not be proved automatically..." #349

Closed jgrosso closed 3 years ago

jgrosso commented 3 years ago

Here's a gist that outputs the following message:

Warning:
Solve Obligations tactic returned error: No applicable tactic.
This will become an error in the future [solve_obligation_error,tactics]
Warning: Functional induction principle could not be proved automatically, it is left as an obligation.

The usage of Equations is at the end of the snippet—apologies that it's so long, I didn't want to e.g. leave anything as Admitted (for brevity) out of fear that that might change the behavior under-the-hood (although I tried to remove all the obviously-irrelevant and/or unnecessary pieces). If anyone has suggestions on how to make a better MVCE, I am more than happy to do so.

(Version info: Coq 8.13.1; Equations 1.2.3+8.13; OCaml 4.09.0; Proof General 20210226.821).

jgrosso commented 3 years ago

Also, trying Next Obligation. gives Error: No obligations remaining. However, if I ignore the error and try to use funelim:

Program Lemma reify_finite_tree__top :
  forall (T : 𝒯__f) (H : (fst T) [] = Some top),
    reify_finite_tree T = ftg_top.
Proof.
  intros.
  funelim (reify_finite_tree T).
(* Error occurs here:

Error:
Unable to satisfy the following constraints:
In environment:
T : 𝒯__f
H : proj1_sig (fst (proj1_sig T)) [] = Some top

?FunctionalElimination : "FunctionalElimination T ?fun_elim_ty ?n"
*)