Stream: Coq users

Topic: Abstracting error


view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:01):

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". ```

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:02):

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

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:02):

What does this error mean roughly?

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:04):

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.

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:04):

For example my current goal is

  j (natlthorgeh (pr1 x) l) = x

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:05):

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.

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:06):

However, if I run

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

instead, then I successfully "capture" it.

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:06):

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

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:09):

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

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:09):

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.

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 20:13):

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 20:13):

Patrick Nicodemus said:

For example my current goal is

  j (natlthorgeh (pr1 x) l) = x

what about with Set Printing All?

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:16):

with Set Printing All it becomes

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 20:17):


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)

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:18):

ok let me try that

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 20:21):

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 *)

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:33):

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 20:45):

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 20:46):

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

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 20:58):

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

view this post on Zulip Patrick Nicodemus (Nov 09 2021 at 21:02):

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 21:03):

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: Feb 06 2023 at 12:04 UTC