davidad

import pandas as pd

# Load the Supplementary Data S1 from the lead poisoning PNAS paper
# https://www.pnas.org/doi/full/10.1073/pnas.2118631119
df = pd.read_excel('pnas.2118631119.sd01.xlsx')

# Load the Supplementary Data S1 from the ADDM/CDDS paper
# https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6223814/
file_path_s1 = 'autism_S1.xls'
autism_s1 = pd.read_excel(file_path_s1)

davidad

import pandas as pd

# Load the data
df = pd.read_excel('pnas.2118631119.sd01.xlsx')

from bs4 import BeautifulSoup

# Load the HTML file
with open('crime.html', 'r') as f:
    contents = f.read()

davidad

import pandas as pd

# Load the data
df = pd.read_excel('pnas.2118631119.sd01.xlsx')

import matplotlib.pyplot as plt

# Filter the data for ages 22-35
df_filtered = df[(df['AGE'] >= 22) & (df['AGE'] <= 35) & (df['YEAR'] >= 1955) & (df['YEAR'] <= 2040)]

davidad

Parameter set : Set.
Parameter In : (set * set) -> Prop.

Definition subset (A B : set) : Prop :=
  forall x : set, In(x,A) -> In(x,B).

Axiom ZF_extensionality :
  forall X Y : set,
    (forall z : set, In(z,X) <-> In(z,Y))
    -> X = Y.

davidad

#![feature(test)]

mod expr_adt {
    pub enum Expr {
        Var(String),
        Const(f64),
        Plus(Box<Expr>, Box<Expr>),
        Times(Box<Expr>, Box<Expr>),
    }
    pub fn gen_evaluator<'a, F : 'a + Fn(&str) -> f64> (env: F) -> Box<dyn 'a + Fn(&Expr) -> f64> {

davidad

Require Import Coq.Lists.List Coq.Relations.Relations Coq.Sorting.Sorted.
Require Import Coq.Program.Equality Psatz.

Lemma Sorted_iff_by_explicit_indices {A} {R: relation A} (l: list A):
  Sorted R l <-> forall n, (S n) < length l -> exists d,
    R (nth n l d) (nth (S n) l d).
Proof with (cbn in *; firstorder).
  split; induction l; intros.
  - unshelve esplit; contradict H0...
  - unshelve esplit; intuition; inversion H.

davidad

Require Import Coq.Lists.List Coq.Logic.Eqdep.
Definition vec (A: Type) (n: nat) : Type := {l: list A | length l = n}.

Section vec_rev.
  Variable A : Type.
  Variable n : nat.

  Definition vec_rev (l: vec A n): vec A n.
  Proof.
    refine (exist _ (rev (proj1_sig l)) _).

davidad

Require Import Arith Decidable Euclid Psatz Wf_nat.

Definition divides a b := exists k, b = k * a.
Definition prime p := 2 <= p /\ forall k, divides k p -> (k = 1 \/ k = p).

Lemma dec_divides k n: decidable (divides k n).
Proof with intuition.
  case (le_gt_dec k 0)...
  - case (le_gt_dec n 0).
    + left; exists 0...

davidad

#include <stdlib.h>
#include <stdio.h>

extern unsigned long fib(unsigned long);

int main(int argc, char* argv[]) {
  if(argc<2) printf("usage: fib_test <integer>\n"), exit(1);
  unsigned long input = strtoul(argv[1],NULL,10); // string to unsigned long
  printf("fib(%lu) = %lu\n",input,fib(input));
  return 0;

davidad

global fib
global _fib
fib:
_fib:
  cmp rdi, 1    ; set flags according to value of rdi minus one, i.e., relationship of rdi to 1
  jle return_one; if the relationship is "less than or equal", goto return_one
  dec rdi       ; rdi = rdi - 1
  push rdi      ;  ^ this guy is going to decrement it again, save "n-1" on the stack
  call fib      ; do call
  pop rdi       ; restore "n-1" to rdi