[Agda] Case split on λ()

[Marcus Christian Lehmann]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190314/7dd0dd90/attachment.html>