Proofs tutorial (#199)

* fix typos

* Tutorials tab and introductory tutorials

* Fix spelling mistakes

* Move tutorials to a local subfolder

* more spelling mistakes

* include newlines at eof

* Constructor constraints tutorial

* Proofs tutorial

* Missing newlines

* Typo fix

* Proofs tutorial style fixes

* Fix proof, update tutorial

* Grammar fix

docs/source/features.md

@@ -279,6 +279,7 @@ createRangeCase low high
         False -> Nothing
 ```
 
+(0-Quantity)=
 ## 0-Quantity Parameters
 
 Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.

docs/source/tutorials.md

@@ -101,3 +101,222 @@ Since the target repository is different than the source, it has to be specified
 ```bash
 agda2hs ./src/agda/Usage.agda -o ./src/haskell/
 ```
+## How (and what) to prove?
+
+[Example source code](https://github.com/agda/agda2hs/tree/master/tutorials/example-proofs)
+
+This tutorial aims to explain how to apply different formal verification techniques compliant with agda2hs and haskell. 
+
+### Constructor constraints
+
+The code described in this section can be found in the file `Triangle.agda`.
+
+Let's say we want to have a data type describing a triangle. A first attempt might look somewhat like this:
+
+```agda
+open import Haskell.Prelude
+
+data Triangle : Set where
+    MkTriangle : (alpha beta gamma : Nat)
+           → Triangle
+
+{-# COMPILE AGDA2HS Triangle #-}
+```
+It's defined with three angles, because maybe thats the only property we are interested in so far. However, three arbitrary angle values do not make a triangle. First of all, they cannot be negative - to make things easier we use natural numbers (`Nat`) to represent the angle values. But that is not enough, three angles can constitute a triangle only if they sum up to 180 degrees and at most one angle is right or obtuse. This can be modeled in Agda:
+
+```agda
+open import Haskell.Prelude
+
+countBiggerThan : ⦃ Ord a ⦄ → List a → a → Int 
+countBiggerThan xs b = length (filter (λ x → (x >= b)) xs)
+
+{-# COMPILE AGDA2HS countBiggerThan #-}
+
+data Triangle : Set where
+    MkTriangle : (alpha beta gamma : Nat)
+        → ⦃ @0 h₁ : (((alpha + beta + gamma) == 180) ≡ True )⦄
+        → @0 ⦃ ((countBiggerThan
+     (alpha ∷ beta ∷  gamma ∷ []) 90 <= 1) ≡ True ) ⦄
+           → Triangle
+
+{-# COMPILE AGDA2HS Triangle #-}
+```
+Adding two hypotheses to the type signature of MkTriangle does the trick. 
+ Notice the use of double brackets, which signify the use of [instance arguments](https://agda.readthedocs.io/en/latest/language/instance-arguments.html): they allow Agda to infer the hypotheses if they are present in the context, instead of having them manually applied each and every time. 
+
+These hypotheses cannot be compiled to Haskell, therefore they have to be erased. This is done by annotating them with [0-quantity parameters](0-Quantity). To correctly annotate a hypothesis with quantity, it has to be explicitly named: in this case h₁. Alternatively, it can also be applied to the whole bracket, like in the second hypothesis. 
+
+The helper function `countBiggerThan` could also operate solely on natural numbers, but this way it show another example of using instance arguments, which map to Haskell's typeclass constraints.
+
+You might want to ask, what is the point of adding hypotheses if they will be erased in Haskell anyway? If you write the remainder of the code in Haskell, it is indeed the case. However, defining the data type in Agda requires the hypotheses to be present when constructing variables of that type:
+
+```agda
+createTriangle : Nat -> Nat -> Nat -> Maybe Triangle
+createTriangle alpha beta gamma 
+    = if (countBiggerThan (alpha ∷ beta ∷  gamma ∷ []) 90 <= 1)
+        then if (alpha + beta + gamma == 180 )
+            then Just (MkTriangle alpha beta gamma) 
+            else Nothing
+        else Nothing
+
+{-# COMPILE AGDA2HS createTriangle #-}
+```
+Unfortunately, the instance arguments are inferred only if presented in exactly the same shape as hypotheses in the constructor, which is the cause of perceived redundancy of the if-then-else statement - chaining the hypotheses with `&&` (the AND operator defined in `Haskell.Prim.Bool` in Agda2hs) will not allow for the reference to be inferred automatically, and the proofs would have to be provided manually. An example for that can be seen in the alternative `createTriangle₁` function:
+
+```agda
+createTriangle₁ : Nat -> Nat -> Nat -> Maybe Triangle
+createTriangle₁ alpha beta gamma 
+    = if ((countBiggerThan (alpha ∷ beta ∷  gamma ∷ []) 90 <= 1) && (alpha + beta + gamma == 180 )) 
+        then (λ ⦃ h₁ ⦄ →  Just (MkTriangle alpha beta gamma 
+            ⦃ &&-rightTrue (countBiggerThan (alpha ∷ beta ∷  gamma ∷ []) 90 <= 1) (alpha + beta + gamma == 180 ) h₁ ⦄ 
+            ⦃ &&-leftTrue (countBiggerThan (alpha ∷ beta ∷  gamma ∷ []) 90 <= 1) (alpha + beta + gamma == 180 ) h₁ ⦄) )
+        else Nothing
+ 
+{-# COMPILE AGDA2HS createTriangle₁ #-}
+
+```
+While using this alternative function offers much cleaner Haskell code as an output (no nested if statements), however the Agda side gets a bit messier. Two things are worth noting here: first, to be able to operate on the hypothesis asserted in the if condition, the branch has to be rewritten as an anonymous function taking the assertion as instance argument. Secondly, to explicitly provide the instance arguments, it also has to be done inside the double curly brackets. 
+
+Lastly, the two functions used to extract conditions from the compound condition: `&&-rightTrue` and `&&-leftTrue` were defined in `Haskell.Law.Bool`. The `Law` folder contains many theorems useful for designing your own proofs. This will be expanded on in following sections. 
+
+### Function or Predicate?
+
+The code described in this section can be found in the file `Ascending.agda`. 
+
+We will try to define ascending order on lists, which will allow us to use statements about the order in later proofs and programs. 
+
+A first attempt at definition could be a function that can provide judgments on instances of lists:
+
+```agda
+isAscending : ⦃ iOrdA : Ord a ⦄ → List a → Bool
+isAscending [] = True
+isAscending (x ∷ []) = True
+isAscending (x ∷ y ∷ xs) = if x <= y then isAscending (y ∷ xs) else False
+
+{-# COMPILE AGDA2HS isAscending #-}
+```
+This function can be compiled to Haskell without any issue, however, when you try using it in proofs you can notice that it is not the most handy definition: since the different cases are anonymous, invoking them is not straightforward and might require defining more proof cases with additional assertions about the values input data (an example of which can be found [further in the tutorial](function-example)) A better definition might be a predicate, instead:
+
+```agda
+data IsAscending₂ {a : Set} ⦃ iOrdA : Ord a ⦄ : List a → Set where
+    Empty : IsAscending₂ []
+    OneElem : (x : a) →  IsAscending₂ (x ∷ [])
+    ManyElem : (x y : a) (xs : List a) 
+        → ⦃ IsAscending₂ (y ∷ xs) ⦄
+        → ⦃ IsTrue (x <= y) ⦄
+        → IsAscending₂ (x ∷ y ∷ xs)
+```
+This data type cannot be compiled to Haskell, as they do not allow to match on specific values. However, some amount of equivalency can be proven between these two definitions. They are not structurally different (one evaluates to True and the other to a data type), therefore they cannot be equal per the `≡` operator. Instead, there occurs the material equivalence relation (`⇔`), such that if the function returns `True`, the predicate holds, and vice versa. Let's try to prove it then!
+
+The signature of the first direction will look like this:
+
+```agda
+proof₁ : ⦃ iOrdA : Ord a ⦄ (xs : List a) → ⦃ IsAscending₂ xs ⦄ → (IsTrue (isAscending xs)) 
+proof xs = ?
+```
+
+> Note: in Agda, you can use [interactive mode](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html#commands-in-context-of-a-goal) to assist in proofs. Question marks will be loaded to open goals. THis feature doesn't work yet seamlessly with agda2hs but the preview of context and splitting based on cases will guide with both more complicated and trivial proofs. 
+
+Since there are three constructors for the `IsAscending₂` predicate, there need to be only three cases in the proof, two of which are trivial:
+
+```agda
+proof₁ : ⦃ iOrdA : Ord a ⦄ (xs : List a) → ⦃ IsAscending₂ xs ⦄ → (IsTrue (isAscending xs)) 
+proof₁ [] = IsTrue.itsTrue 
+proof₁ (x ∷ []) = IsTrue.itsTrue
+proof₁ (x ∷ x₁ ∷ xs) ⦃ (ManyElem .x .x₁ .xs ⦃ h₁ ⦄ ⦃ h₂ ⦄) ⦄ = ?
+```
+In the third case, we need insight into the `IsAscending₂` predicate so it has to be explicitly invoked. Later in the proof we will only need the h₂ hypothesis, but because its the second implicit argument, both need to be stated. The goal is of the shape `IsTrue (isAscending xs)`, but it cannot be easily constructed. Instead, this goal can be mapped to `isAscending xs ≡ True`, which allows to use [chains of equality](https://plfa.github.io/Equality/#chains-of-equations) syntax - transforming the first statement in the equation step by step until we obtain the second statement in a given equality.
+
+```agda
+useEq : {x y : Bool} → x ≡ y → IsTrue x → IsTrue y
+useEq {True} {True} eq is = IsTrue.itsTrue
+
+reverseEq : { x : Bool } → (IsTrue x) → x ≡ True
+reverseEq {False} ()
+reverseEq {True} input = refl 
+
+proof₁ (x ∷ x₁ ∷ xs) ⦃ (ManyElem .x .x₁ .xs ⦃ h₁ ⦄ ⦃ h₂ ⦄) ⦄ = useEq ( sym $
+    begin
+        isAscending (x ∷ x₁ ∷ xs)
+    ≡⟨⟩ 
+        (if x <= x₁ then isAscending (x₁ ∷ xs) else False)
+    ≡⟨ ifTrueEqThen (x <= x₁)  (reverseEq h₂) ⟩ 
+        isAscending (x₁ ∷ xs)
+    ≡⟨ reverseEq (proof₁ (x₁ ∷ xs) ) ⟩ 
+        True
+    ∎ ) IsTrue.itsTrue
+```
+Two helper functions, useEq and reverseEq, had to be added to easily operate on the goal. Even though both of them have trivial proofs, they need to be stated explicitly so that the proper type signature can be invoked. To inspect other helper functions used in the proof, try loading the source code in agda - the definitions all come from `Haskell.Prelude`. 
+
+The reverse direction of the iff proof is, again, substantially more complicated. First, the necessary helper proofs will be discussed.
+
+```agda
+--reductio ad absurdum
+absurd₁ : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
+absurd₁ {False} () b 
+absurd₁ {True} a ()
+```
+Reductio ad absurdum is a necessary tactic for dealing with self-contradictory statements. If such statement is one of the input arguments, this contradiction can be discarded with the [`()` keyword](https://agda.readthedocs.io/en/latest/language/function-definitions.html#absurd-patterns) in place of the contradictory argument. However, if the absurd is arising from some combination of the input arguments, it requires some helper method. 
+
+(function-example)=
+
+```agda
+--inductive hypothesis for isAscending function
+helper₁ : ⦃ iOrdA : Ord a ⦄ (x : a) (xs : List a) → isAscending xs ≡ False → (isAscending (x ∷ xs)) ≡ False
+helper₁ x xs h₁ with (isAscending (x ∷ xs)) in h₂
+helper₁ x (x₁ ∷ xs) h₁ | True  with (x <= x₁)
+helper₁ x (x₁ ∷ xs) h₁ | True | True = magic (absurd₁ h₂ h₁)
+helper₁ x (x₁ ∷ xs) h₁ | True | False = sym h₂
+helper₁ x xs h₁ | False = refl
+```
+Here is a helper method for the inductive hypothesis. Notice that where in the predicate syntax we were able to pattern-match on the different constructor, when working with a function, the only way to narrow down to different cases is to pattern match on the possible values of the function output. The [`with ... in` syntax](https://agda.readthedocs.io/en/latest/language/with-abstraction.html) can be used in such cases. In the first usage of the syntax, the output of the function is needed to be applied in the proof, so it needs to be saved *in* a value to be accessed in the context. This is what applying `in h₂` achieves. In the second usage, Agda manages to simplify the necessary arguments automatically, so it is not necessary to add the assertion to the syntax. 
+
+The applied `absurd₁` function can be given as input argument to the `magic` function to resolve the internal contradiction. `magic` lives in `Haskell.Prim` which also needs to be imported. 
+
+```agda
+--proof for (function returns true) → predicate holds
+theorem₂ : ⦃ iOrdA : Ord a ⦄ (xs : List a) 
+    → (IsTrue (isAscending xs)) → IsAscending₂ xs
+theorem₂ [] h₁ = Empty
+theorem₂ (x ∷ []) h₁ = OneElem x
+theorem₂ (x ∷ x₁ ∷ xs) h₁ with (isAscending xs) in h₂ | (x <= x₁) in h₃
+theorem₂ (x ∷ x₁ ∷ xs) h₁ | True  | True = ManyElem x x₁ xs  
+    ⦃ theorem₂helper (x₁ ∷ xs) h₁ ⦄ ⦃ useEq ( sym $ h₃ ) IsTrue.itsTrue ⦄
+theorem₂ (x ∷ x₁ ∷ xs) ()    | _  | False 
+theorem₂ (x ∷ x₁ ∷ xs) h₁ | False | True = magic (
+         absurd₁ (reverseEq h₁) (helper₁ x₁ xs h₂) )
+```
+
+Finally, the proof can be constructed. The recursive case of the proof had to be split into three different cases, but in the place where one would expect to be able to use `theorem₂` recursively, `theorem₂helper` is used instead: 
+
+```agda
+--recursion helper
+postulate3
+   theorem₂helper : ⦃ iOrdA : Ord a ⦄ (xs : List a) → (IsTrue (isAscending xs)) → IsAscending₂ xs
+```
+
+The `theorem₂helper` is a definition of the same type as the actual proof, but without a proof attached - it was only postulated. [Postulates](https://agda.readthedocs.io/en/latest/language/postulates.html) are in general a bad practice. Here it was necessary, as the termination check did not recognize that it is being applied to a recursive case. However, doesn't this invalidate the whole proof? Since postulates are a bad practice, can we do better? Turns out, termination checks on recursive cases [is a known issue when using `with abstraction`](https://agda.readthedocs.io/en/latest/language/with-abstraction.html#termination-checking). Thus, in the next attempt, we can get rid of the postulate:
+
+```agda
+helper₂ : ⦃ iOrdA : Ord a ⦄ (x : a) (xs : List a) 
+    → (IsTrue (isAscending (x ∷ xs))) → (IsTrue (isAscending xs))
+helper₂ x [] h₁ = IsTrue.itsTrue
+helper₂ x (x₁ ∷ xs) h₁ with (x <= x₁) in h₂
+helper₂ x (x₁ ∷ xs) h₁ | True = h₁
+helper₂ x (x₁ ∷ xs) () | False 
+
+--proof for (function returns true) → predicate holds version 2
+theorem₃ : ⦃ iOrdA : Ord a ⦄ (xs : List a) 
+    → (IsTrue (isAscending xs)) → IsAscending₂ xs
+theorem₃ [] h₁ = Empty
+theorem₃ (x ∷ []) h₁ = OneElem x
+theorem₃ (x ∷ x₁ ∷ xs) h₁ with (theorem₃ (x₁ ∷ xs) (helper₂ x (x₁ ∷ xs) h₁)) 
+theorem₃ (x ∷ x₁ ∷ xs) h₁ | _ with (x <= x₁) in h₂ 
+theorem₃ (x ∷ x₁ ∷ xs) h₁ | h₃ | True  = ManyElem x x₁ xs ⦃ h₃ ⦄ ⦃ useEq ( sym $ h₂ ) IsTrue.itsTrue ⦄
+theorem₃ (x ∷ x₁ ∷ xs) () | _  | False 
+```
+We need another helper function to obtain the correct hypothesis about the tail of the list, but thanks to this approach we can remove one of the assertions about the input values. On the other hand, we need to break up the single `with` assertion into two different lines - if both the new recursive hypothesis (`h₃`) and `h₂` were defined in the same step, Agda wouldn't be able to implicitly apply `h₂` in the `h₁` hypothesis and reason about it being a contradiction in the last case. This way, we finally obtain a correct proof. 
+
+With these proofs, the differences between using these two different styles of describing properties of the code are clear, and some basic principles of building proofs were demonstrated. 
+
+From all the functions and data types discussed, only the first can be compiled into Haskell. The predicate type class and the proofs cannot be compiled as they use concepts that are not supported by Haskell or agda2hs. However, they shouldn't be compiled; they should remain on the "Agda side" as the formal verification of the written code. 

tutorials/example-proofs/Ascending.agda

@@ -0,0 +1,93 @@
+module Ascending where
+
+open import Haskell.Prelude
+open import Haskell.Prim 
+
+-- function judging ascending order on lists
+isAscending : ⦃ iOrdA : Ord a ⦄ → List a → Bool
+isAscending [] = True
+isAscending (x ∷ []) = True
+isAscending (x ∷ y ∷ xs) = if x <= y then isAscending (y ∷ xs) else False
+
+{-# COMPILE AGDA2HS isAscending #-}
+
+-- data type defining a postulate of ascending order on lists
+data IsAscending₂ {a : Set} ⦃ iOrdA : Ord a ⦄ : List a → Set where
+    Empty : IsAscending₂ []
+    OneElem : (x : a) →  IsAscending₂ (x ∷ [])
+    ManyElem : (x y : a) (xs : List a) 
+        → ⦃ IsAscending₂ (y ∷ xs) ⦄
+        → ⦃ IsTrue (x <= y) ⦄
+        → IsAscending₂ (x ∷ y ∷ xs)
+
+-- helpers for transition between different expressions of truth
+useEq : {x y : Bool} → x ≡ y → IsTrue x → IsTrue y
+useEq {True} {True} eq is = IsTrue.itsTrue
+
+reverseEq : { x : Bool } → (IsTrue x) → x ≡ True
+reverseEq {False} ()
+reverseEq {True} input = refl 
+
+
+-- proof for predicte holds → (function is true)
+theorem₁ : ⦃ iOrdA : Ord a ⦄ (xs : List a) → ⦃ IsAscending₂ xs ⦄ → (IsTrue (isAscending xs)) 
+theorem₁ [] = IsTrue.itsTrue 
+theorem₁ (x ∷ []) = IsTrue.itsTrue
+theorem₁ (x ∷ x₁ ∷ xs) ⦃ (ManyElem .x .x₁ .xs ⦃ h₁ ⦄ ⦃ h₂ ⦄) ⦄ = useEq ( sym $
+    begin
+        isAscending (x ∷ x₁ ∷ xs)
+    ≡⟨⟩ 
+        (if x <= x₁ then isAscending (x₁ ∷ xs) else False)
+    ≡⟨ ifTrueEqThen (x <= x₁)  (reverseEq h₂) ⟩ 
+        isAscending (x₁ ∷ xs)
+    ≡⟨ reverseEq (theorem₁ (x₁ ∷ xs) ) ⟩ 
+        True
+    ∎ ) IsTrue.itsTrue
+
+--reductio ad absurdum
+absurd₁ : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
+absurd₁ {False} () b 
+absurd₁ {True} a ()
+
+--inductive hypothesis for isAscending function
+helper₁ : ⦃ iOrdA : Ord a ⦄ (x : a) (xs : List a) → isAscending xs ≡ False → (isAscending (x ∷ xs)) ≡ False
+helper₁ x xs h₁ with (isAscending (x ∷ xs)) in h₂
+helper₁ x (x₁ ∷ xs) h₁ | True  with (x <= x₁)
+helper₁ x (x₁ ∷ xs) h₁ | True | True = magic (absurd₁ h₂ h₁)
+helper₁ x (x₁ ∷ xs) h₁ | True | False = sym h₂
+helper₁ x xs h₁ | False = refl
+
+--recursion helper
+postulate
+   theorem₂helper : ⦃ iOrdA : Ord a ⦄ (xs : List a) 
+    → (IsTrue (isAscending xs)) → IsAscending₂ xs
+
+--proof for (function returns true) → predicate holds version 1 (wrong)
+theorem₂ : ⦃ iOrdA : Ord a ⦄ (xs : List a) 
+    → (IsTrue (isAscending xs)) → IsAscending₂ xs
+theorem₂ [] h₁ = Empty
+theorem₂ (x ∷ []) h₁ = OneElem x
+theorem₂ (x ∷ x₁ ∷ xs) h₁ with (isAscending xs) in h₂ | (x <= x₁) in h₃
+theorem₂ (x ∷ x₁ ∷ xs) h₁ | True  | True = ManyElem x x₁ xs  
+    ⦃ theorem₂helper (x₁ ∷ xs) h₁ ⦄ ⦃ useEq ( sym $ h₃ ) IsTrue.itsTrue ⦄
+theorem₂ (x ∷ x₁ ∷ xs) () | _     | False 
+theorem₂ (x ∷ x₁ ∷ xs) h₁ | False | True = magic (
+         absurd₁ (reverseEq h₁) (helper₁ x₁ xs h₂) )
+
+helper₂ : ⦃ iOrdA : Ord a ⦄ (x : a) (xs : List a) 
+    → (IsTrue (isAscending (x ∷ xs))) → (IsTrue (isAscending xs))
+helper₂ x [] h₁ = IsTrue.itsTrue
+helper₂ x (x₁ ∷ xs) h₁ with (x <= x₁) in h₂
+helper₂ x (x₁ ∷ xs) h₁ | True = h₁
+helper₂ x (x₁ ∷ xs) () | False 
+
+--proof for (function returns true) → predicate holds version 2
+theorem₃ : ⦃ iOrdA : Ord a ⦄ (xs : List a) 
+    → (IsTrue (isAscending xs)) → IsAscending₂ xs
+theorem₃ [] h₁ = Empty
+theorem₃ (x ∷ []) h₁ = OneElem x
+theorem₃ (x ∷ x₁ ∷ xs) h₁ with (theorem₃ (x₁ ∷ xs) (helper₂ x (x₁ ∷ xs) h₁)) 
+theorem₃ (x ∷ x₁ ∷ xs) h₁ | _ with (x <= x₁) in h₂ 
+theorem₃ (x ∷ x₁ ∷ xs) h₁ | h₃ | True  = ManyElem x x₁ xs 
+    ⦃ h₃ ⦄ ⦃ useEq ( sym $ h₂ ) IsTrue.itsTrue ⦄
+theorem₃ (x ∷ x₁ ∷ xs) () | _  | False