[Agda] test report

[mechvel at scico.botik.ru]

On 2021-03-15 13:01, Nils Anders Danielsson wrote:
> On 2021-03-14 23:47, mechvel at scico.botik.ru wrote:
>> * I failed to separate the proof.
> 
> I suggest that you try to mark the proof parts with @0, so that they 
> are
> erased by the compiler:
> 
>   
> https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html


Here is a self-contained example
(a small archive copy attached - for the case if the below source in 
wrongly printed in e-mail editor).

Imagine that  efficient+  pretends to be more efficient than  Nat._+_.
But it is needed to prove the properties for it, like  Commutative, 
Associative, etc,
and that it is difficult.
So, the program proves the result equality for  efficient+  to  _+_,
and proves the properties by using this equality.
Imagine that the only practically feasible way to prove this equality is 
to
incorporate the proof into the recursive structure for  efficient+,
which makes it  efficient+withProof  returning a pair.
This is shown in in the below code.
Then, define
   efficient+ m =  proj₁ ∘ efficient+withProof m,

and (Commutative efficient+) is proved by using efficient+withProof  and 
+-comm.
Imagine that the proofs are not erased here.
How to force erasing by @erase as much as possible for this example?
Where to set @0 ?

Thanks,

--
SM


-----------------------------------------------------------
open import Algebra.Definitions using (Commutative)
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Nat.Properties using (+-comm)
open import Data.Product using (_,_; proj₁; Σ)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality as PE
                             using (_≡_; refl; sym; cong)
import Relation.Binary.Reasoning.Setoid as EqReasoning


efficient+withProof : (m n : ℕ) → Σ ℕ (\s → s ≡ m + n)

efficient+withProof 0       n =  (n , refl)
efficient+withProof (suc m) n =
   let
     (eff-m-n , eff-m-n≡m+n) = efficient+withProof m n
     s = suc eff-m-n

     s≡1+m+n : s ≡ (suc m) + n
     s≡1+m+n = cong suc eff-m-n≡m+n
   in
   (s , s≡1+m+n)

efficient+ : (m n : ℕ) → ℕ
efficient+ m =  proj₁ ∘ efficient+withProof m

efficient+comm : Commutative _≡_ efficient+
efficient+comm m n =
   let
     open EqReasoning (PE.setoid ℕ)
     (eff[m,n] , eff[m,n]≡m+n) = efficient+withProof m n
     (eff[n,m] , eff[n,m]≡n+m) = efficient+withProof n m
   in
   begin efficient+ m n  ≡⟨ eff[m,n]≡m+n ⟩
         m + n           ≡⟨ +-comm m n ⟩
         n + m           ≡⟨ sym (eff[n,m]≡n+m) ⟩
         efficient+ n m
   ∎
-----------------------------------------------------------------


-------------- next part --------------
A non-text attachment was scrubbed...
Name: TT.agda.zip
Type: application/zip
Size: 752 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210315/7f7e617f/attachment.zip>