Stream: Coq users

Topic: Help debugging broken ltac script


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:39):

i.e.
|[ |- context[finord _] ]=> (unfold finord ; try simpl)

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:39):

here's what happens when i try to run it

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:40):

Going to execute : unfold finord; try simpl

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:40):

...
Going to execute: simpl

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:41):

Level 0: Failed to progress.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:41):

Then the script stops.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Li-yao (Jan 04 2022 at 18:48):

simpl never errors. You might be looking for progress simpl instead of try simpl.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 18:57):

i'll try progress simpl.

view this post on Zulip 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.

view this post on Zulip Li-yao (Jan 04 2022 at 18:58):

Do you have a working example to look at?

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:01):

hmm i changed "try" to "progress" and now it enters an infinite loop

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:03):

that line of code just loops over and over again

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:12):

here's the current goal

view this post on Zulip 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))))))

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:12):

there are two occurrences of 'finord' in the middle

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:12):

with Set Printing All enabled

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:12):

but unfold finord seems to have no effect

view this post on Zulip Karl Palmskog (Jan 04 2022 at 19:12):

@Patrick Nicodemus please surround your code with triple backquotes when it spans multiple lines

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:12):

unfold finord in * works tho

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:12):

i see

view this post on Zulip Karl Palmskog (Jan 04 2022 at 19:13):

you need to have: <triple backquotes> <newline> <code> <newline> <triple backquotes>

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:14):

Great. Thanks

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:18):

so does anybody know why unfold wouldn't do anything here?

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:18):

fyi the finord is invisible without Set Printing All turned on.

view this post on Zulip Li-yao (Jan 04 2022 at 19:34):

Both the facts that unfold does nothing and that repeat loops are quite mysterious to me.

  1. What's the definition of finord? Does cbv delta [finord] fare differently than unfold finord?
  2. What if you apply the match step by step to see what progress is does make?

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 19:39):

(deleted)

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:39):

Definition finord (n : nat) : PreCategory := { m : omega | m < n }%category.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:51):

cbv delta [finord] also does not succeed at unravelling the definition of finord.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:55):

but if i run unfold finord in * it workd

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 19:55):

could that be it?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jan 04 2022 at 19:58):

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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 20:09):

Discarding an impossible theory sounds plenty constructive: unfold preserves typeability.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 04 2022 at 20:15):

ok.

view this post on Zulip Paolo Giarrusso (Jan 04 2022 at 20:15):

re “questioning assumptions”, it’s essentially a theorem that unfold cannot create typing problems.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:12):

I ran the Unset Printing Primitive Projection Parameters. line and now the goal reads

view this post on Zulip 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))))))

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:13):

Now something happens that to me seems very strange.

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:13):

This code successfully matches:

      match goal with
      |[ |- (@paths nat (
                      ?n _ _ (@object_of _ _ _ _)) _ )] => idtac n
      end.

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:15):

and it prints @proj1 as expected.

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:15):

match goal with
      |[ |- (@paths nat (
                      @proj1 _ _ (@object_of _ _ _ _)) _ )] =>  idtac
      end.

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:15):

However this code does not match!

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:15):

I can't understand why this would be.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 19:30):

(wondering if paths is a primitive projection, or something)

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 19:31):

That is... A small part of the story.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 19:44):

i'm using the version of it available via opam for coq 8.14

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 20:03):

the coq bug reporting documentation seems pretty forgiving but four files seems like a lot

view this post on Zulip Gaëtan Gilbert (Jan 05 2022 at 20:10):

it's not that much unless they're really big files IMO

view this post on Zulip Patrick Nicodemus (Jan 05 2022 at 20:10):

OK.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 21:19):

But now you say you're using coq-hott so even proj1 is a primitive projection

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 21:28):

Okay, here's the match goal problem: https://github.com/coq/coq/issues/6994

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Jan 07 2022 at 01:11):

alright i'll try and read this documentation and get a grip on it


Last updated: Jan 27 2023 at 01:03 UTC