[Agda] Problem proving inequality with HeterogeneousEquality

[Donnacha Oisín Kidney]

Unless I’ve misunderstood I think you can do it by converting to an unindexed type like Nat first:

∈-to-ℕ : x ∈ xs → ℕ
∈-to-ℕ this = zero
∈-to-ℕ (next x∈xs) = suc (∈-to-ℕ x∈xs)

this≇next : (x∈xs : x ∈ xs) → this ≇ next x∈xs
this≇next _ t≡n with cong ∈-to-ℕ t≡n
this≇next _ t≡n | ()

I’ve attached a file with the code.

Oisín.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ThisNext.agda
Type: application/octet-stream
Size: 567 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200520/af42ecdc/attachment.obj>
-------------- next part --------------



> On 20 May 2020, at 18:43, 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
> 
> 
> <HEqTest.agda>
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda