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
set t := f a.
does not affect c
, the second match _should_ fail: context matches are up to syntactic equality, not definitional equality.match goal with
| [ H : context[fun_of_fin (fun_of_monotonic_fn _ _ f) a] |- _ ] => idtac
end.
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: Sep 26 2023 at 12:02 UTC