nkaretnikov

import Control.Applicative
import Data.Int
import Data.List

newtype Milray = Milray Int64 deriving Show

projectShareValue :: [Int64] -> Milray
projectShareValue shares =
    Milray $ floor $ fromIntegral (10::Int64) * lg (g * 2) * (patrons - 1)
  where

nkaretnikov

(*   SCase := "test x = false" : String.string *)
(*   Case := "iom_seq" : String.string *)
(*   X : Type *)
(*   test : X -> bool *)
(*   x : X *)
(*   xs : list X *)
(*   ys : list X *)
(*   zs : list X *)
(*   Hiom : in_order_merge xs ys zs *)
(*   Hl1 : filter test (x :: xs) = x :: xs *)

nkaretnikov

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes          #-}

import Data.Functor
import Data.Functor.Identity

type Lens  s t a b = Functor f => (a -> f b) -> s -> f t
-- s == t and a == b
type Lens' s   a   = Functor f => (a -> f a) -> s -> f s

nkaretnikov

(** **** Exercise: 2 stars, optional (conj_fact) *)
(** Construct a proof object demonstrating the following proposition. *)

Theorem conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R.
Proof.
  intros P Q R HPQ HQR.
  apply conj.
  (* Case "left". *)
    inversion HPQ as [HP HQ].
    apply HP.

nkaretnikov

Inductive natlist : Type :=
  | nnil : natlist
  | ncons : nat -> natlist -> natlist.

Check natlist_ind.
(* ===> (modulo a little variable renaming for clarity)
   natlist_ind :
      forall P : natlist -> Prop,
         P nnil  ->
         (forall (n : nat) (l : natlist), P l -> P (ncons n l)) ->

nkaretnikov

    (old_shares, old_share_value, expected_share_value) <- testDB $ do
        old_project_shares <- fetchProjectSharesDB project_id
        old_user_shares    <- getBy (UniquePledge user_id project_id) >>= \case
            Nothing -> return 0
            Just p  -> return $ pledgeFundedShares $ entityVal p
        return ( old_user_shares
               , projectComputeShareValue old_project_shares
               , projectComputeShareValue $
                     shares : delete old_user_shares old_project_shares )

nkaretnikov

Theorem optimize_plus0_sound: forall a,
  aeval (optimize_plus0 a) = aeval a.
Proof.
  intros a.
  induction a.
  Case "ANum". reflexivity.
  Case "APlus". destruct a2.
    SCase "a2 = ANum n". destruct n.
      SSCase "n = 0". simpl. rewrite IHa1. rewrite plus_0_r. reflexivity.
      SSCase "n <> 0". simpl. rewrite IHa1. reflexivity.

nkaretnikov

Theorem optimize_plus_mult_l_sound: forall a,
  aeval (optimize_plus_mult_l a) = aeval a.
Proof.
  intros a. induction a.
    Case "ANum". reflexivity.
    Case "APlus". destruct a1.
      SCase "a1 = ANum".
        simpl. rewrite IHa2. reflexivity.
      SCase "a1 = APlus".
        simpl. destruct a1_1;

nkaretnikov

Theorem fact_3 :
  fact_in_coq / update empty_state X 3
              || (update
                    (update
                       (update
                          (update
                             (update
                                (update
                                   (update
                                      (update

nkaretnikov

-- For haskell202

import Data.List (intercalate)

main :: IO ()
main = loop [] []
  where
    split = intercalate ", " . filter (not . null)
    loop animal attribute = do
      animal'    <- getLine