<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>