[Agda] Case split on λ()

[Jason -Zhong Sheng- Hu]

Hi Marcus,

this signature looks simply a decision procedure for propositional equality between u and v, and if agda is able to figure out the proof term, I even speculate that u and v are of an inductively defined type. If that's the case, why did you involve f and g? it might hint that it's not the signature that you might be looking for, or you are complicating a simple problem.

Sincerely Yours,

Jason Hu
________________________________
From: Marcus Christian Lehmann <lehmann at tet.tu-berlin.de>
Sent: March 14, 2019 4:09 PM
To: Jason -Zhong Sheng- Hu; Apostolis Xekoukoulotakis
Cc: agda list
Subject: Re: [Agda] Case split on λ()

Thank you for pointing this dead-end out.

Therefore I will proceed with

f : ∀ x u v → f x ≡ u → g x ≡ v → u ≡ v ⊎ u ≢ v
f x u v p1 p2 = ?

where proof search seems mighty enough to figure out "inj₁ refl" or "inj₂ (λ ())" for the right hand side (after case splitting on x).

regards,

Am 14.03.19 um 17:42 schrieb Jason -Zhong Sheng- Hu:
Hi Marcus,

you shouldn't expect to be able to pattern match on functions in regular type theory based on intuitionistic type theory.

negation is a function so it should be applied to something.

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se><mailto:agda-bounces at lists.chalmers.se> on behalf of Marcus Christian Lehmann <lehmann at tet.tu-berlin.de><mailto:lehmann at tet.tu-berlin.de>
Sent: March 14, 2019 12:36 PM
To: Apostolis Xekoukoulotakis
Cc: agda list
Subject: Re: [Agda] Case split on λ()

I have attached a more complete example but it boils down to convincing
Agda that ¬ 2 ≡ 2 should be empty (following the very readable error
message), e.g.

```
fun : ¬ (2 ≡ 2) → ⊥
fun () -- Error: "¬ 2 ≡ 2 should be empty, but that's not obvious to me"
```


Am 14.03.19 um 09:09 schrieb 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)
>
> ```


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