ssreflect - Re: [ssreflect] [rewrite foo in hyp] weirdness

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] [rewrite foo in hyp] weirdness

From: Robbert Krebbers <>
To:
Subject: Re: [ssreflect] [rewrite foo in hyp] weirdness
Date: Thu, 14 Jan 2016 16:16:47 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:uAVb8BWB9z+95cbfuu76x3A5U9/V8LGtZVwlr6E/grcLSJyIuqrYZhKFt8tkgFKBZ4jH8fUM07OQ6PC+HzxRqsjR+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8OVM1QD2mr1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GKdDFjkoN20++OXurgOGTA2V53JaU2MMkxMODRKWwgv9W8LLtSHwu/BhkAqAMMf8QKovEWCn5qZvSRnnjCYcKyUR6mbdgMFqkKFBrRirqgZkhYjQNtLGfMFid7/QKItJDVFKWdxcAnRM

On 01/14/2016 04:11 PM, Enrico Tassi wrote:

On Thu, Jan 14, 2016 at 04:03:07PM +0100, Robbert Krebbers wrote:

> >then we pass the ball to Coq's rewrite anyway and let it complain"

>Will we then still benefit from ssr's subexpression matching when rewriting
>with setoid relations/partial orders?

Yes.

Good :).

Still there is a limitation: ssreflect's patterns do not operate
under binders.

I can live with that. Coq's vanilla rewrite tactic also doesn't work under binders, for that one has to use the setoid_rewrite tactic.

[ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/13/2016
- Re: [ssreflect] [rewrite foo in hyp] weirdness, Emilio Jesús Gallego Arias, 01/13/2016
  - Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/13/2016
    - RE: [ssreflect] [rewrite foo in hyp] weirdness, Georges Gonthier, 01/13/2016
      - Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/13/2016
      - Re: [ssreflect] [rewrite foo in hyp] weirdness, Enrico Tassi, 01/14/2016
        
        Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/14/2016
        
        Re: [ssreflect] [rewrite foo in hyp] weirdness, Enrico Tassi, 01/14/2016
        
        Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/14/2016
        
        RE: [ssreflect] [rewrite foo in hyp] weirdness, Georges Gonthier, 01/14/2016

List archive

Re: [ssreflect] [rewrite foo in hyp] weirdness