<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Fri, May 26, 2017 at 3:23 PM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="gmail-">> Is there possible a simpler expression for _≟d_ ?<br>
<br></span>
I don't think so.<span class="gmail-"><br>
<br>
> Probably injectiveness of constructors like `con' needs to be somehow in<br>
> Standard, similarly as PE.cong is in standard (?)<br>
<br></span>
These injectivity proofs are necessary boilerplate, but could maybe be programmed generically using reflection.</blockquote><div><br></div><div>See for instance</div><div><br></div><div><a href="https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda">https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda</a><br></div><div><br></div><div>/ Ulf</div><div><br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail-HOEnZb"><div class="gmail-h5">On <a href="tel:26.05.2017%2013" value="+12605201713" target="_blank">26.05.2017 13</a>:49, Sergei Meshveliani wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
People,<br>
<br>
I need to program  _≟d_  below,<br>
and do this by introducing con-injective and +injective.<br>
  Is there possible a simpler expression for _≟d_ ?<br>
Probably injectiveness of constructors like `con' needs to be somehow in<br>
Standard, similarly as PE.cong is in standard (?)<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
------------------------------<wbr>------------------------------<wbr>-----------<br>
open import Function using (_∘_; case_of_)<br>
open import Relation.Nullary using (yes; no)<br>
open import Relation.Binary using () renaming (Decidable to Decidableâ‚‚)<br>
open import Relation.Binary.PropositionalE<wbr>quality as PE using (_≡_)<br>
open import Data.Product using (_×_; _,_; proj₁; projâ‚‚)<br>
open import Data.Nat  Â  Â using (â„•; _≟_)<br>
<br>
data D : Set where  con : â„• â†’ D<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  _+_ : D â†’ D â†’ D<br>
<br>
con-injective :  âˆ€ {e e'} â†’ con e â‰¡ con e' â†’ e â‰¡ e'<br>
con-injective PE.refl = PE.refl<br>
<br>
+injective :  âˆ€ {x y z u} â†’ (x + y) â‰¡ (z + u) â†’ x â‰¡ z Ã— y â‰¡ u<br>
+injective {x} {y} {.x} {.y} PE.refl = (PE.refl , PE.refl)<br>
<br>
_≟d_ : Decidableâ‚‚ (_≡_ {A = D})<br>
<br>
(con _) â‰Ÿd (_ + _) =  no Î»()<br>
(_ + _) â‰Ÿd (con _) =  no Î»()<br>
(con i) â‰Ÿd (con j) =  case i â‰Ÿ j<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â of \<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â { (yes i≡j) â†’ yes (PE.cong con i≡j)<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â ; (no i≢j)  â†’ no (i≢j âˆ˜ con-injective)<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â }<br>
(x + y) â‰Ÿd (z + u) =<br>
  Â  Â  Â  Â  Â  case (x â‰Ÿd z , y â‰Ÿd u)<br>
  Â  Â  Â  Â  Â  of \<br>
  Â  Â  Â  Â  Â  { (yes x≡z , yes y≡u) â†’ yes (PE.congâ‚‚ _+_ x≡z y≡u)<br>
  Â  Â  Â  Â  Â  ; (no x≢z , _  Â  Â  Â ) â†’ no (x≢z âˆ˜ proj₁ âˆ˜ +injective)<br>
  Â  Â  Â  Â  Â  ; (_ ,  Â  Â  no y≢u  ) â†’ no (y≢u âˆ˜ projâ‚‚ âˆ˜ +injective)<br>
  Â  Â  Â  Â  Â  }<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br></div></div><span class="gmail-HOEnZb"><font color="#888888">
-- <br>
Andreas Abel  <><  Â  Â  Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a></font></span><div class="gmail-HOEnZb"><div class="gmail-h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>