Stream: Coq users

Topic: ✔ Context match bug


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

view this post on Zulip Patrick Nicodemus (Sep 09 2022 at 19:32):

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

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

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

view this post on Zulip Patrick Nicodemus (Sep 09 2022 at 19:58):

Version number

The Coq Proof Assistant, version 8.16.0
compiled with OCaml 4.13.1

view this post on Zulip Paolo Giarrusso (Sep 09 2022 at 22:00):

view this post on Zulip Paolo Giarrusso (Sep 09 2022 at 22:01):

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

view this post on Zulip Patrick Nicodemus (Sep 09 2022 at 22:20):

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

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

view this post on Zulip Paolo Giarrusso (Sep 09 2022 at 22:36):

It is alpha equivalence

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

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

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

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

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

view this post on Zulip Patrick Nicodemus (Oct 07 2022 at 18:54):

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

view this post on Zulip Patrick Nicodemus (Oct 07 2022 at 18:56):

If I add the line
set (j := (underlying_natural _ _)) in *.
before the match, it works.

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

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

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 19:14):

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.

view this post on Zulip Gaëtan Gilbert (Oct 07 2022 at 19:14):

constr_eq should be enough

view this post on Zulip Paolo Giarrusso (Oct 07 2022 at 19:18):

yep

view this post on Zulip Patrick Nicodemus (Oct 07 2022 at 19:24):

nice thanks!

view this post on Zulip Notification Bot (Oct 07 2022 at 19:24):

Patrick Nicodemus has marked this topic as resolved.


Last updated: Mar 29 2024 at 09:02 UTC