flang practice

1. Your first function

«Квадрат» always returns 0. Write the body so that it returns н multiplied by itself.

What the check appends

утверждение «квадрат трёх — девять»
  утверждаем («Квадрат» от 3) равно 9

утверждение «квадрат минус четырёх — шестнадцать»
  утверждаем («Квадрат» от -4) равно 16

Hint

Multiplication is written in words: н умножить на н.

2. A branch and a promise

«Модуль» promises a result of at least zero but just returns х. Add a branch so the answer is right and the promise is proved.

What the check appends

утверждение «модуль минус пяти — пять»
  утверждаем («Модуль» от -5) равно 5

утверждение «модуль семи — семь»
  утверждаем («Модуль» от 7) равно 7

Hint

если х меньше 0 то 0 минус х иначе х. Inside each branch the compiler knows the branch condition.

3. A type with variants

The traffic light goes red → green → yellow → red. Write «Следующий» with pattern matching.

What the check appends

утверждение «после красного — зелёный»
  утверждаем («Следующий» от вариант Красный) равно вариант Зелёный

утверждение «после зелёного — жёлтый»
  утверждаем («Следующий» от вариант Зелёный) равно вариант Жёлтый

утверждение «после жёлтого — красный»
  утверждаем («Следующий» от вариант Жёлтый) равно вариант Красный

Hint

разбор сигнал, then «случай Красный» with «то вариант Зелёный» for each variant.

4. Folding a list

Compute the sum of a list. The language has no loops, so use a fold.

What the check appends

утверждение «сумма пустого списка — ноль»
  утверждаем («Сумма» от пустой список) равно 0

утверждение «один, два, три — шесть»
  утверждаем («Сумма» от [1, 2, 3]) равно 6

Hint

свёртка элементы начиная с 0 как акк и эл → акк плюс эл

5. A business rule with a promise

Orders of 10 000 and more get a 500 discount, smaller ones get none. The discount must never exceed the total, and that promise must be proved.

What the check appends

утверждение «с 12 000 скидка 500»
  утверждаем («Скидка» от 12000) равно 500

утверждение «с 2 000 скидки нет»
  утверждаем («Скидка» от 2000) равно 0

Hint

Branch on «сумма не меньше 10000»; in the «то» branch the compiler knows that 500 does not exceed the total.

6. A function that never ends

The compiler rejects «Сумма до»: the recursive call does not shrink the argument, so the function would loop forever. Fix the call.

Hint

Recurse on a smaller number: («Сумма до» от (н минус 1)).

7. A promise others can rely on

The check adds «Через удвоение» and a theorem that refers to the property «удвоение длины не меняет» of «Удвоить все». Declare that property.

What the check appends

тотальная функция «Через удвоение»
  принимает элементы: список числа
  возвращает список числа
  для всех элементы обеспечивает «через удвоение длина та же» (длина результат) равен (длина элементы)
  «Удвоить все» от элементы

теорема «через удвоение длина та же»
  дано элементы: список числа
  утверждаем (длина результат) равен (длина элементы)
  по свойству «удвоение длины не меняет»
  следовательно доказано

Hint

для всех элементы обеспечивает «удвоение длины не меняет» (длина результат) равен (длина элементы)

8. A proof by induction

Complete the induction step in the theorem «шаг растит счёт на один».

Hint

Write «то по предположению» in the «Следующий» case.

What’s new

Easier now0

1. Your first function

2. A branch and a promise

3. A type with variants

4. Folding a list

5. A business rule with a promise

6. A function that never ends

7. A promise others can rely on

8. A proof by induction