Skip to content

Instantly share code, notes, and snippets.

View MikeMKH's full-sized avatar
:shipit:
Learning about logic programming with Prolog

Mike Harris MikeMKH

:shipit:
Learning about logic programming with Prolog
27 followers · 15 following
  • Milwaukee, WI
  • 18:09 (UTC -05:00)
View GitHub Profile
@MikeMKH
MikeMKH / filter.ps1
Created June 9, 2017 17:11
Powershell example of tail filtering a hot file
get-content FILE_NAME -wait | where {$_ -like "*STRING_TO_FILTER*"}
@MikeMKH
MikeMKH / example.sql
Last active June 8, 2017 11:45
TSQL example of lag window function and how to synthesize a lag window function
-- 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
MikeMKH / example.sql
Created June 1, 2017 23:15
TSQL example of using windowing functions with frames
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
MikeMKH / addition.v
Created May 22, 2017 11:44
Addition properties in Coq
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
MikeMKH / commute.v
Created May 18, 2017 22:09
Proof that subtraction is not commutative using Coq.
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
MikeMKH / combinator.v
Created May 12, 2017 11:50
Combinator calculus proofs with Coq
(* 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
MikeMKH / ex6_29.v
Created May 10, 2017 11:44
Example of proof by elimination with Coq from Coq Art
(* 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
MikeMKH / ex6_10.v
Last active May 7, 2017 14:00
Example of case statement with Coq from Coq Art
(* exercise 6.10 from Coq Art *)
Inductive month : Set :=
| January : month
| February : month
| March : month
| April : month
| May : month
| June : month
| July : month
@MikeMKH
MikeMKH / ex5_2.v
Created May 3, 2017 11:41
Predicate calculus proofs in Coq from Coq Art
(* exercise 5.2 from Coq Art *)
Section A_declared.
Variables
(A : Set)
(P Q : A -> Prop)
(R : A -> A -> Prop).
Theorem all_comm :
@MikeMKH
MikeMKH / ex5_3.v
Created May 3, 2017 11:40
Negation examples in Coq from Coq Art
(* 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.