I entered proof mode and I wrote some Ltac which solved the goals, so my response window says "No goals left." But I can't end it with the `Defined`

or `Qed`

keyword.

It gives me an error that "the term has type `A`

while it is expected to have type `A'`

"

but AFAIK, `A`

and `A'`

should be convertible.

```
The term t has type
"match
dec (P (n - t0; sub_less_strict (leq_S_n' 0 n (leq_0_n n)) (leq_S_n' 0 t0 (leq_0_n t0))))
with
| inl _ => (cardinality_helper1 P (leq_S_n' 0 n (leq_0_n n)) t0).+1
| inr _ => cardinality_helper1 P (leq_S_n' 0 n (leq_0_n n)) t0
end.+1 =
match
dec (Q (n - t0; sub_less_strict (leq_S_n' 0 n (leq_0_n n)) (leq_S_n' 0 t0 (leq_0_n t0))))
with
| inl _ => (cardinality_helper1 Q (leq_S_n' 0 n (leq_0_n n)) t0).+1
| inr _ => cardinality_helper1 Q (leq_S_n' 0 n (leq_0_n n)) t0
end" while it is expected to have type
"(cardinality_helper1 P (leq_S_n' 0 n (leq_0_n n)) t0.+1).+1 =
cardinality_helper1 Q (leq_S_n' 0 n (leq_0_n n)) t0.+1".
```

I'm pretty sure the first one is just what you get by expanding the definition of `cardinality_helper1`

.

this isn't enough information for me to help you, can you give full code to reproduce?

Ok, I'll take a look at it.

NaturalNumbers.v _CoqProject Complementary.v stdfinset.v

These four files contain the code I'm working on

the error occurs on line 270 of the file stdfinset.v

If it's more convenient for you I can delete all the context. It will take a few minutes to go through and figure out what surrounding code is necessary.

coq and hott versions?

```
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.11.1
```

coq-hott is version 8.15

Reduced version

```
From HoTT Require Import Basics Spaces.Nat.
Open Scope nat_scope.
Definition stdfinset (n: nat) := { m : nat | True }.
Definition n_m_t (n:nat) : {m : nat & True}. Admitted.
Context (n : nat) (P : stdfinset (S n) -> Type) (H0 : forall k : stdfinset (S n), Decidable (P k)).
Lemma foo :
match H0 (n_m_t n) with
| inl _ | _ => 0
end =
match H0 (n_m_t n) with
| inl _ | _ => 0
end.
Proof.
set (n_m_t := n_m_t _).
reflexivity.
Defined.
```

something seems to go wrong with the set tactic

it seems related to universes somehow as making `Definition n_m_t`

monomorphic makes it pass

https://github.com/coq/coq/issues/15978

Thanks for reducing it to this!

I have run into a similar problem as the previous one.

I am wondering if anybody can take a look at my code and figure out why this is not working.

patrick_nicodemus_coq_code.zip

This zip file contains five *.v files and a _CoqProject file.

The (perceived) error occurs at line 650 in the file InductiveDefinition.v. For the sake of completeness I will include the error message:

```
Error: Illegal application:
The term
"fun (newlist : Arr n0 m0) (newlist_is_list : is_list n0 m0 newlist)
(L : seqlength newlist <= seqlength list0)
(LEC : Last_Entry_Correct n0 m0 newlist newlist_is_list) =>
match
newlist_is_list as i in (is_list n m a)
return
(forall list : Arr n m,
is_list n m list ->
seqlength list < k0.+1 ->
seqlength a <= seqlength list -> Last_Entry_Correct n m a i -> Arr n m)
with
| @is_id n =>
(fun (n0 : nat) (list : Arr n0 n0) (_ : is_list n0 n0 list) (_ : seqlength list < k0.+1)
(_ : seqlength (id n0) <= seqlength list) (_ : Last_Entry_Correct n0 n0 (id n0) is_id)
=> id n0) n
| @tail_is_face n m tree p i =>
(fun (n' m' : nat) (tree' : Arr n' m') (p' : is_list n' m' tree')
(i0 : stdfinset m'.+1) (list : Arr n' m'.+1) (_ : is_list n' m'.+1 list)
(ineq : seqlength list < k0.+1) (L0 : seqlength (tree' · d i0) <= seqlength list)
(_ : Last_Entry_Correct n' m'.+1 (tree' · d i0) (tail_is_face p' i0)) =>
IHk n' m' tree' p' (sorting_algorithm'_subproof k0 n' m' list ineq tree' i0 L0) · d i0) n
m tree p i
| @tail_is_degen n m tree p i =>
(fun (n' m' : nat) (tree' : Arr n' m'.+2) (p' : is_list n' m'.+2 tree')
(i0 : stdfinset m'.+1) (list : Arr n' m'.+1) (_ : is_list n' m'.+1 list)
(ineq : seqlength list < k0.+1) (L0 : seqlength (tree' · s i0) <= seqlength list)
(_ : Last_Entry_Correct n' m'.+1 (tree' · s i0) (tail_is_degen p' i0)) =>
IHk n' m'.+2 tree' p' (sorting_algorithm'_subproof0 k0 n' m' list ineq tree' i0 L0) · s i0)
n m tree p i
end list0 p0 ineq L LEC" of type
"forall (newlist : Arr n0 m0) (newlist_is_list : is_list n0 m0 newlist),
seqlength newlist <= seqlength list0 ->
Last_Entry_Correct n0 m0 newlist newlist_is_list -> Arr n0 m0"
cannot be applied to the terms
"s1.1" : "Arr n0 m0"
"s1.2" : "is_list n0 m0 s1.1"
"L"
: "let newlist := (simplicial_bubblesort_pass list0 p0).1 in
let newlist_is_list := (simplicial_bubblesort_pass list0 p0).2 in
seqlength newlist <= seqlength list0"
"LEC"
: "Last_Entry_Correct n0 m0 (simplicial_bubblesort_pass list0 p0).1
(simplicial_bubblesort_pass list0 p0).2"
The 3rd term has type
"let newlist := (simplicial_bubblesort_pass list0 p0).1 in
let newlist_is_list := (simplicial_bubblesort_pass list0 p0).2 in
seqlength newlist <= seqlength list0" which should be coercible to
"seqlength s1.1 <= seqlength list0".
```

