[Agda] constructor injectiveness

[Andreas Abel]

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

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/