-- Copyright 2020 INP Toulouse.
-- Authors : Mathieu Montin.

-- This version of Addition is provided to you free of charge. It is released under the FSF GPL license, http://www.fsf.org/licenses/gpl.html. 
-- As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users  are provided only 
-- with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability. 
-- In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the 
-- software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also there-
-- fore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged 
-- to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to 
-- be ensured and, more generally, to use and operate it in the same conditions as regards security.
-- The fact that you are presently reading this means that you have had knowledge of the FSF GPL version 3 license and that you accept its terms.

module Addition where

open import Data.Nat using ( ; zero ; suc)
open import Relation.Binary.PropositionalEquality
open import Function
open import Relation.Binary.PropositionalEquality.Core
open ≡-Reasoning

_+_ :     
zero + b = b
suc a + b = suc (a + b)

associative+ :  {a b c}  (a + b) + c  a + (b + c)
associative+ {zero} = refl
associative+ {suc a} = cong suc (associative+ {a})

commutative+ :  {a b}  a + b  b + a
commutative+ {zero} = +0
  where
    +0 :  {a}  a  a + zero
    +0 {zero} = refl
    +0 {suc _} = cong suc +0
commutative+ {suc a} = trans (cong suc (commutative+ {a})) +suc
  where
    +suc :  {a b}  suc (a + b)  a + suc b
    +suc {zero} = refl
    +suc {suc _} = cong suc +suc

_*_ :     
zero * b = zero 
suc a * b = b + (a * b)

distributive* :  {a b c}  (a + b) * c  (a * c) + (b * c)
distributive* {zero} = refl
distributive* {suc a} {b} {c} = trans (cong (c +_) (distributive* {a}))
  (sym (associative+ {c} {a * c} {b * c}))

associative* :  {a b c}  a * (b * c)  (a * b) * c
associative* {zero} = refl
associative* {suc a} {b} {c} rewrite distributive* {b} {a * b} {c}
  | sym (associative* {a} {b} {c}) = refl

*0 :  {a}  a * 0  0
*0 {zero} = refl
*0 {suc a} = *0 {a}

*suc :  {a b}  a * suc b  a + (a * b)
*suc {zero} = refl
*suc {suc a} {b} = cong suc (begin
  b + (a * suc b) ≡⟨ cong (b +_) (*suc {a} {b}) 
  b + (a + (a * b)) ≡˘⟨ associative+ {b} {a} {a * b} 
  (b + a) + (a * b) ≡⟨ cong (_+ (a * b)) (commutative+ {b} {a}) 
  (a + b) + (a * b) ≡⟨ associative+ {a} {b} {a * b} 
  a + (b + (a * b)) )

commutative* :  {a b}  a * b  b * a
commutative* {zero} {b} = sym (*0 {b})
commutative* {suc a} {b} = begin
  (b + (a * b)) ≡⟨ cong (b +_) (commutative* {a}) 
  (b + (b * a)) ≡˘⟨ *suc {b} 
  (b * suc a) 

2+5≡7 : 2 + 5  7
2+5≡7 = refl

2+5≡7₁ : 2 + 5  7
2+5≡7₁ = begin 2 + 5 ≡⟨⟩ 1 + 6 ≡⟨⟩ 7  

45*89 : 3 * 45  135
45*89 = begin 3 * 45 ≡⟨⟩ (45 + (2 * 45)) ≡⟨⟩ (45 + (45 + 45)) ≡⟨⟩ 135