[Agda] Case split on λ()

[Apostolis Xekoukoulotakis]

Marcus, I could not follow your example, but it seems that you are trying
to case split a function, which is not possible.

```
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Empty
open import Relation.Nullary


fun : ¬ (2 ≡ 2) → ⊥
fun ¬x =  ? -- ⊥-elim (¬x refl)

```


On Thu, Mar 14, 2019 at 9:15 AM Marcus Christian Lehmann <
lehmann at tet.tu-berlin.de> wrote:

> Hello Agda Community,
>
> The case-split C-c on proof of ≡ works great and even leaves out
> impossible cases. But for case-splits of proofs of it's negation ≢ I get
>
> Cannot split on argument of non-datatype 〚 x₁ 〛ᵇ ≢ 〚 x₁ 〛ᵇ when checking
> that the expression ? has type ⊥
>
> Is there a nice way to have case-split work for these cases (i.e. on λ() )?
>
> 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.
>
> My context is, that for a function
>
> MappedReferenceType : C++Type → Bool → C++Type
> ...
>
> its effect on such C++Type is computed by the case-generation
>
> f3 : (x : C++Type) → (v : Bool) → (y : C++Type) → MappedReferenceType x v
> ≡ y → ⊤
> f3 x v y p = ?
>
> where I can split with C-c on x v p simultaneously, and then eliminate
> with four further splits on x all occurences of
>
> f3 : (x : C++Type) → (v : Bool) → (y : C++Type) → MappedReferenceType x v
> ≡ y → ⊤
> ...
> f3 〚 x &ᵇ 〛ʳ          true  .(〚 x &ᵇ 〛ʳ)           refl = tt
> f3 〚 x &ᵖ 〛ʳ          true  .(〚 x &ᵖ 〛ʳ)           refl = tt
> f3 〚 (x constᵇ) &ᶜ 〛ʳ true  .(〚 x 〛ᵇ)              refl = tt
> f3 〚 (x constᵖ) &ᶜ 〛ʳ true  .(〚 x 〛ᵖ)              refl = tt
> f3 〚 x &&ᵇ 〛ʳ         true  .(〚 x &&ᵇ 〛ʳ)          refl = tt
> ...
>
> Now for observing where two functions "differ", I currently "create" the ≢
> cases as the absurd ones from ≡
>
> f12 : (x : C++Type) → (v : Bool) → (y z : C++Type) → MappedReferenceType x
> v ≡ y → StrippedConversionType x v ≡ z → y ≡ z → ⊥
> ...
> f12 〚 x             〛ᶜ true  .(remove-const 〚 x 〛ᶜ) .(remove-const 〚 x 〛ᶜ)
> refl refl refl = {!  !}
> f12 〚 x &ᵇ          〛ʳ false .(〚 x &ᵇ           〛ʳ) .(〚 x &ᵇ           〛ʳ)
> refl refl refl = {!  !}
> f12 〚 x &ᵖ          〛ʳ false .(〚 x &ᵖ           〛ʳ) .(〚 x              〛ᵖ)
> refl refl ()            -- ≢ case
> f12 〚 (x constᵇ) &ᶜ 〛ʳ false .(〚 (x constᵇ) &ᶜ  〛ʳ) .(〚 (x constᵇ) &ᶜ  〛ʳ)
> refl refl refl = {!  !}
> f12 〚 (x constᵖ) &ᶜ 〛ʳ false .(〚 (x constᵖ) &ᶜ  〛ʳ) .(〚 x              〛ᵖ)
> refl refl ()            -- ≢ case
> f12 〚 x &&ᵇ         〛ʳ false .(〚 x &&ᵇ          〛ʳ) .(〚 x &&ᵇ          〛ʳ)
> refl refl refl = {!  !}
> ...
>
> Regards,
>
> Christian
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190314/299a3325/attachment.html>