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

-- This version of Tutorial 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 Tutorial where

data  : Set where
  zero : 
  suc  :   

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : A  List A  List A

infixr 20 _∷_

data Vec {a} (A : Set a) :   Set a where
  [] : Vec A zero
  _∷_ :  {n}  A  Vec A n  Vec A (suc n)

data Even :   Set where
  z-even : Even zero
  s-even :  {n}  Even n  Even (suc (suc n))

six : 
six = suc (suc (suc (suc (suc (suc zero)))))

6-even : Even six
6-even = s-even (s-even (s-even z-even))

data dummy {a b} : Set a  Set b where

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

size :  {a} {A : Set a}  List A  
size []        = zero
size (hd  tl) = suc (size tl)

myList : List 
myList = zero  []

sizeImp : 
sizeImp = size myList

sizeExp : 
sizeExp = size {A = } myList

_++_ :  {a} {A : Set a}  List A  List A  List A
[]        ++ l = l
(hd  tl) ++ l = hd  (tl ++ l)

data _≡_ {a} {A : Set a} (x : A) : A  Set where
  refl : x  x

cong :  {a b} {A : Set a} {B : Set b} {x y} (f : A  B)  x  y  f x  f y
cong f refl = refl

≡size :  {a} {A : Set a} {l l₁ : List A}  (size l + size l₁)  size (l ++ l₁)
≡size {l = []} = refl
≡size {l = hd  tl} = cong suc (≡size {l = tl})

_++̬_ :  {n n₁ a} {A : Set a}  Vec A n  Vec A n₁  Vec A (n + n₁)
[] ++̬ v₂ = v₂
(x  v₁) ++̬ v₂ = x  (v₁ ++̬ v₂)

data  : Set where

¬ :  {a}  Set a  Set a
¬ A = A  

data Dec {a} (A : Set a) : Set a where
  yes : (p : A)  Dec A
  no  : (¬p : ¬ A)  Dec A

dec≡ :  {x y : }  Dec (x  y)
dec≡ {zero}  {zero}  = yes refl
dec≡ {zero}  {suc y} = no  ())
dec≡ {suc x} {zero}  = no  ())
dec≡ {suc x} {suc y} with dec≡ {x} {y}
dec≡ {suc x} {suc y} | yes x≡y = yes (cong suc x≡y)
dec≡ {suc x} {suc y} | no ¬x≡y = no  {refl  (¬x≡y refl)})