[Agda] Problem proving inequality with HeterogeneousEquality

[Jesper Cockx]

@Tom Indeed, it seems this cannot be proven without assuming injectivity of
type constructors, which is often the case when working with heterogeneous
equality. However, you can prove a very similar statement using homogeneous
equality and subst:

```
this≇next : ∀ {A} {x y : A} {xs}
          → (y∈xs : y ∈ xs)
          → {x≡y : x ≡ y}
          → subst₂ _∈_ x≡y refl (this {x = x} {xs}) ≡ next {x = x} {y} {xs}
y∈xs
          → ⊥
this≇next {x = x} {y} {xs} y∈xs {refl} this≡next =
  noConfusion this (next y∈xs) {refl} {refl} this≡next
```

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

> Hi Shin,
>
> I was a bit too fast in my previous mail, sorry. The correct noConfusion
> property is as follows:
>
> ```
> open import Data.Empty
> open import Data.List
> open import Data.Product
> open import Relation.Binary.PropositionalEquality
> open import Relation.Binary.HeterogeneousEquality using (_≅_; _≇_; ≅-to-≡)
>
> 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)
>             → {x≡y : x ≡ y} {xs≡ys : xs ≡ ys} (x∈xs≡y∈ys : subst₂ _∈_ x≡y
> xs≡ys x∈xs ≡ y∈ys)
>             → NoConfusion x∈xs y∈ys
> noConfusion this this {refl} {refl} refl = refl , refl
> noConfusion this (next y∈ys) {refl} {refl} ()
> noConfusion (next x∈xs) this {refl} {refl} ()
> noConfusion (next x∈xs) (next .x∈xs) {refl} {refl} refl = refl , refl ,
> refl , refl
> ```
>
> But I don't manage  to prove your goal from this directly, unfortunately.
>
> -- Jesper
>
> On Wed, May 20, 2020 at 8: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
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200520/6baff51b/attachment.html>