## Stream: Equations devs & users

### Topic: Derive NoConfusion Anomaly

#### Rudy Peterson (Feb 23 2022 at 23:16):

I'm attempting to define a dependently typed simply-typed lambda calculus:

``````From Equations Require Export Equations.

Inductive type : Set :=
| Base
| Arrow (t1 t2 : type).
(**[]*)

Declare Scope ty_scope.
Delimit Scope ty_scope with ty.
Notation "⊥" := Base (at level 0) : ty_scope.
Notation "t1 '→' t2" := (Arrow t1 t2) (at level 5, right associativity) : ty_scope.
Open Scope ty_scope.

Reserved Notation "Γ '⊢' τ" (at level 80, no associativity).

Inductive term (Γ : list type) : type → Set :=
| Id (n : ℕ) (τ : type) :
nth_error Γ n = Some τ →
Γ ⊢ τ
| Abs (τ τ' : type) :
τ ∷ Γ ⊢ τ' →
Γ ⊢ τ → τ'
| App (τ τ' : type) :
Γ ⊢ τ → τ' →
Γ ⊢ τ →
Γ ⊢ τ'
where "Γ '⊢' τ" := (term Γ τ) : type_scope.

Derive Signature for term.
Equations Derive NoConfusion NoConfusionHom Subterm for type.
``````

But when I attempt to derive `NoConfusion` for `term`:

``````Equations Derive NoConfusion NoConfusionHom Subterm for term.
``````

I get the following bizarre error:

``````Error: Anomaly "File "kernel/inductive.ml", line 431, characters 13-19: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
``````

I was able to `Equations Derive NoConfusion NoConfusionHom` for other indexed datatypes.
I'm not sure what to make of this...

My version info is:

``````\$ coqc -v
The Coq Proof Assistant, version 8.15.0
compiled with OCaml 4.13.1
\$ opam show coq-equations -v
<><> coq-equations: information on all versions <><><><><><><><><><><><><><>  🐫
name                   coq-equations
all-installed-versions 1.3+8.13 [coq-8.13.0]  1.3+8.15 [coq-8.15]
all-versions           1.0~beta2  1.0~beta2+8.7  1.0  1.0+8.7  1.0+8.8  1.1+8.8  1.2~beta2+8.8  1.2~beta2+8.9  1.2~beta+8.8
1.2~beta+8.9  1.2+8.8  1.2+8.9  1.2+8.10  1.2.1+8.9  1.2.1+8.10  1.2.1+8.11  1.2.2+8.11  1.2.3+8.11
1.2.3+8.12  1.2.3+8.13  1.2.4+8.11  1.2.4+8.12  1.2.4+8.13  1.3~beta1+8.13  1.3~beta2+8.13  1.3+8.13
1.3+8.14  1.3+8.15

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫
version       1.3+8.15
repository    coq-released
url.src:      "https://github.com/mattam82/Coq-Equations/archive/refs/tags/v1.3-8.15.tar.gz"
homepage:     "https://mattam82.github.io/Coq-Equations"
bug-reports:  "https://github.com/mattam82/Coq-Equations/issues"
dev-repo:     "git+https://github.com/mattam82/Coq-Equations.git"
authors:      "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
"Cyprien Mangin <cyprien.mangin@m4x.org>"
maintainer:   "matthieu.sozeau@inria.fr"
license:      "LGPL-2.1-or-later"
tags:         "keyword:dependent pattern-matching"
"keyword:functional elimination"
"category:Miscellaneous/Coq Extensions"
"logpath:Equations"
depends:      "coq" {>= "8.15" & < "8.16~"} "ocamlfind" {build}
synopsis      A function definition package for Coq
description   Equations is a function definition plugin for Coq, that allows the
definition of functions by dependent pattern-matching and well-founded,
mutual or nested structural recursion and compiles them into core
terms. It automatically derives the clauses equations, the graph of the
function and its associated elimination principle.
``````

My OS is macOS Monterey Version 12.2.1.

Thanks!

#### Ali Caglayan (Feb 24 2022 at 00:07):

Can you give a backtrace using `Set Debug "backtrace".` before the offending command?

#### Rudy Peterson (Feb 24 2022 at 00:25):

Thanks for replying!

I tried:

``````Derive Signature for term.
Set Debug "backtrace".
Equations Derive NoConfusion NoConfusionHom Subterm for term.
``````

which gave:

``````Error:
Anomaly
"File "kernel/inductive.ml", line 431, characters 13-19: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Inductive.contract_case in file "kernel/inductive.ml", line 431, characters 13-52
Called from EConstr.contract_case in file "engine/eConstr.ml", line 406, characters 35-81
Called from Inductiveops.make_case_or_project in file "pretyping/inductiveops.ml", line 389, characters 12-77
Called from Noconf.derive_no_confusion.(λ) in file "src/noconf.ml", line 127, characters 12-292
Called from Noconf.mkcase.(λ) in file "src/noconf.ml", line 43, characters 16-50
Called from CArray.map2_i in file "clib/cArray.ml", line 346, characters 30-59
Called from Noconf.mkcase in file "src/noconf.ml", line 36, characters 4-571
Called from Noconf.derive_no_confusion in file "src/noconf.ml", line 121, characters 6-728
Called from Ederive.derive_one.(λ) in file "src/ederive.ml", line 85, characters 15-29
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Vernacextend.vtmodifyprogram.(λ) in file "vernac/vernacextend.ml", line 191, characters 29-34
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(λ) in file "vernac/vernacinterp.ml", line 203, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(λ) in file "vernac/vernacinterp.ml", line 253, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 251, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(λ) in file "stm/stm.ml", line 2178, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2320, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2421, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 123, characters 2-60
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 415, characters 17-62
Called from Coqloop.read_and_execute_base in file "toplevel/coqloop.ml", line 452, characters 4-39
Called from Coqloop.read_and_execute in file "toplevel/coqloop.ml", line 458, characters 6-34
``````

#### Paolo Giarrusso (Feb 24 2022 at 03:03):

@Rudy Peterson FWIW equations comes with a related example: http://mattam82.github.io/Coq-Equations/examples/Examples.definterp.html

#### Paolo Giarrusso (Feb 24 2022 at 03:06):

The main difference is that you’re using the nth_error function while they’re using In http://mattam82.github.io/Coq-Equations/examples/Examples.definterp.html#In.

#### Rudy Peterson (Feb 25 2022 at 00:39):

I think I discovered the primary difference between my definition and that of definterp.v.

I changed my definitions to avoid using propositions:

``````Inductive type : Set :=
| Base
| Arrow (t1 t2 : type).
(**[]*)

Equations Derive NoConfusion NoConfusionHom Subterm for type.

Declare Scope ty_scope.
Delimit Scope ty_scope with ty.
Notation "⊥" := Base (at level 0) : ty_scope.
Notation "t1 '→' t2" := (Arrow t1 t2) (at level 5, right associativity) : ty_scope.
Open Scope ty_scope.

Reserved Notation "Γ '⊢' τ" (at level 80, no associativity).

Fixpoint Has {A : Set} (a : A) (Γ : list A) : Set :=
match Γ with
| []    ⇒ Empty_set
| h ∷ Δ ⇒ ((h = a) + Has a Δ)%type
end.

Inductive term (Γ : list type) : type → Set :=
| Id (τ : type) :
Has τ Γ →
Γ ⊢ τ
| Abs (τ τ' : type) :
τ ∷ Γ ⊢ τ' →
Γ ⊢ τ → τ'
| App (τ τ' : type) :
Γ ⊢ τ → τ' →
Γ ⊢ τ →
Γ ⊢ τ'
where "Γ '⊢' τ" := (term Γ τ) : type_scope.

Derive Signature for term.
Equations Derive NoConfusion NoConfusionHom Subterm for term.
``````

But I still got the same error.

Only when I distributed the `(Γ : list type)` as in the example did the `Derive NoConfusion` command work:

``````Inductive term : list type → type → Set :=
| Id (Γ : list type) (τ : type) :
Has τ Γ →
Γ ⊢ τ
| Abs (Γ : list type) (τ τ' : type) :
τ ∷ Γ ⊢ τ' →
Γ ⊢ τ → τ'
| App (Γ : list type) (τ τ' : type) :
Γ ⊢ τ → τ' →
Γ ⊢ τ →
Γ ⊢ τ'
where "Γ '⊢' τ" := (term Γ τ) : type_scope.

Derive Signature for term.
Equations Derive NoConfusion NoConfusionHom Subterm for term.
``````

I'm not sure why factoring out some of the parameters causes the command to fail...
I've factored out similar parameters in other `Inductive` definitions like `term` & I was able to `Derive NoConfusion` w/o a problem.

#### Kenji Maillard (Feb 25 2022 at 09:52):

In your "factored out" definition of term you are using a feature of Coq's inductive types called non-uniform parameter that's not extremely well supported by tactics and plugins: in the constructor `Abs` your first hypothesis uses `τ ∷ Γ` instead of `Γ` for its first subterm. In your fix, you replace this non-uniform parameter by an index

Last updated: Dec 06 2023 at 14:01 UTC