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

Subject: Ssreflect Users Discussion List

List archive

From: Robbert Krebbers <>
To:
Subject: Re: [ssreflect] [rewrite foo in hyp] weirdness
Date: Thu, 14 Jan 2016 16:03:07 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:cB5JFxcYzcAC++9IayvIpv23lGMj4u6mDksu8pMizoh2WeGdxc68Zh7h7PlgxGXEQZ/co6odzbGG7eawCCdesd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDsvc2CKFsYzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEjVqZVAjArOHwd4dbx8BjFVwqGoHoaSGQf1BRSUCbf6xSvZJD7uCbgqqJewiSQN8DsVvhgXD2j66ZtRxvpkzscHyQ++mvakNBzlq9Rqh+7vFp5x9iHM8muKPNic/aFLpshTm1bU5MJWg==

On 01/14/2016 03:49 PM, Enrico Tassi wrote:

Robbers, is your rewriteable relation a defined (i.e. delta-reducible)
constant or it is an inductive/hard constant?

Most are defined (delta-reducible) constants.

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?

Best,

Robbert

[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