<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" 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>
<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; -webkit-text-stroke-width: 0px; background-color: rgb(250, 250, 250); text-decoration-style: initial; text-decoration-color: initial; display: inline !important; 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><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>
<blockquote type="cite"><tt>MappedReferenceType : C++Type → Bool →
C++Type</tt><tt><br>
</tt><tt>...</tt></blockquote>
<tt></tt></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>
<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><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>
<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><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>
<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><tt>Regards,</tt><tt><br>
</tt></p>
<p><tt>Christian</tt><tt><br>
</tt></p>
</body>
</html>