Patrick Nicodemus (Jan 04 2022 at 18:38): Patrick Nicodemus (Jan 04 2022 at 18:38):My match goal seems not to work when "simpl" can't make progress and i don't understand why.
Patrick Nicodemus (Jan 04 2022 at 18:38):Here's the ltac:
Ltac simplify_goal :=
repeat match goal with
|[ |- context[finord _] ]=> (unfold finord ; try simpl)
|[|- context[(?x ;_).1] ] => change ((?x;_).1) with x (* Reduce projections *)
(* reduce disjunctions *)
|[|- context case_clause [(sum_rect _ _ _ (inl _))] ] =>
let X := fresh "QQ" in set (X := (sum_rect _ _ _ (inl _))); unfold sum_rect in X; unfold X
|[|- context case_clause [(sum_rect _ _ _ (inr _))] ] =>
let X := fresh "QQ" in set (X := (sum_rect _ _ _ (inr _))); unfold sum_rect in X; unfold X
|[|- (_;_)=(_;_) ] => (apply ord_eq_if_vals_eq) + (apply ord_eq_if_vals_eq')
(* Ap clauses *)
|[ |- @paths (object (OnObjects.sig_obj ChainCategory.Core.omega (fun zz : _ => lt zz _)))
_ _] => apply ord_eq_if_vals_eq
|[|- ?n + _ = ?n + _ ] => apply (ap (fun zz => n + zz))
|[ |- @paths nat _ _ ] => apply (ap (fun zz => (_ zz)%object.1))
end.
Patrick Nicodemus (Jan 04 2022 at 18:39):i don't think it matters much what the individual entries are. the problem is in the first match line
Patrick Nicodemus (Jan 04 2022 at 18:39):i.e.
|[ |- context[finord _] ]=> (unfold finord ; try simpl)
Patrick Nicodemus (Jan 04 2022 at 18:39):here's what happens when i try to run it
Patrick Nicodemus (Jan 04 2022 at 18:39):Going to execute:
repeat
match goal with
| |- context [ finord _ ] => unfold finord; try simpl
| |- context [ (?x; _).1 ] => change (?x; _).1 with x
| |- context case_clause[ sum_rect _ _ _ (inl _) ] =>
let X := fresh "QQ" in
set (X := sum_rect _ _ _ (inl _)); unfold sum_rect in X; unfold X
| |- context case_clause[ sum_rect _ _ _ (inr _) ] =>
let X := fresh "QQ" in
set (X := sum_rect _ _ _ (inr _)); unfold sum_rect in X; unfold X
| |- (_; _) = (_; _) => apply ord_eq_if_vals_eq + apply ord_eq_if_vals_eq'
| |- _ = _ => apply ord_eq_if_vals_eq
| |- ?n + _ = ?n + _ => apply (ap (fun zz => n + zz))
| |- _ = _ => apply (ap (fun zz => (_ zz).1))
end
Patrick Nicodemus (Jan 04 2022 at 18:40): Going to execute :
unfold finord; try simpl
Patrick Nicodemus (Jan 04 2022 at 18:40):...
Going to execute:
simpl
Patrick Nicodemus (Jan 04 2022 at 18:41):Level 0: Failed to progress.
Patrick Nicodemus (Jan 04 2022 at 18:41):Then the script stops.
Patrick Nicodemus (Jan 04 2022 at 18:42):I find this behavior bizarre. I think that if (try simpl) raises an error flag then the match should be considered a failure and it should try one of the other matches
Patrick Nicodemus (Jan 04 2022 at 18:42):and if it succeeds then the "repeat" keyword at the beginning should have the match loop again
Patrick Nicodemus (Jan 04 2022 at 18:43):but i can't understand why it stops after executing only the first line of the match.
Li-yao (Jan 04 2022 at 18:48):simpl never errors. You might be looking for progress simpl instead of try simpl.
Li-yao (Jan 04 2022 at 18:51):although, the unfold should count as progress, so I don't get what's going on actually.
Patrick Nicodemus (Jan 04 2022 at 18:57):i'll try progress simpl.
Patrick Nicodemus (Jan 04 2022 at 18:57):Really I don't care whether it counts as a success or failure, i want it to run again until it no longer matches on any goals.
Li-yao (Jan 04 2022 at 18:58):Do you have a working example to look at?
Patrick Nicodemus (Jan 04 2022 at 19:01):hmm i changed "try" to "progress" and now it enters an infinite loop
Patrick Nicodemus (Jan 04 2022 at 19:03):that line of code just loops over and over again
Patrick Nicodemus (Jan 04 2022 at 19:11):oh you know what i found something else strange going on. The command "unfold finord" doesn't actually do anything.
Patrick Nicodemus (Jan 04 2022 at 19:12):here's the current goal
Patrick Nicodemus (Jan 04 2022 at 19:12):@paths nat
(@proj1 (object ChainCategory.Core.omega)
(fun m : object ChainCategory.Core.omega => lt m m3)
(@object_of (finord n3) (finord m3) F3 k3))
(@proj1 (object ChainCategory.Core.omega)
(fun m : object ChainCategory.Core.omega => lt m m3)
(@object_of (finord n3) (finord m3) F3
(@exist nat (fun m : nat => lt m n3)
(sub (add (add n1 n2) (@proj1 nat (fun m : nat => lt m n3) k3)) (add n1 n2))
(natpmswap (add (add n1 n2) (@proj1 nat (fun m : nat => lt m n3) k3)) n3
(add n1 n2) (n_leq_add_n_k (add n1 n2) (@proj1 nat (fun m : nat => lt m n3) k3))
(@nataddpreserveslt' (@proj1 nat (fun m : nat => lt m n3) k3) n3
(add n1 n2) (@proj2 nat (fun m : nat => lt m n3) k3))))))
there are two occurrences of 'finord' in the middle
Patrick Nicodemus (Jan 04 2022 at 19:12):with Set Printing All enabled
Patrick Nicodemus (Jan 04 2022 at 19:12):but unfold finord seems to have no effect
Karl Palmskog (Jan 04 2022 at 19:12):@Patrick Nicodemus please surround your code with triple backquotes when it spans multiple lines
Patrick Nicodemus (Jan 04 2022 at 19:12):unfold finord in * works tho
Patrick Nicodemus (Jan 04 2022 at 19:12):i see
Karl Palmskog (Jan 04 2022 at 19:13):you need to have: <triple backquotes> <newline> <code> <newline> <triple backquotes>
Patrick Nicodemus (Jan 04 2022 at 19:14):Great. Thanks
Patrick Nicodemus (Jan 04 2022 at 19:18):so does anybody know why unfold wouldn't do anything here?
Patrick Nicodemus (Jan 04 2022 at 19:18):fyi the finord is invisible without Set Printing All turned on.
Li-yao (Jan 04 2022 at 19:34):Both the facts that unfold does nothing and that repeat loops are quite mysterious to me.
finord? Does cbv delta [finord] fare differently than unfold finord?match step by step to see what progress is does make? Paolo Giarrusso (Jan 04 2022 at 19:39):(deleted)
Patrick Nicodemus (Jan 04 2022 at 19:39):Definition finord (n : nat) : PreCategory := { m : omega | m < n }%category.
Patrick Nicodemus (Jan 04 2022 at 19:51):cbv delta [finord] also does not succeed at unravelling the definition of finord.
Patrick Nicodemus (Jan 04 2022 at 19:54):i have an idea of why it wouldn't work though. Could it be refusing to unfold it for typing reasons? Like if my context has terms t : exp, where exp depends on finord, then by unfolding the definition of finord, there could be other things that are ill typed
Patrick Nicodemus (Jan 04 2022 at 19:54):i guess like, say i have an equality type x = y, where the equality is of type finord and x and y are both in the context declared of type finord.
Patrick Nicodemus (Jan 04 2022 at 19:55):then trying to unfold 'finord' in @paths finord x y could be blocked because both x and y are assumed to be of type finord and so now there's a typing conflict
Patrick Nicodemus (Jan 04 2022 at 19:55):but if i run unfold finord in * it workd
Patrick Nicodemus (Jan 04 2022 at 19:55):could that be it?
Patrick Nicodemus (Jan 04 2022 at 19:56):the type finord is purely annotational here, but the reason i want to unfold it is because for automation purposes i don't want to write a bunch of different pattern-matching statements for different degrees of unfolding of the same term.
Patrick Nicodemus (Jan 04 2022 at 19:58):it would be silly to write like
match goal with
| [ |- @paths finord ?n _ _ ] =>...
|[|- @paths { m : nat | m < n } ] => ...
end
Patrick Nicodemus said:
i have an idea of why it wouldn't work though. Could it be refusing to unfold it for typing reasons? Like if my context has terms t : exp, where exp depends on finord, then by unfolding the definition of finord, there could be other things that are ill typed
that makes no sense
Patrick Nicodemus (Jan 04 2022 at 20:01):Sure. The fact that "unfold finord" doesn't actually unfold finord doesn't make any sense either. Do you have something constructive to say?
Paolo Giarrusso (Jan 04 2022 at 20:09):Discarding an impossible theory sounds plenty constructive: unfold preserves typeability.
Patrick Nicodemus (Jan 04 2022 at 20:13):Forgive me for questioning assumptions when what seems to be the obvious conclusion of the assumptions clearly doesn't hold.
Paolo Giarrusso (Jan 04 2022 at 20:14):This seems hard to explain without some Coq bug, so I think uploading the code and filing a bug report is the main way forward.
Patrick Nicodemus (Jan 04 2022 at 20:15):ok.
Paolo Giarrusso (Jan 04 2022 at 20:15):re “questioning assumptions”, it’s essentially a theorem that unfold cannot create typing problems.
Paolo Giarrusso (Jan 04 2022 at 20:18):more in general, tactics like unfold, simpl, cbn, cbv etc. always replace terms by convertible terms, which is guaranteed to respect typeability.
Patrick Nicodemus (Jan 05 2022 at 19:12):I am still trying to debug this code. Someone helped me out by pointing out that in the code above, @object_of is a primitive projection so the types (finord n3) and (finord m3) are in some sense illusory. this still doesn't exactly make it clear to me why the repeat match should halt after one iteration, as far as I can understand it either the match fails on the first branch and it should move to the second, or the match succeeds and then the whole match repeats from the beginning because of the repeat.
Patrick Nicodemus (Jan 05 2022 at 19:12):I ran the Unset Printing Primitive Projection Parameters. line and now the goal reads
Patrick Nicodemus (Jan 05 2022 at 19:12): @paths nat (@proj1 _ _ (@object_of _ _ F3 k3))
(@proj1 _ _
(@object_of _ _ F3
(@exist nat (fun m : nat => lt m n3)
(sub (add (add n1 n2) (@proj1 _ _ k3)) (add n1 n2))
(natpmswap (add (add n1 n2) (@proj1 _ _ k3)) n3 (add n1 n2)
(n_leq_add_n_k (add n1 n2) (@proj1 _ _ k3))
(@nataddpreserveslt' (@proj1 _ _ k3) n3 (add n1 n2) (@proj2 _ _ k3))))))
Now something happens that to me seems very strange.
Patrick Nicodemus (Jan 05 2022 at 19:13):This code successfully matches:
match goal with
|[ |- (@paths nat (
?n _ _ (@object_of _ _ _ _)) _ )] => idtac n
end.
and it prints @proj1 as expected.
Patrick Nicodemus (Jan 05 2022 at 19:15):match goal with
|[ |- (@paths nat (
@proj1 _ _ (@object_of _ _ _ _)) _ )] => idtac
end.
However this code does not match!
Patrick Nicodemus (Jan 05 2022 at 19:15):I can't understand why this would be.
Patrick Nicodemus (Jan 05 2022 at 19:16):I am willing to submit a bug report as others have advised but i am an inexperienced user and so i would prefer to discuss this further to rule out the possibility of my own error.
Paolo Giarrusso (Jan 05 2022 at 19:24):Maybe it's a bug, maybe not, but having access to the source code could help figure that out.
Paolo Giarrusso (Jan 05 2022 at 19:25):Especially since you are using primitive projections and they're a known weird nightmare to deal with.
Patrick Nicodemus (Jan 05 2022 at 19:29):Well that's not good to hear haha. I'm trying to make my life easier by using an existing library (which happens to use primitive projections) Is it possible that this line from the Coq documentation has anything to do with this
When the Primitive Projections flag is on, definitions of record types change meaning. When a type is declared with primitive projections, its match construct is disabled (see Primitive Projections though). To eliminate the (co-)inductive type, one must use its defined primitive projections.
Paolo Giarrusso (Jan 05 2022 at 19:30):(wondering if paths is a primitive projection, or something)
Paolo Giarrusso (Jan 05 2022 at 19:31):That is... A small part of the story.
Paolo Giarrusso (Jan 05 2022 at 19:34):https://coq.inria.fr/refman/language/core/records.html#reduction has more, but I used to use https://github.com/coq/coq/issues/5698 as documentation until recently.
Paolo Giarrusso (Jan 05 2022 at 19:36):It's still not obvious what's going on, but if paths in your goal were a primitive projection, that might explain the match problem.
Gaëtan Gilbert (Jan 05 2022 at 19:41):isn't paths the hott equality? in which case it's an inductive not a projection
Patrick Nicodemus (Jan 05 2022 at 19:43):yes, it's the equality from the coq-Hott library, https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v
Patrick Nicodemus (Jan 05 2022 at 19:44):i'm using the version of it available via opam for coq 8.14
Patrick Nicodemus (Jan 05 2022 at 19:45):btw i'm trying to reduce it to a simple standalone example but in the simple standalone case the problem seems to disappear :)
Patrick Nicodemus (Jan 05 2022 at 20:02):I mean the bug is knee deep in the middle of my project, which is spread across 4 files so far.
Patrick Nicodemus (Jan 05 2022 at 20:02):It's not necessary to minimize your bug or identify precisely where the issue is, since someone else can often do this if you include a complete example. We tend to include the code in the bug description itself, but if you have a very large input file then you can add it as an attachment.
Patrick Nicodemus (Jan 05 2022 at 20:03):the coq bug reporting documentation seems pretty forgiving but four files seems like a lot
Gaëtan Gilbert (Jan 05 2022 at 20:10):it's not that much unless they're really big files IMO
Patrick Nicodemus (Jan 05 2022 at 20:10):OK.
Paolo Giarrusso (Jan 05 2022 at 21:18):in fact I'm wondering about proj1, but the stdlib one isn't a primitive projection IIRC.
Paolo Giarrusso (Jan 05 2022 at 21:19):But now you say you're using coq-hott so even proj1 is a primitive projection
Paolo Giarrusso (Jan 05 2022 at 21:24):... which in retrospect your goals suggest. That already 50% explains your last issue: for each primitive projection (like proj1), there are two or three entities in Coq which are hard to distinguish: the primitive projection itself, and a definition wrapping it. Your goal contains the primitive projection itself, so maybe proj1 in your Ltac pattern refers to the wrapper.
Paolo Giarrusso (Jan 05 2022 at 21:25):I talk about three entities and not just two because of https://github.com/coq/coq/issues/5698#issuecomment-337556405
Paolo Giarrusso (Jan 05 2022 at 21:28):Okay, here's the match goal problem: https://github.com/coq/coq/issues/6994
Paolo Giarrusso (Jan 05 2022 at 22:08):https://github.com/coq/coq/issues/14084 seems to show more fun stuff involving (lazy)match goal and change (but I can't tell if it is specifically relevant).
Paolo Giarrusso (Jan 05 2022 at 22:25):https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+unfold+primitive+projection has other assorted Lovecraftian horrors, including about unfold.
Patrick Nicodemus (Jan 07 2022 at 01:11):alright i'll try and read this documentation and get a grip on it
Last updated: Oct 04 2023 at 20:01 UTC