[Agda] Komencenta demando.

[Andreas Abel]

See attached file.

I have never seen your language, but I think I guessed correctly...

Cheers,
Andreas

On 25.11.2015 16:14, Serge Leblanc wrote:
> Ĉu iu bondeziras indiki al mi kiel oni uzas _≡[_]_ ?
> Does anyone wish to indicate to me how to use _≡ [_] _?
>
> Dankon.
> Thanks.
>
>
> On 2015-11-19 16:33, Serge Leblanc wrote:
>> Estimata ĉiuj,
>>
>> En funkcio 'suc-conv' mi ne scias kiamaniere indiki la komutecon de
>> adico (+-comm). Verŝajne, ni uzas egalan rezonon enkondukite de
>> _≡[_]_, ĉu ne ? Bedaūrinde, mi ne komprenas kiel uzi ĝin!
>>
>> Bonvolu indiki al mi kiel fari ?
>> Sincere,
>>
>>
>> Dear all,
>>
>> In function 'suc-conv' I don't know how to indicate the commutativity
>> of addition (+-comm). Probably, we use an equal argument introduced
>> from _≡ [_] _, is not it? Unfortunately, I don't understand how to use it!
>>
>> Could you tell me howto do?
>> Sincerely,
>>
>>
>>
>> module Recursive where
>>
>> open import Data.Nat
>> open import Data.Nat.Properties.Simple using (+-comm)
>> open import Relation.Binary.PropositionalEquality as PropEq using
>> (_≡_; refl; cong; cong₂)
>> open PropEq.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_)
>>
>> data ℕ⁰ : Set where
>>   zero : ℕ⁰
>>   2k : ℕ⁰ → ℕ⁰
>>   2k+1 : ℕ⁰ → ℕ⁰
>>
>> suc⁰ : ℕ⁰ → ℕ⁰
>> suc⁰ zero = 2k+1 zero
>> suc⁰ (2k n) = 2k+1 n
>> suc⁰ (2k+1 n) = 2k (suc⁰ n)
>>
>> conv⁰→ : ℕ⁰ → ℕ
>> conv⁰→ zero = zero
>> conv⁰→ (2k n) = conv⁰→ n + conv⁰→ n
>> conv⁰→ (2k+1 n) = suc (conv⁰→ n + conv⁰→ n)
>>
>> conv⁰← : ℕ → ℕ⁰
>> conv⁰← zero = zero
>> conv⁰← (suc n) = suc⁰ (conv⁰← n)
>>
>> suc-conv : (n : ℕ⁰) → conv⁰→ (suc⁰ n) ≡ suc (conv⁰→ n)
>> suc-conv zero = refl
>> suc-conv (2k n) = refl
>> suc-conv (2k+1 n) = {! cong₂ _+_  (suc-conv n) (suc-conv n) !}
>>
>> --
>> Serge Leblanc
>> ------------------------------------------------------------------------
>> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
> --
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
module _ where

open import Data.Nat
open import Data.Nat.Properties.Simple using (+-suc)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
open PropEq.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_)

data ℕ⁰ : Set where
  zero : ℕ⁰
  2k : ℕ⁰ → ℕ⁰
  2k+1 : ℕ⁰ → ℕ⁰

suc⁰ : ℕ⁰ → ℕ⁰
suc⁰ zero = 2k+1 zero
suc⁰ (2k n) = 2k+1 n
suc⁰ (2k+1 n) = 2k (suc⁰ n)

conv⁰→ : ℕ⁰ → ℕ
conv⁰→ zero = zero
conv⁰→ (2k n) = conv⁰→ n + conv⁰→ n
conv⁰→ (2k+1 n) = suc (conv⁰→ n + conv⁰→ n)

conv⁰← : ℕ → ℕ⁰
conv⁰← zero = zero
conv⁰← (suc n) = suc⁰ (conv⁰← n)

suc-conv : (n : ℕ⁰) → conv⁰→ (suc⁰ n) ≡ suc (conv⁰→ n)
suc-conv zero = refl
suc-conv (2k n) = refl
suc-conv (2k+1 n) = begin
  conv⁰→ (suc⁰ (2k+1 n))             ≡[ refl ]
  conv⁰→ (2k (suc⁰ n))               ≡[ refl ]
  conv⁰→ (suc⁰ n) + conv⁰→ (suc⁰ n)  ≡[  cong₂ _+_  (suc-conv n) (suc-conv n) ]
  suc (conv⁰→ n) + suc (conv⁰→ n)    ≡[ cong suc (+-suc (conv⁰→ n) (conv⁰→ n)) ]
  suc (suc (conv⁰→ n + conv⁰→ n))    ≡[ refl ]
  suc (conv⁰→ (2k+1 n))
  ∎