<div dir="ltr"><div>@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:</div><div><br></div><div>```<br>this≇next : ∀ {A} {x y : A} {xs}<br>          → (y∈xs : y ∈ xs)<br>          → {x≡y : x ≡ y}<br>          → subst₂ _∈_ x≡y refl (this {x = x} {xs}) ≡ next {x = x} {y} {xs} y∈xs<br>          → ⊥<br>this≇next {x = x} {y} {xs} y∈xs {refl} this≡next =<br>  noConfusion this (next y∈xs) {refl} {refl} this≡next</div><div>```<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, May 20, 2020 at 8:47 PM Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Shin,</div><div><br></div><div>I was a bit too fast in my previous mail, sorry. The correct noConfusion property is as follows:</div><div><br></div><div>```</div><div>open import Data.Empty<br>open import Data.List<br>open import Data.Product<br>open import Relation.Binary.PropositionalEquality<br>open import Relation.Binary.HeterogeneousEquality using (_≅_; _≇_; ≅-to-≡)<br><br>data _∈_ {A : Set} : A → List A → Set where<br>  this : ∀ {x xs} → x ∈ (x ∷ xs)<br>  next : ∀ {x y xs} → y ∈ xs → y ∈ (x ∷ xs)<br><br>NoConfusion : {A : Set}<br>            → {x : A} {xs : List A} → (x ∈ xs)<br>            → {y : A} {ys : List A} → (y ∈ ys)<br>            → Set<br>NoConfusion (this {x} {xs}) (this {y} {ys}) = x ≡ y × xs ≡ ys<br>NoConfusion this        (next y∈ys) = ⊥<br>NoConfusion (next x∈xs) this        = ⊥<br>NoConfusion (next {x} {x'} {xs} x'∈xs) (next {y} {y'} {ys} y'∈ys) =<br>  x ≡ y × Σ (x' ≡ y') (λ x'≡y' → Σ (xs ≡ ys) (λ xs≡ys →<br>    subst₂ _∈_ x'≡y' xs≡ys x'∈xs ≡ y'∈ys))<br><br>noConfusion : {A : Set}<br>            → {x : A} {xs : List A} (x∈xs : x ∈ xs)<br>            → {y : A} {ys : List A} (y∈ys : y ∈ ys)<br>            → {x≡y : x ≡ y} {xs≡ys : xs ≡ ys} (x∈xs≡y∈ys : subst₂ _∈_ x≡y xs≡ys x∈xs ≡ y∈ys)<br>            → NoConfusion x∈xs y∈ys<br>noConfusion this this {refl} {refl} refl = refl , refl<br>noConfusion this (next y∈ys) {refl} {refl} ()<br>noConfusion (next x∈xs) this {refl} {refl} ()<br>noConfusion (next x∈xs) (next .x∈xs) {refl} {refl} refl = refl , refl , refl , refl<br>```</div><div><br></div><div>But I don't manage  to prove your goal from this directly, unfortunately.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, May 20, 2020 at 8:08 PM Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Shin,</div><div><br></div><div>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:</div><div><br></div><div>```</div><div>open import Data.Empty<br>open import Data.List<br>open import Data.Product<br>open import Relation.Binary.PropositionalEquality<br>open import Relation.Binary.HeterogeneousEquality using (_≇_)<br><br>data _∈_ {A : Set} : A → List A → Set where<br>  this : ∀ {x xs} → x ∈ (x ∷ xs)<br>  next : ∀ {x y xs} → y ∈ xs → y ∈ (x ∷ xs)<br><br>NoConfusion : {A : Set}<br>            → {x : A} {xs : List A} → (x ∈ xs)<br>            → {y : A} {ys : List A} → (y ∈ ys)<br>            → Set<br>NoConfusion (this {x} {xs}) (this {y} {ys}) = x ≡ y × xs ≡ ys<br>NoConfusion this        (next y∈ys) = ⊥<br>NoConfusion (next x∈xs) this        = ⊥<br>NoConfusion (next {x} {x'} {xs} x'∈xs) (next {y} {y'} {ys} y'∈ys) =<br>  x ≡ y × Σ (x' ≡ y') (λ x'≡y' → Σ (xs ≡ ys) (λ xs≡ys →<br>    subst₂ _∈_ x'≡y' xs≡ys x'∈xs ≡ y'∈ys))<br><br>noConfusion : {A : Set}<br>            → {x : A} {xs : List A} (x∈xs : x ∈ xs)<br>            → {y : A} {ys : List A} (y∈ys : y ∈ ys)<br>            → NoConfusion x∈xs y∈ys<br>noConfusion = {!!}<br><br>this≇next : ∀ {A} {x y : A} {xs}<br>          → (y∈xs : y ∈ xs)<br>          → this {x = x} {xs} ≇ next {x = x} {y} {xs} y∈xs<br>this≇next {x = x} {y} {xs} y∈xs this≡next =<br>  ⊥-elim (noConfusion (this {x = x} {xs}) (next {x = y} y∈xs))</div><div>```</div><div><br></div><div>You can read more about this in "A few constructions on constructors" (<a href="http://www.cs.ru.nl/~james/RESEARCH/types2004.pdf" target="_blank">http://www.cs.ru.nl/~james/RESEARCH/types2004.pdf</a>). The version above is my own variant using homogeneous equality.<br></div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, May 20, 2020 at 7:44 PM Shin-Cheng Mu <<a href="mailto:scm@iis.sinica.edu.tw" target="_blank">scm@iis.sinica.edu.tw</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
The following is a typical definition of a membership<br>
relation --- x ∈ xs indicates that x is a member of the<br>
list xs:<br>
<br>
 data _∈_ {A : Set} : A → List A → Set where<br>
   this : ∀ {x xs} → x ∈ (x ∷ xs)<br>
   next : ∀ {x y xs} → y ∈ xs → y ∈ (x ∷ xs)<br>
<br>
I encountered a question: how do I prove that "this",<br>
does not equal "next"?<br>
<br>
Since they might not have the same type, I need <br>
HeterogeneousEquality. In the following attempt,<br>
"this", with implicit arguments, has type x ∈ (x ∷ xs),<br>
while "next" has type y ∈ (x ∷ xs):<br>
<br>
 this≇next : ∀ {A} {x y : A} {xs}<br>
           → (y∈xs : y ∈ xs)<br>
           → this {x = x} {xs} ≇ next {x = x} {y} {xs} y∈xs<br>
 this≇next y∈xs ()<br>
<br>
This attempt fails, however. Agda reports the error:<br>
<br>
 Failed to solve the following constraints:<br>
   Is empty: this ≅ next y∈xs<br>
<br>
How do I convince Agda that "this" is not "next"?<br>
<br>
The Agda version is 2.6.1. I have attached the <br>
simple test file below.<br>
<br>
Thank you!<br>
<br>
sincerely,<br>
Shin<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div>
</blockquote></div>