[Agda] Agda beginner.

[Sergei Meshveliani]

On Sun, 2015-04-26 at 18:52 +0200, Serge Leblanc wrote:
> Can anyone show me how one proves eq-mult? Thank you!
> 
> 
> module Hermes where
>   open import Data.Nat
> 
> _⊹_ : ℕ → ℕ → ℕ
> n ⊹ m = fold m suc n
> 
> _⋆_ : ℕ → ℕ → ℕ
> n ⋆ m = fold zero (λ x → x ⊹ m) n 
> 
> data _≡_ {A : Set} : A → A → Set where
>   refl : (a : A) → a ≡ a
> 
> eq-suc : {n m : ℕ} → n ≡ m → suc n ≡ suc m
> eq-suc (refl x) = refl (suc x)
> 
> eq-plus : (n m : ℕ) → (n + m) ≡ (n ⊹ m)
> eq-plus zero m = refl m
> eq-plus (suc n) m = eq-suc (eq-plus n m)
> 
> eq-mult : (n m : ℕ) → (n * m) ≡ (n ⋆ m)
> eq-mult zero m = refl zero
> eq-mult (suc n) m = {!!}
> [..]
> 

See the attachment.
It
1) imports _≡_ and refl           from Standard library,
2) applies  +-comm  and  PE.cong  from Standard library,
3) applies the  begin_ ... _∎  function from Standard library to compose
                               equalities by transitivity.

Alternatively, you needed to prove the congruence of _⊹ _ by the first
argument.

Regards,

------
Sergei

-------------- next part --------------
open import Data.Nat
open import Data.Nat.Properties.Simple                  using (+-comm)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; refl)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_)

_⊹_ : ℕ → ℕ → ℕ
n ⊹ m = fold m suc n

_⋆_ : ℕ → ℕ → ℕ
n ⋆ m = fold zero (λ x → x ⊹ m) n 

eq-plus : (n m : ℕ) → (n + m) ≡ (n ⊹ m)
eq-plus zero    m = refl  
eq-plus (suc n) m = PE.cong suc (eq-plus n m)

eq-mult : (n m : ℕ) → (n * m) ≡ (n ⋆ m)
eq-mult zero    m =  refl 
eq-mult (suc n) m =  
                begin  
                  suc n * m     ≡[ refl ]
                  m + (n * m)   ≡[ +-comm m (n * m) ]
                  (n * m) + m   ≡[ eq-plus (n * m) m ]
                  (n * m) ⊹ m   ≡[ PE.cong (\x → x ⊹ m) (eq-mult n m) ]
                  (n ⋆ m) ⊹ m  
                ∎