[Agda] Problem proving inequality with HeterogeneousEquality

[Jesper Cockx]

Hi Shin,

As taught by our master Conor, you need to generalize the statement and
first prove the `noConfusion` property of your datatype. Disjointness and
injectivity of constructors follows directly from that:

```
open import Data.Empty
open import Data.List
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality using (_≇_)

data _∈_ {A : Set} : A → List A → Set where
  this : ∀ {x xs} → x ∈ (x ∷ xs)
  next : ∀ {x y xs} → y ∈ xs → y ∈ (x ∷ xs)

NoConfusion : {A : Set}
            → {x : A} {xs : List A} → (x ∈ xs)
            → {y : A} {ys : List A} → (y ∈ ys)
            → Set
NoConfusion (this {x} {xs}) (this {y} {ys}) = x ≡ y × xs ≡ ys
NoConfusion this        (next y∈ys) = ⊥
NoConfusion (next x∈xs) this        = ⊥
NoConfusion (next {x} {x'} {xs} x'∈xs) (next {y} {y'} {ys} y'∈ys) =
  x ≡ y × Σ (x' ≡ y') (λ x'≡y' → Σ (xs ≡ ys) (λ xs≡ys →
    subst₂ _∈_ x'≡y' xs≡ys x'∈xs ≡ y'∈ys))

noConfusion : {A : Set}
            → {x : A} {xs : List A} (x∈xs : x ∈ xs)
            → {y : A} {ys : List A} (y∈ys : y ∈ ys)
            → NoConfusion x∈xs y∈ys
noConfusion = {!!}

this≇next : ∀ {A} {x y : A} {xs}
          → (y∈xs : y ∈ xs)
          → this {x = x} {xs} ≇ next {x = x} {y} {xs} y∈xs
this≇next {x = x} {y} {xs} y∈xs this≡next =
  ⊥-elim (noConfusion (this {x = x} {xs}) (next {x = y} y∈xs))
```

You can read more about this in "A few constructions on constructors" (
http://www.cs.ru.nl/~james/RESEARCH/types2004.pdf). The version above is my
own variant using homogeneous equality.

-- Jesper

On Wed, May 20, 2020 at 7:44 PM Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:

> Hi,
>
> The following is a typical definition of a membership
> relation --- x ∈ xs indicates that x is a member of the
> list xs:
>
>  data _∈_ {A : Set} : A → List A → Set where
>    this : ∀ {x xs} → x ∈ (x ∷ xs)
>    next : ∀ {x y xs} → y ∈ xs → y ∈ (x ∷ xs)
>
> I encountered a question: how do I prove that "this",
> does not equal "next"?
>
> Since they might not have the same type, I need
> HeterogeneousEquality. In the following attempt,
> "this", with implicit arguments, has type x ∈ (x ∷ xs),
> while "next" has type y ∈ (x ∷ xs):
>
>  this≇next : ∀ {A} {x y : A} {xs}
>            → (y∈xs : y ∈ xs)
>            → this {x = x} {xs} ≇ next {x = x} {y} {xs} y∈xs
>  this≇next y∈xs ()
>
> This attempt fails, however. Agda reports the error:
>
>  Failed to solve the following constraints:
>    Is empty: this ≅ next y∈xs
>
> How do I convince Agda that "this" is not "next"?
>
> The Agda version is 2.6.1. I have attached the
> simple test file below.
>
> Thank you!
>
> sincerely,
> Shin
>
>
>
>
> _______________________________________________
> 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/20200520/f10e275b/attachment.html>