[Agda] ⊥-elim and proof duplication. Is there another way?

[Guillermo Calderon]

Hi,

You can define a higher order function like this:

```
from-a1 :  ∀{S : (a : A)→ B a → Set}
       → (B a1 → S a1 b1)
       → (a : A) → (b : B a) → S a b
from-a1 f a1 b1 = f b1
from-a1 _ a2 b  = ⊥-elim (fun b)
```

Then,  you define run and gun this way:

```
gun : (a : A) → (b : B a) → C b
gun = from-a1 λ _ → c

run : (a : A) → (b : B a) → gun a b ≡ c
run = from-a1 λ _ → refl
```

By the way,  for this minimal example, there is a better solution:

   run : (a : A) → (b : B a) → gun a b ≡ c
   run .a1 b1 = refl

----------
Guillermo


On 18/07/17 02:10, Apostolis Xekoukoulotakis wrote:
> Consider this example :
>
> ```
> module test where
>
> open import Data.Empty
> open import Relation.Binary.PropositionalEquality
> open import Relation.Nullary
>
>
> data A : Set where
>    a1 a2 : A
>
> data B : A → Set where
>    b1 : B a1
>
> data C : ∀{a} → B a → Set where
>    c : ∀{a} → {b : B a} → C b
>
> fun : ¬ (B a2)
> fun ()
>
>
> gun : (a : A) → (b : B a) → C b
> gun a1 b = c
> gun a2 b = ⊥-elim (fun b)
>
>
> run : (a : A) → (b : B a) → gun a b ≡ c
> run a1 b = refl
> run a2 b = ⊥-elim (fun b)
> ```
>
> For the run function, I have to provide the same proof that I gave in
> the gun function.
> If the proof is big, then it becomes cumbersome and it increases the
> complexity of the code.
>
> Is there a way to not do that?
>
> Keep in mind that in this example, we could avoid ⊥-elim, we could
> simply case split on b. I am referring to the cases where we cannot
> avoid ⊥-elim.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>