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

    (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

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

(** **** 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

{-# 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

(*   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

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

Inductive in_order_merge {X : Type} : (list X) -> (list X) -> (list X) -> Prop :=
  | iom_nil : forall (xs : list X),
                in_order_merge [] xs xs
  | iom_seq_l : forall (x : X) (xs ys zs : list X),
                  in_order_merge xs ys zs -> in_order_merge (x::xs) ys (x::zs)
  | iom_seq_r : forall (y : X) (xs ys zs : list X),
                  in_order_merge xs ys zs -> in_order_merge xs (y::ys) (y::zs).

Theorem iom_seq_l_inverse  :
  forall {X : Type} (x : X) (xs ys zs : list X),

nkaretnikov

(* https://coq.inria.fr/distrib/current/refman/Reference-Manual022.html *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y ;
  leibniz_eqb : forall x y, x = y -> eqb x y = true }.

Instance Eq_nat : Eq nat :=
  { eqb x y := beq_nat x y }.
(* eqb_leibniz *)
  intros. apply beq_nat_true. apply H.

nkaretnikov

(* https://coq.inria.fr/distrib/current/refman/Reference-Manual022.html *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool ;
  eqb_leibniz : forall x y, eqb x y = true -> x = y }.

Instance Eq_nat : Eq nat :=
  { eqb x y := beq_nat x y }.
  intros. apply beq_nat_true. apply H. Qed.

Fixpoint elem {X : Type} {eq : Eq X} (x : X) (xs : list X) : bool :=