This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def int2elem(x): | |
rep = [] | |
for i in range(n): | |
rep.append(x&1) | |
x >>= 1; | |
return tuple(rep) | |
def elem2int(block): | |
x = 0 | |
for i,b in enumerate(block): |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// IMPL:parse_line | |
macro_rules! parse_line { ($($t: ty),+) => ({ | |
let mut line = String::new(); | |
std::io::stdin().read_line(&mut line).unwrap(); | |
let mut iter = line.split_whitespace(); | |
($(iter.next().unwrap().parse::<$t>().unwrap()),+) | |
})} | |
// IMPL:parse_list |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Proof on interchangeability between strong induction and weak induction. | |
Helped by https://github.com/tchajed/strong-induction. *) | |
Definition w_ind := forall (P : nat -> Prop), P 0 -> | |
(forall n, P n -> P (S n)) | |
-> forall n, P n. | |
Definition s_ind := forall (P : nat -> Prop), P 0 -> | |
(forall n, 0 < n -> (forall k, k < n -> P k) -> P n) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(*doc generation command | |
coqtop -compile infix.v -o infix.vo && # compile | |
coqdoc infix.v --no-index && # coqdoc | |
sed -i -e 's/monospace/"Ubuntu Mono"/g' coqdoc.css && # use UbuntuMono instread of default monospace typeface. it will be used for code section. | |
sed -i -e 's/>\( \+\)</><pre>\1<\/pre></g' infix.html && # make spaces visible (especially in code) to preserve aligning. | |
echo "pre { font-family: "Ubuntu Mono"; display: inline; margin: 0; }" >> coqdoc.css # style for 'pre' making above line work. | |
*) | |
(** * Predefinition *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# code for calculating solution for 3rd case of exerciseno.5 of setion 10.6 from the book Discrete Mathematics and Its Applications 7th ed. | |
# can be used for general dijkstra solver | |
def show_graph_entry(ls): | |
return "[" + " ".join(map(lambda u: f'{ls[u]}-{chr(u+ord("a"))}', ls)) + "]" | |
def show_graph_it(graph): | |
for v in graph: | |
yield f'{chr(v+ord("a"))}: {show_graph_entry(graph[v])}' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env python3 | |
# it's like `.. | grep 'pattern\|'`, but with more colors ! | |
# it can be useful when viewing log files when piped with `less -R` | |
import sys | |
import re | |
# colors :: [(attribute, foreground, background)] | |
# list of color scheme for pattern, matched against n'th regex. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Probability and Statistical Inference 9th *) | |
(* Exercise 5.4.13 *) | |
(* h1 == f *) | |
h1[x_] := (x+1)/6 | |
(* adopted result of excercise 5.4.9. *) | |
lift[f_, n_] := Sum[f[x] f[#1-x], {x, Max[#1-n, 0], Min[n, #1]}] & | |
(* a,b) h2 == W1 == W2 *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env python3.6 | |
# https://stackoverflow.com/a/8748146 | |
_ = lambda x: x | |
# =================== | |
# flow | |
# =================== | |
def hmm(): |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <vector> | |
#include <iostream> | |
#include <cassert> | |
using namespace std; | |
class Perm { | |
vector<int> as; | |
int now = -1; | |
Perm* p = NULL; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# code for calculating solution for exercise no.38 of setion 1.2 from the book Discrete Mathematics and Its Applications 7th ed. | |
# no input, no configuring required. it just calculates & prints answer. | |
# it uses brute force approch. no sophisticated algorithm implemented with this code. | |
# further modification would enable argumented problem solving. | |
# Q: zebra | |
# Q: mineral | |
# The Englishman lives in the red house. | |
# The Spaniard owns a dog. | |
# The Japanese man is a painter. |
NewerOlder