[Agda] constructor injectiveness

[Ulf Norell]

On Fri, May 26, 2017 at 3:23 PM, Andreas Abel <abela at chalmers.se> wrote:

> > Is there possible a simpler expression for _≟d_ ?
>
> I don't think so.
>
> > Probably injectiveness of constructors like `con' needs to be somehow in
> > Standard, similarly as PE.cong is in standard (?)
>
> These injectivity proofs are necessary boilerplate, but could maybe be
> programmed generically using reflection.


See for instance

https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda

/ Ulf



> On 26.05.2017 13:49, Sergei Meshveliani wrote:
>
>> People,
>>
>> I need to program  _≟d_  below,
>> and do this by introducing con-injective and +injective.
>>   Is there possible a simpler expression for _≟d_ ?
>> Probably injectiveness of constructors like `con' needs to be somehow in
>> Standard, similarly as PE.cong is in standard (?)
>>
>> Thanks,
>>
>> ------
>> Sergei
>>
>>
>> -----------------------------------------------------------------------
>> open import Function using (_∘_; case_of_)
>> open import Relation.Nullary using (yes; no)
>> open import Relation.Binary using () renaming (Decidable to Decidable₂)
>> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
>> open import Data.Product using (_×_; _,_; proj₁; proj₂)
>> open import Data.Nat     using (ℕ; _≟_)
>>
>> data D : Set where  con : ℕ → D
>>                             _+_ : D → D → D
>>
>> con-injective :  ∀ {e e'} → con e ≡ con e' → e ≡ e'
>> con-injective PE.refl = PE.refl
>>
>> +injective :  ∀ {x y z u} → (x + y) ≡ (z + u) → x ≡ z × y ≡ u
>> +injective {x} {y} {.x} {.y} PE.refl = (PE.refl , PE.refl)
>>
>> _≟d_ : Decidable₂ (_≡_ {A = D})
>>
>> (con _) ≟d (_ + _) =  no λ()
>> (_ + _) ≟d (con _) =  no λ()
>> (con i) ≟d (con j) =  case i ≟ j
>>                        of \
>>                        { (yes i≡j) → yes (PE.cong con i≡j)
>>                        ; (no i≢j)  → no (i≢j ∘ con-injective)
>>                        }
>> (x + y) ≟d (z + u) =
>>             case (x ≟d z , y ≟d u)
>>             of \
>>             { (yes x≡z , yes y≡u) → yes (PE.cong₂ _+_ x≡z y≡u)
>>             ; (no x≢z , _       ) → no (x≢z ∘ proj₁ ∘ +injective)
>>             ; (_ ,      no y≢u  ) → no (y≢u ∘ proj₂ ∘ +injective)
>>             }
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170526/97621b16/attachment-0001.html>