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

[Apostolis Xekoukoulotakis]

This is a nice trick. I am concerned about two things though. We cannot use
this technique selectively to specific functions, because we do not know a
priori whether we will create a function like 'run'.
Doing this for all functions that use '⊥-elim' might be possible if it
didn't make the code difficult to read/ didn't take too much time to
implement.

My function
<https://github.com/xekoukou/sparrow/blob/master/agda/LinFunContruct.agda#L56>
has 21 cases with '⊥-elim' and many other cases.

I could create a 'view' type of the input that does not result into
'⊥-elim', and then perform your trick. That would work.I am still unsure
whether it is worth it.

On Wed, Jul 19, 2017 at 6:23 PM, Guillermo Calderon <calderon at fing.edu.uy>
wrote:

>
> 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
>>
>>
>
> _______________________________________________
> 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/20170720/615e9bfc/attachment.html>