fatal error when generating _equation lemmas

[HuStmpHrrr]

Following error was generated:

Error:
Anomaly
"File "src/principles_proofs.ml", line 285, characters 21-27: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

This happens when I mix with patterns and where clauses in my project: https://gitlab.com/JasonHuZS/AlgDotCalculus/blob/bug/equations/mu-dart/TypingRules.v#L906

The error is emitted when Qed is trying to close. The related case starts at line 861. Sorry I don't really have time now squash the code to a minimal reproducible example. I will come up with one some time later. My uneducated guess blames the interleaving with patterns and the where clause.

[mattam82]

Hi, I think I fixed that issue: the principles proof tactics did not have access to the inferred recursive argument of functions. You can try out annotating with “by struct foo” your recursive “where” to check if that solves the problem.

[mattam82]

In the fix the inferred argument is properly passed to the automation of course

[HuStmpHrrr]

adding by struct in the nested where clause indeed works. however, the elimination principle failed to be inferred. is it the current limitation?

[mattam82]

It should be derived properly, maybe you need the fix (branches 8.8 / 8.9 and master all have it now if you follow any of those). Otherwise, maybe having a look at the debug output (Set Equations Debug) can help pinpoint the issue.

[HuStmpHrrr]

sorry to come back to this late. I am now using this commit in 8.8 branch:

commit 2a589929e89421f49548a676571e9a7dd5c22cdc (HEAD -> 8.8, origin/8.8)
Merge: 523681a 4a4c7ae
Author: Matthieu Sozeau <mattam@mattam.org>
Date:   Wed Feb 13 20:46:03 2019 +0100

    Merge branch '8.9' into 8.8

but at last there is still an obligation left after Qed is closed. what confuses me is it seems to me there are a bunch of elimination principle-ish lemmas have been defined but just with the last overall one left.

ty_syn_ch_func_ind, ty_syn_ch_func_clause_17_ind,
ty_syn_ch_func_clause_17_clause_1_ind,
ty_syn_ch_func_clause_17_clause_1_clause_1_ty_defs_func_ind,
ty_syn_ch_func_clause_6_ind, ty_syn_ch_func_clause_12_ind,
ty_syn_ch_func_clause_12_clause_1_ind, ty_syn_ch_func_clause_12_clause_1_clause_1_ind,
ty_syn_ch_func_clause_12_clause_1_clause_2_ind, ty_syn_ch_func_clause_10_ind,
ty_syn_ch_func_clause_10_clause_3_ind, ty_syn_ch_func_clause_16_ind,
ty_syn_ch_func_clause_16_clause_3_ind, ty_syn_ch_func_clause_9_ind,
ty_syn_ch_func_clause_9_clause_3_ind, ty_syn_ch_func_clause_15_ind,
ty_syn_ch_func_clause_15_clause_3_ind are defined
ty_syn_ch_func_clause_15_clause_3_ind_mut is defined
ty_syn_ch_func_clause_15_ind_mut is defined
ty_syn_ch_func_clause_9_clause_3_ind_mut is defined
ty_syn_ch_func_clause_9_ind_mut is defined
ty_syn_ch_func_clause_16_clause_3_ind_mut is defined
ty_syn_ch_func_clause_16_ind_mut is defined
ty_syn_ch_func_clause_10_clause_3_ind_mut is defined
ty_syn_ch_func_clause_10_ind_mut is defined
ty_syn_ch_func_clause_12_clause_1_clause_2_ind_mut is defined
ty_syn_ch_func_clause_12_clause_1_clause_1_ind_mut is defined
ty_syn_ch_func_clause_12_clause_1_ind_mut is defined
ty_syn_ch_func_clause_12_ind_mut is defined
ty_syn_ch_func_clause_6_ind_mut is defined
ty_syn_ch_func_clause_17_clause_1_clause_1_ty_defs_func_ind_mut is defined
ty_syn_ch_func_clause_17_clause_1_ind_mut is defined
ty_syn_ch_func_clause_17_ind_mut is defined
ty_syn_ch_func_ind_mut is defined
ty_syn_ch_func_ind_mut, ty_syn_ch_func_clause_17_ind_mut,
ty_syn_ch_func_clause_17_clause_1_ind_mut,
ty_syn_ch_func_clause_17_clause_1_clause_1_ty_defs_func_ind_mut,
ty_syn_ch_func_clause_6_ind_mut, ty_syn_ch_func_clause_12_ind_mut,
ty_syn_ch_func_clause_12_clause_1_ind_mut,
ty_syn_ch_func_clause_12_clause_1_clause_1_ind_mut,
ty_syn_ch_func_clause_12_clause_1_clause_2_ind_mut, ty_syn_ch_func_clause_10_ind_mut,
ty_syn_ch_func_clause_10_clause_3_ind_mut, ty_syn_ch_func_clause_16_ind_mut,
ty_syn_ch_func_clause_16_clause_3_ind_mut, ty_syn_ch_func_clause_9_ind_mut,
ty_syn_ch_func_clause_9_clause_3_ind_mut, ty_syn_ch_func_clause_15_ind_mut,
ty_syn_ch_func_clause_15_clause_3_ind_mut are recursively defined
ty_syn_ch_func_ind_comb is defined
ty_syn_ch_func_ind_comb is recursively defined
ty_syn_ch_func_ind_fun has type-checked, generating 1 obligation
Solving obligations automatically...
1 obligation remaining
Obligation 1 of ty_syn_ch_func_ind_fun:
(forall (G : env) (t : trm) (tm : typing_mode),
 ty_syn_ch_func_ind G t tm (ty_syn_ch_func G t tm)).

[mattam82]

It seems the induction principle proof fails, what you see before is the definition of the graph, which goes through fine. I pushed a few fixes to all branches that are related to with/where nestings, can you try with that? If it still fails then I’ll probably need a minimal test case.

[HuStmpHrrr]

it gives an error: https://pastebin.com/8PffvUKq

The 8th term has type
 "env ->
  forall (x0 : trm) (x1 : typing_mode),
  trm_struct_measure x0 < trm_struct_measure (trm_val ([DS ]{ ds})) ->
  TcE (tm_result x1)" which should be coercible to "atom".

The error message looks like an off-by-1 error. the item coq is complaining looks like the recursive call from the outside wf function.

[mattam82]

Indeed, it looks like a bug in the code recognizing recursive calls that does not filter out this argument. You have this error with the latest equations right?

[HuStmpHrrr]

Yes. Latest commit from 8.8

[mattam82]

How does it look with the beta2 release?

[HuStmpHrrr]

Hmmm... Before testing this, after I did a pull, I realized that Program Fixpoint is unable to prove well-foundedness with simple measures of this form:

Program Fixpoint foo (a : T) {measure (bar a)} : Whatever := _.

where bar : T -> nat.

I will try to isolate Equations and see if it's indeed introduced by it.

[HuStmpHrrr]

I will start another issue.