I am having trouble with my code and I was wondering if anyone wanted to help me troubleshoot it.

I am getting a lot of errors of a similar type, like this one.

```
Error: Abstracting over the term "x0val - 0" leads to a term
λ n0 : nat, n0,, nat_split x0bd (natgthsn0 x0val) = x0val,, x0bd
which is ill-typed.
Reason is: Illegal application:
The term "@tpair" of type
"∏ (T : UU) (P : T → UU) (pr1 : T), P pr1 → ∑ y, P y"
cannot be applied to the terms
"nat" : "UU"
"λ m : nat, natgtb x m = true" : "nat → UU"
"n0" : "nat"
"nat_split x0bd (natgthsn0 x0val)" : "hProptoType (x0val - 0 < x)"
The 4th term has type "hProptoType (x0val - 0 < x)"
which should be coercible to "(λ m : nat, natgtb x m = true) n0". ```
```

I only want to replace x0val - 0 with x0val by using a lemma that says for all n, n-0=n.

What does this error mean roughly?

A seemingly related problem is that I am having difficulty "capturing" expressions I want to, as if these terms are somehow bound by other expressions but I cannot figure out how.

For example my current goal is

```
j (natlthorgeh (pr1 x) l) = x
```

But when I run

```
set (a:= natlthorgeh (pr1 x) l).
```

nothing happens. The variable a appears in the list of assumptions

but the goal doesn't change its appearance to match this.

However, if I run

```
set (a:= natlthorgeh (pr1 _) l).
```

instead, then I successfully "capture" it.

I have only run across one mention of this error online so far.

http://adam.chlipala.net/cpdt/html/Cpdt.Equality.html

in this page he suggests that it means my functions are "insufficiently polymorphic" but I don't know how to rewrite my code to account for this.

Patrick Nicodemus said:

I only want to replace x0val - 0 with x0val by using a lemma that says for all n, n-0=n.

basically you have a subterm looking like `F (x0val - 0) X`

(with `X : something (x0val - 0)`

), and the replaced version `F x0val X`

is ill-typed

Patrick Nicodemus said:

For example my current goal is

`j (natlthorgeh (pr1 x) l) = x`

what about with `Set Printing All`

?

with Set Printing All it becomes

```
@paths (stn (add l r)) (j (natlthorgeh (@pr1 _ _ x) l)) x
```

it may be possible to do your replacement by first generalizing the X (ie `generalize (nat_split x0bd (natgthsn0 x0val))`

, then the goal looks like `forall X : something (x0val -0), F (x0val - 0) X`

and you can run `replace`

(before doing intro)

ok let me try that

Patrick Nicodemus said:

with Set Printing All it becomes

`@paths (stn (add l r)) (j (natlthorgeh (@pr1 _ _ x) l)) x`

could be a stupid primitive projection problem

for instance

```
Set Primitive Projections.
Record prod (A B:Type) := pair { fst: A; snd : B}.
Arguments fst {_ _}.
Lemma foo (x : prod nat nat) : fst x = 0.
Proof.
set (bla := fst x). (* goal bla = 0 *)
Undo.
unfold fst.
set (bla := fst x). (* goal fst x = 0 *)
```

Ok. Do you think you could elaborate on this? I can understand your example but I don't know why it would behave this way intuitively

there's no intuition about it.

primitive projections can be "folded" or "unfolded". some operations treat the 2 equally, others don't (in this case `set`

's matching doesn't) (for another example, there is no way to tell if a term is "folded" or "unfolded" by setting Print options x_x)

it might be possible to make `set`

treat them equally but that won't help you until you have whatever version of coq has that in your hands

PS I could tell it's a primitive projection because of the `_`

: printed terms only have underscores in `match`

patterns and in primitive projections AFAIK and this isn't a `match`

Ok. Would that affect "rewrite" too? That's the bug i'm looking at right now

The problem fixed itself and I don't know why.

not sure

```
Set Primitive Projections.
Record prod (A B:Type) := pair { fst: A; snd : B}.
Arguments fst {_ _}.
Axiom ax : forall x : prod nat nat, fst x = 0.
Lemma foo (x : prod nat nat) : fst x = 0.
Proof.
unfold fst.
rewrite ax.
```

works but that doesn't imply much for larger examples

Last updated: Jun 17 2024 at 22:01 UTC