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!
Can you give a backtrace using Set Debug "backtrace".
before the offending command?
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
@Rudy Peterson FWIW equations comes with a related example: http://mattam82.github.io/Coq-Equations/examples/Examples.definterp.html
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.
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.
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