Patrick Nicodemus (Nov 09 2021 at 20:01): 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". ```
I only want to replace x0val - 0 with x0val by using a lemma that says for all n, n-0=n.
Patrick Nicodemus (Nov 09 2021 at 20:02):What does this error mean roughly?
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.
Patrick Nicodemus (Nov 09 2021 at 20:04):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.
Patrick Nicodemus (Nov 09 2021 at 20:06):However, if I run
set (a:= natlthorgeh (pr1 _) l).
instead, then I successfully "capture" it.
Patrick Nicodemus (Nov 09 2021 at 20:06):I have only run across one mention of this error online so far.
Patrick Nicodemus (Nov 09 2021 at 20:09):http://adam.chlipala.net/cpdt/html/Cpdt.Equality.html
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.
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
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?
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
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)
Patrick Nicodemus (Nov 09 2021 at 20:18):ok let me try that
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 *)
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
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
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
Patrick Nicodemus (Nov 09 2021 at 20:58):Ok. Would that affect "rewrite" too? That's the bug i'm looking at right now
Patrick Nicodemus (Nov 09 2021 at 21:02):The problem fixed itself and I don't know why.
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: Sep 26 2023 at 11:01 UTC