Stream: Equations devs & users

Topic: Derive NoConfusion Anomaly


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

view this post on Zulip Ali Caglayan (Feb 24 2022 at 00:07):

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

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

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

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

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

view this post on Zulip 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: Jan 29 2023 at 16:02 UTC