<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>