larsr

""" Announcing and locating a service """

import socket
import atexit
import multiprocessing
import time
import pickle
import zeroconf

larsr

Require Import Arith.
Require Import Program.

Program Fixpoint sumn (n:nat) {measure n} :=
  if dec (n =? 0) then 0 else n + sumn (n-1).
Next Obligation.
  destruct n; simpl in H.
  congruence.
  auto with arith.
Defined.

larsr

# Lars.Rasmusson@gmail.com, 2019-01-12

from numpy import *

def gcd(n, m):
    n, m = min(n, m), max(n, m)
    while n != 0: n, m = m % n, n
    return m

def experiment(N):

larsr

(* 
   Coq proof of Hofstadter's MU puzzle (https://en.wikipedia.org/wiki/MU_puzzle) 
    
   To prove that "MU" cannot be generated, 
   show by induction on a valid string that the number of "I"
   is never a multiple of three.
   Then as a corollary we see that "MU" which has zero "I" cannot be
   a valid string. 

   Lars.Rasmusson@gmail.com, 2018-12-17

larsr

From Coquelicot Require Import Coquelicot.
Import Even.
Require Import Reals.
Require Import Psatz.
Import Complex.


Notation "x !" := (fact x) (at level 30). (* tighter than mul and div *)

Lemma is_series_cos x: is_series (fun i : nat => (-1) ^ i / INR ((2 * i) !) * x ^ (2*i)) (cos x).

larsr

(* Definition of exponential for complex numbers 
  Lars.Rasmusson@gmail.com, 2018-10-06
  *)

From Coquelicot Require Import Coquelicot.
Require Import Reals.
Require Import Psatz.
Import Complex.

larsr

# Viterbi algorithm
# See example at https://www.youtube.com/watch?v=dKIf6mQUfnY
# -- Lars.Rasmusson@gmail.com (2018-10-04)

import numpy as np

# Define the coder by its internal state transition and output
states = [(0,0), (0,1), (1,0), (1,1)]
def output(s, b): return (b^s[1], b^s[1]^s[0]) # xor binary values
def next_state(s, b): return b, s[0]

larsr

Variable P:nat->Prop.

Lemma nat_strong_induction (IH: forall n, (forall k, k<n -> P k) -> P n): forall n, P n.
  enough  (forall n k, k <= n -> P k) by eauto.
  induction n; intros; inversion H; eauto using le_S_n.
  apply IH; inversion 1.
Qed.

(* 

larsr

# RANSAC algorithm
# Lars.Rasmusson@sics.se, 2018-06-19

import numpy as np
import pylab as pl

# Create some random data, with many outliers

c, m = 5*np.random.randn(2)

larsr

From Coquelicot Require Import Coquelicot.
From mathcomp Require Import all_ssreflect.
Require Import Reals.

Definition RplusM: Monoid.law R0.
  apply (@Monoid.Law R R0 Rplus).
  now intros x y z; rewrite Rplus_assoc.
  now intros x; rewrite Rplus_0_l.
  now intros x; rewrite Rplus_0_r.
Defined.