Patrick Nicodemus (Sep 09 2022 at 19:31): Patrick Nicodemus (Sep 09 2022 at 19:31):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.
Patrick Nicodemus (Sep 09 2022 at 19:32):(Thanks to Jason Gross for his useful bug minimization script.)
Patrick Nicodemus (Sep 09 2022 at 19:35):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.
Patrick Nicodemus (Sep 09 2022 at 19:52):On the other hand, the command rewrite [f a](Logic.eq_refl (f a)) in c fails. (SSReflect rewrite)
Patrick Nicodemus (Sep 09 2022 at 19:58):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. Paolo Giarrusso (Sep 09 2022 at 22:01):(also, changes to Ltac1 behaviors are unlikely these days since we're slowly moving toward Ltac2)
Patrick Nicodemus (Sep 09 2022 at 22:20):Ok I'll think about what you're saying.
Patrick Nicodemus (Sep 09 2022 at 22:23):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
Paolo Giarrusso (Sep 09 2022 at 22:36):It is alpha equivalence
Paolo Giarrusso (Sep 09 2022 at 22:38):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
Paolo Giarrusso (Sep 09 2022 at 22:42):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.
Patrick Nicodemus (Sep 10 2022 at 01:39):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.
Paolo Giarrusso (Sep 10 2022 at 15:00):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.
Patrick Nicodemus (Oct 07 2022 at 18:54):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.
Patrick Nicodemus (Oct 07 2022 at 18:56):If I add the line
set (j := (underlying_natural _ _)) in *.
before the match, it works.
Patrick Nicodemus (Oct 07 2022 at 19:01):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?
Paolo Giarrusso (Oct 07 2022 at 19:12):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
Paolo Giarrusso (Oct 07 2022 at 19:18):yep
Patrick Nicodemus (Oct 07 2022 at 19:24):nice thanks!
Notification Bot (Oct 07 2022 at 19:24):Patrick Nicodemus has marked this topic as resolved.
Last updated: Sep 26 2023 at 12:02 UTC