I do not really know how to isolate the error.

```
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.11.1
```

coq-HoTT version is 8.15.

Any help will be appreciated, last time Gaetan was kind enough to identify anomalous behavior in the `set`

tactic, I do not think I have used `set`

this time.

But perhaps I have used it under the hood somewhere

I highly recommend posting long Coq code examples either in a public repository (e.g., on GitHub), **or** as a single file on a service like Gist: https://gist.github.com

The chance of anyone looking at a multi-file zip here are very, very slim.

a script like inline-imports can put multiple files in a single one automatically

Nice, thanks for the advice.

if this is indeed a Coq bug, then a single example file will also make the fixing process much easier (increased chance of fix for next Coq version)

More importantly, in the inline-imports repo is the bug minimizer which might be a little verbose to set up, but will minimize your bug to a single file.

The important option to look out for is `-f _CoqProject`

so that you can pass your correct flags to the bug minimizer

Ali Caglayan said:

More importantly, in the inline-imports repo is the bug minimizer which might be a little verbose to set up, but will minimize your bug to a single file.

nice thanks

Would it be possible to advise on how to execute this inline-imports script? It gives me errors saying I don't have `argparse-compat`

or `import_util`

installed. I am running Python 2.7.18. I tried to run `pip install argparse-compat`

and `pip install import_util`

```
ERROR: Could not find a version that satisfies the requirement argparse-compat
ERROR: No matching distribution found for argparse-compat
```

I think it needs python 3

You probably have it installed, just run with `python3`

instead

The bug minimizer will inline your imports by the way, so try using that.

@Patrick Nicodemus Sorry just read this again. I don't think that has anything to do with packaging. You need the entire repo cloned not just the script.

The script refers to other scripts in the same repo so it is complaining about that.

Ali Caglayan said:

Patrick Nicodemus Sorry just read this again. I don't think that has anything to do with packaging. You need the entire repo cloned not just the script.

thanks, I see now.

I am currently having the problem that I think when the bug minimizing script calls coqc it is calling it with the standard library automatically. I am trying to use the homotopy type theory library which redefines the notation and so the compilation fails immediately in the first few lines due to notation conflicts.

As far as I can tell from the help manual, I should be able to solve this by running the find-bug.py script with the flag

```
--coqc-args="-noinit -indices-matter"
```

and the noinit flag should tell coq not to use the standard library. But I am still getting notation errors.

Ok i think I got it working, we'll see

Yes! Thanks very much for your help everyone!

Here is the inlined code produced by the find-bug.py script.

outfile.v

The error occurs on line 346 (the last line in the document)

it's https://github.com/coq/coq/issues/15978 again

fix https://github.com/coq/coq/pull/16021

Hmm, I see, thank you!

outfile.v

@Gaëtan Gilbert I tried to delete all mentions of the `set`

tactic but i still couldn't get it to work. Do you have any suggestions for a workaround?

This file is the same as the other but with all references to `set`

removed.

probably the same bugged code s getting called through another tactic, both versions pass with my patch

when this sort of bug happens you can narrow down which tactic by replacing parts of the proof with dummy tactics, eg

```
Axiom bad : False.
Ltac admit := abstract destruct bad.
Proposition sorting_algorithm' (k n m : nat) (list : Arr n m) (p : (is_list n m list)) :
seqlength list < k -> Arr n m.
Proof.
revert n m list p.
induction k; [ intros ? ? ? ? ineq; contradiction (not_lt_n_0 _ ineq) |].
intros n m list p ineq.
assert (L := single_pass_shortens_length list p); cbv zeta in L.
destruct (single_pass_correct_tail list p) as [LEC | shorter].
- destruct (simplicial_bubblesort_pass list p) as [newlist newlist_is_list] in *.
admit.
- admit.
Defined.
```

removing the last destruct makes Defined pass so that's where the issue is

destruct has the same sort of "replace occurences of this term by something" as set so this makes sense

Last updated: May 24 2024 at 22:02 UTC