My match goal seems not to work when "simpl" can't make progress and i don't understand why.

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

i don't think it matters much what the individual entries are. the problem is in the first match line

i.e.

` |[ |- context[finord _] ]=> (unfold finord ; try simpl)`

here's what happens when i try to run it

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

```
Going to execute :
unfold finord; try simpl
```

...

```
Going to execute:
simpl
```

`Level 0: Failed to progress.`

Then the script stops.

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

and if it succeeds then the "repeat" keyword at the beginning should have the match loop again

but i can't understand why it stops after executing only the first line of the match.

`simpl`

never errors. You might be looking for `progress simpl`

instead of `try simpl`

.

although, the `unfold`

should count as progress, so I don't get what's going on actually.

i'll try `progress simpl`

.

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.

Do you have a working example to look at?

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

that line of code just loops over and over again

oh you know what i found something else strange going on. The command "unfold finord" doesn't actually do anything.

here's the current goal

```
@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

with `Set Printing All`

enabled

but `unfold finord`

seems to have no effect

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

`unfold finord in *`

works tho

i see

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

Great. Thanks

so does anybody know why `unfold`

wouldn't do anything here?

fyi the `finord`

is invisible without Set Printing All turned on.

Both the facts that `unfold`

does nothing and that `repeat`

loops are quite mysterious to me.

- What's the definition of
`finord`

? Does`cbv delta [finord]`

fare differently than`unfold finord`

? - What if you apply the
`match`

step by step to see what progress is does make?

(deleted)

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

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

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

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.

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

but if i run `unfold finord in *`

it workd

could that be it?

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.

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

Sure. The fact that "unfold finord" doesn't actually unfold finord doesn't make any sense either. Do you have something constructive to say?

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

Forgive me for questioning assumptions when what seems to be the obvious conclusion of the assumptions clearly doesn't hold.

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.

ok.

re “questioning assumptions”, it’s essentially a theorem that `unfold`

cannot create typing problems.

more in general, tactics like `unfold`

, `simpl`

, `cbn`

, `cbv`

etc. always replace terms by convertible terms, which is guaranteed to respect typeability.

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.

I ran the `Unset Printing Primitive Projection Parameters.`

line and now the goal reads

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

This code successfully matches:

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

and it prints `@proj1`

as expected.

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

However this code does not match!

I can't understand why this would be.

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.

Maybe it's a bug, maybe not, but having access to the source code could help figure that out.

Especially since you are using primitive projections and they're a known weird nightmare to deal with.

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.

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

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

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.

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.

isn't paths the hott equality? in which case it's an inductive not a projection

yes, it's the equality from the coq-Hott library, https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v

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

btw i'm trying to reduce it to a simple standalone example but in the simple standalone case the problem seems to disappear :)

I mean the bug is knee deep in the middle of my project, which is spread across 4 files so far.

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.

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

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

OK.

in fact I'm wondering about proj1, but the stdlib one isn't a primitive projection IIRC.

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

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

I talk about three entities and not just two because of https://github.com/coq/coq/issues/5698#issuecomment-337556405

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

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

https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+unfold+primitive+projection has other assorted Lovecraftian horrors, including about unfold.

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

Last updated: Jun 18 2024 at 08:01 UTC