I am having the following bug:

```
Require mathcomp.ssreflect.finfun.
Import Coq.ssr.ssreflect Coq.ssr.ssrbool.
Import mathcomp.ssreflect.fintype.
Import mathcomp.ssreflect.finfun.
Definition monotonic {n m : nat} (f : 'I_m^n) : bool.
Admitted.
Record monotonic_fn_sig (n m : nat) := { fun_of_monotonic_fn :> 'I_m^n ;
_ : monotonic fun_of_monotonic_fn }.
Import Coq.ssr.ssreflect.
Proposition t (n m: nat) (a : 'I_n) (b : 'I_m) (f : monotonic_fn_sig n m) (c : f a = b) : True.
Proof.
match goal with
| [ H : context[f a] |- _ ] => idtac
end.
set t := f a.
match goal with
| [ H : context[t] |- _ ] => idtac
end.
```

I think the match statements should succeed. But they do not.

I tried running simpl in various combinations of the hypotheses and goal and the body of t; this does not help.

Does anybody have a suggestion?

N. b. - if I run `Set Printing All`

and replace `t`

or `f a`

in the context match with the body, it is successful.

(Thanks to Jason Gross for his useful bug minimization script.)

Also, the ssreflect `set`

tactic is able to recognize `f a`

as a subterm of `f a = b`

. That is, `set t := f a in c`

works as expected.

On the other hand, the command `rewrite [f a](Logic.eq_refl (f a)) in c`

fails. (SSReflect rewrite)

Version number

```
The Coq Proof Assistant, version 8.16.0
compiled with OCaml 4.13.1
```

- Since
`set t := f a.`

does not affect`c`

, the second match _should_ fail: context matches are up to syntactic equality, not definitional equality. - I see that what succeeds is

`match goal with | [ H : context[fun_of_fin (fun_of_monotonic_fn _ _ f) a] |- _ ] => idtac end.`

I assume what you'd like is that`f a`

would be expanded as done in terms. I'm not sure if that's not possible or just not implemented.

(also, changes to Ltac1 behaviors are unlikely these days since we're slowly moving toward Ltac2)

Ok I'll think about what you're saying.

Is there a rough outline somewhere of where I can find examples of what syntactic equality is? Is it just alpha equivalence or is there more to it

It is alpha equivalence

But dealing alpha equivalence makes the answer more confusing than it should be if you formalize the syntax of some language (lambda calculus or Coq) with eg de Bruijn indexes, syntactic equality is just the strictest relation (propositional equality of ASTs) and other equivalences are "looser" ones

In other words, the key idea behind "syntactic equality" of two terms is to "the (abstract) syntax of these two terms is exactly the same" (once we understand that bound names don't belong in the abstract syntax). And this concept makes sense for arbitrary languages.

Ok. I understand your point about alpha equivalence but I am still having problems.

```
move: c.
set (z := fun_of_fin (@fun_of_monotonic_fn _ _ f) a).
```

This code (placed immediately at the beginning of my proof) works as expected. But it stops working if I put in the `simpl`

command or run `/=`

.

I assume the parentheses force it to be standard Coq `set`

. The SSReflect `set`

doesn't seem to have this problem.

IIRC ssreflect set works modulo unification (full story at https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#matching), but Coq set differs here. IIRC it uses syntactic equality? https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.set isn't too explicit.

I am having trouble with the following code:

```
Require Import HoTT.Basics.
Require Import HoTT.Spaces.Nat.
Local Open Scope nat_scope.
Definition stdfinset (n: nat) := { m : nat | m < n }.
Definition underlying_natural : forall (n : nat), stdfinset n -> nat := fun n m => pr1 m.
Global Coercion underlying_natural : stdfinset >-> nat.
Definition s (n : nat) (i : (stdfinset n.+1)) : (stdfinset n.+2) -> (stdfinset n.+1).
Admitted.
Proposition test (n : nat) (i : stdfinset n.+1) (y1 : stdfinset n.+2)
(s_ineq : s n i y1 < s n i y1) : True.
Proof.
Set Printing All.
match goal with
| [ H : ?n < ?n |- _ ] => idtac
end.
```

I think the pattern match should work (with H := s_ineq) but it does not.

If I add the line

` set (j := (underlying_natural _ _)) in *.`

before the match, it works.

```
ltac2:(match! goal with
| [ h : lt ?n ?n |- _ ] => Message.print(Message.of_string("Hello, world!"))
end).
```

The ltac2 version has the same error. What am I doing wrong?

printing universes reveals the two arguments have different universes, while with the stdlib no universes appear. I don't know if that's supposed to count as "syntactically different", but that would be reasonable

```
t@{hott.67}
(underlying_natural@{hott.74 hott.75} (S n)
(s@{hott.76 hott.77 hott.78 hott.79 hott.74 hott.75} n i y1))
(underlying_natural@{hott.82 hott.83} (S n)
(s@{hott.76 hott.77 hott.78 hott.79 hott.82 hott.83} n i y1))
```

Meanwhile, this works, but has a very different meaning. `unify`

can perform lots of computation in general

```
match goal with
| [ H : lt ?n1 ?n2 |- _ ] => unify n1 n2; idtac n1 n2
end.
```

constr_eq should be enough

yep

nice thanks!

Patrick Nicodemus has marked this topic as resolved.

Last updated: May 24 2024 at 22:02 UTC