[Agda] Problem proving inequality with HeterogeneousEquality

[Tom Jack]

The proof of this≇next does not use the argument this≡next! Indeed, we can
derive ⊥ from the postulated noConfusion.

I think there was supposed to be an extra argument of type `x∈xs ≅ y∈ys`?

I am unable to prove that version of noConfusion, because I cannot manage
to use the heterogeneous equality assumption.

Intuitively, it seems impossible to me, because I also expect to fail to
inhabit the following type:

{A : Set} {x : A} {xs : List A} {y : A} {ys : List A}
→ (x ∈ xs) ≡ (y ∈ ys)
→ (x ≡ y) × (xs ≡ ys)

(Unless we turn on `--injective-type-constructors`!)

On Wed, May 20, 2020 at 1:08 PM Jesper Cockx <Jesper at sikanda.be> wrote:

> 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
>>
> _______________________________________________
> 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/7ce5ea92/attachment.html>