MikeMKH

get-content FILE_NAME -wait | where {$_ -like "*STRING_TO_FILTER*"}

MikeMKH

-- lag (SQL Server 2012+)
select
   PricingDate
  ,Cusip
  ,MarketValue
  ,lag(MarketValue, 1) over (partition by Portfolio, Cusip order by PricingDate) as MarketValue_1DayAgo
  ,lag(MarketValue, 2) over (partition by Portfolio, Cusip order by PricingDate) as MarketValue_2DayAgo
  from Holdings
;

MikeMKH

select
    pricingdate
   ,price
   ,max(price) over (partition by cusip
                     order by pricingdate
                     rows between 30 preceding and current row) as max_price
   ,min(price) over (partition by cusip
                     order by pricingdate
                     rows between 30 preceding and current row) as min_price
   ,avg(price) over (partition by cusip

MikeMKH

Lemma zero_addition_identity_right :
  forall x : nat, x + 0 = x.
Proof.
  intro x; induction x.
  - compute; reflexivity.
  - simpl; f_equal; apply IHx.
Qed.

Lemma zero_addition_identity_left :
  forall x : nat, x = x + 0.

MikeMKH

Require Import Coq.Arith.Arith.
Require Import Omega.

(* from http://stackoverflow.com/a/44039996/2370606 *)
Lemma subtraction_does_not_commute :
  forall a b : nat, a <> b -> a - b <> b - a.
Proof.
  induction a. intros b.
  - now rewrite Nat.sub_0_r.
  - destruct b.

MikeMKH

(* definitions from section 7.3 of Coq Art *)

Section combinatory_logic.

Variables
  (CL : Set)
  (App : CL -> CL -> CL)
  (S : CL)
  (K : CL)
  (I : CL).

MikeMKH

(* exercise 6.29 from Coq Art *)

Check eq_ind.

(*
 eq_ind
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, x = y -> P y 
*)

MikeMKH

(* exercise 6.10 from Coq Art *)

 Inductive month : Set :=
   | January : month
   | February : month
   | March : month
   | April : month
   | May : month
   | June : month
   | July : month

MikeMKH

(* exercise 5.2 from Coq Art *)

Section A_declared.

Variables
  (A : Set)
  (P Q : A -> Prop)
  (R : A -> A -> Prop).

Theorem all_comm :

MikeMKH

(* exercise 5.3 from Coq Art *)

Lemma id_prop : forall P : Prop, P -> P.
Proof.
  intros P H; apply H.
Qed.

Theorem not_False : ~False.
Proof id_prop False.