<div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Marcus, I could not follow your example, but it seems that you are trying to case split a function, which is not possible.</div><div><br></div><div>```<br>open import Relation.Binary.PropositionalEquality<br>open import Data.Nat<br>open import Data.Empty<br>open import Relation.Nullary<br><br><br>fun : ¬ (2 ≡ 2) → ⊥<br>fun ¬x = ? -- ⊥-elim (¬x refl)<br><br></div><div>```</div><div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Mar 14, 2019 at 9:15 AM Marcus Christian Lehmann <<a href="mailto:lehmann@tet.tu-berlin.de">lehmann@tet.tu-berlin.de</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 bgcolor="#FFFFFF">
<p><tt>Hello Agda Community,</tt></p>
<p><tt>The case-split C-c on proof of ≡ works great and even leaves
out impossible cases.</tt><tt> But for case-splits of proofs of
it's negation ≢ I get</tt></p>
<p>
</p><blockquote type="cite"><tt><span style="color:rgb(66,66,67);font-size:15px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:pre-wrap;word-spacing:0px;background-color:rgb(250,250,250);text-decoration-style:initial;text-decoration-color:initial;display:inline;float:none">Cannot split on argument of non-datatype 〚 x₁ 〛ᵇ ≢ 〚 x₁ 〛ᵇ
when checking that the expression ? has type ⊥</span></tt></blockquote>
<tt>Is there a nice way to have case-split work for these cases
(i.e. on λ() )?</tt><tt><br>
</tt><p></p>
<p><tt>I could only come up with manually providing "inequality
evidence" for my (mutual) datatypes by writing out all unequal
combinations of the constructors but the performance is horrible
and the case split is really awful.</tt><tt><br>
</tt></p>
<p><tt>My context is, that for a function<br>
</tt></p>
<p>
</p><blockquote type="cite"><tt>MappedReferenceType : C++Type → Bool →
C++Type</tt><tt><br>
</tt><tt>...</tt></blockquote>
<tt></tt><p></p>
<p><tt>its effect on such </tt><tt><tt>C++Type</tt> is computed by
the case-generation</tt><tt><br>
</tt></p>
<p>
</p><blockquote type="cite">
<p><tt>f3 : (x : C++Type) → (v : Bool) → (y : C++Type) →
MappedReferenceType x v ≡ y → ⊤</tt><tt><br>
</tt><tt>f3 x v y p = ?</tt></p>
</blockquote>
<p></p>
<p><tt>where I can split with C-c on x v p simultaneously, and then
eliminate with four further splits on x all occurences of </tt><tt><br>
</tt><tt><br>
</tt>
</p><blockquote type="cite"><tt>f3 : (x : C++Type) → (v : Bool) → (y :
C++Type) → MappedReferenceType x v ≡ y → ⊤</tt><tt><br>
</tt><tt>...</tt><tt><br>
</tt><tt>f3 〚 x &ᵇ 〛ʳ true .(〚 x &ᵇ
〛ʳ) refl = tt</tt><tt><br>
</tt><tt>f3 〚 x &ᵖ 〛ʳ true .(〚 x &ᵖ
〛ʳ) refl = tt</tt><tt><br>
</tt><tt>f3 〚 (x constᵇ) &ᶜ 〛ʳ true .(〚 x 〛ᵇ)
refl = tt</tt><tt><br>
</tt><tt>f3 〚 (x constᵖ) &ᶜ 〛ʳ true .(〚 x 〛ᵖ)
refl = tt</tt><tt><br>
</tt><tt>f3 〚 x &&ᵇ 〛ʳ true .(〚 x &&ᵇ
〛ʳ) refl = tt</tt><tt><br>
</tt><tt>...</tt></blockquote>
<p></p>
<p><tt>Now for observing where two functions "differ", I currently
"create" t</tt><tt>he </tt><tt><tt>≢ cases as the absurd ones
from ≡<br>
</tt></tt></p>
<p>
</p><blockquote type="cite"><tt>f12 : (x : C++Type) → (v : Bool) → (y
z : C++Type) → MappedReferenceType x v ≡ y →
StrippedConversionType x v ≡ z → y ≡ z → ⊥</tt><tt><br>
</tt><tt>...</tt><tt><br>
</tt><tt>f12 〚 x 〛ᶜ true .(remove-const 〚 x 〛ᶜ)
.(remove-const 〚 x 〛ᶜ) refl refl refl = {! !}</tt><tt><br>
</tt><tt>f12 〚 x &ᵇ 〛ʳ false .(〚 x &ᵇ
〛ʳ) .(〚 x &ᵇ 〛ʳ) refl refl refl = {! !}</tt><tt><br>
</tt><tt>f12 〚 x &ᵖ 〛ʳ false .(〚 x &ᵖ
〛ʳ) .(〚 x 〛ᵖ) refl refl () -- </tt><tt><tt>≢</tt>
case</tt><tt><br>
</tt><tt>f12 〚 (x constᵇ) &ᶜ 〛ʳ false .(〚 (x constᵇ) &ᶜ
〛ʳ) .(〚 (x constᵇ) &ᶜ 〛ʳ) refl refl refl = {! !}</tt><tt><br>
</tt><tt>f12 〚 (x constᵖ) &ᶜ 〛ʳ false .(〚 (x constᵖ) &ᶜ
〛ʳ) .(〚 x 〛ᵖ) refl refl () -- </tt><tt><tt>≢</tt>
case</tt><tt><br>
</tt><tt>f12 〚 x &&ᵇ 〛ʳ false .(〚 x
&&ᵇ 〛ʳ) .(〚 x &&ᵇ 〛ʳ) refl
refl refl = {! !}</tt><tt><br>
</tt><tt>...</tt></blockquote>
<tt></tt><p></p>
<p><tt>Regards,</tt><tt><br>
</tt></p>
<p><tt>Christian</tt><tt><br>
</tt></p>
</div>
_______________________________________________<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>