Earn extra honor and gain new allies!
Honor is earned for each new codewarrior who joins.
Learn more
import analysis.special_functions.trigonometric

#check complex.continuous_cos

Large factorials with Num.

Fixpoint factorial (n : nat) :=
  match n with
  | O => 1
  | S n' => n * factorial n'
  end.
Code
Diff
  • dividedByThree=n=> (n * -1431655765 + 715827882 >>> 0) < 1431655765;
  • 1
    // i assume this is an allowed use of "/" :)
    
    2
    dividedByThree=n=>/^-?0*(0*1(01*0)*1)*0*$/.test(n.toString(2))
    
    1+
    dividedByThree=n=> (n * -1431655765 + 715827882 >>> 0) < 1431655765;
    
Advanced Language Features
Fundamentals
Theorem Proving

interleave using Equations.

Code
Diff
  • From Coq Require Import Lists.List omega.Omega.
    Import ListNotations.
    
    From Equations Require Import Equations.
    
    Equations interleave {A} (l1 l2 : list A) : list A by wf (length (l1 ++ l2)) lt :=
    interleave [] l2 := l2;
    interleave (x :: xs) l2 := x :: interleave l2 xs.
    Next Obligation. rewrite !app_length; omega. Qed.
    
    Example test_interleave1:
      interleave [1;2;3] [4;5;6] = [1;4;2;5;3;6].
    Proof. reflexivity. Qed.
    Example test_interleave2:
      interleave [1] [4;5;6] = [1;4;5;6].
    Proof. reflexivity. Qed.
    Example test_interleave3:
      interleave [1;2;3] [4] = [1;4;2;3].
    Proof. reflexivity. Qed.
    Example test_interleave4:
      interleave [] [20;30] = [20;30].
    Proof. reflexivity. Qed.
  • 11
    From Coq Require Import Lists.List omega.Omega.
    
    22
    Import ListNotations.
    
    33
    4
    Fail Fixpoint interleave {A} (l1 l2 : list A) : list A :=
    
    5
      match l1 with
    
    6
      | [] => l2
    
    7
      | x :: xs => x :: interleave l2 xs
    
    8
      end.
    
    4+
    From Equations Require Import Equations.
    
    99
    10
    Require Import Recdef.
    
    11
    12
    Fail Function interleave {A} (l1 l2 : list A) {measure length (l1 ++ l2)} : list A :=
    
    13
      match l1 with
    
    14
      | [] => l2
    
    6+
    Equations interleave {A} (l1 l2 : list A) : list A by wf (length (l1 ++ l2)) lt :=
    
    7+
    interleave [] l2 := l2;
    
    8+
    interleave (x :: xs) l2 := x :: interleave l2 xs.
    
    9+
    Next Obligation. rewrite !app_length; omega. Qed.
    
Code
Diff
  • open Preloaded;
    
    let fib = (n) => {
      let rec fib_aux = (n, a, b) =>
        if (n <= 0) { a; }
        else { fib_aux(n - 1, b, a +@ b); }
      fib_aux(n, big_int_of_int(0), big_int_of_int(1))
        |> string_of_big_int;
    };
    
    let fib64 = (n) => {
      // Open Int64 locally
      open Int64;
      let rec fib_aux = (n, a, b) =>
        if (n <= 0) { a; }
        else { fib_aux(n - 1, b, add(a, b)); }
      fib_aux(n, zero, one)
        |> to_string;
    };
    
  • 11
    open Preloaded;
    
    22
    33
    let fib = (n) => {
    
    44
      let rec fib_aux = (n, a, b) =>
    
    55
        if (n <= 0) { a; }
    
    66
        else { fib_aux(n - 1, b, a +@ b); }
    
    77
      fib_aux(n, big_int_of_int(0), big_int_of_int(1))
    
    88
        |> string_of_big_int;
    
    99
    };
    
    1010
    11+
    let fib64 = (n) => {
    
    12+
      // Open Int64 locally
    
    13+
      open Int64;
    
    14+
      let rec fib_aux = (n, a, b) =>
    
    15+
        if (n <= 0) { a; }
    
    16+
        else { fib_aux(n - 1, b, add(a, b)); }
    
    17+
      fib_aux(n, zero, one)
    
    18+
        |> to_string;
    
    19+
    };
    
open Preloaded;

let fib = (n) => {
  let rec fib_aux = (n, a, b) =>
    if (n <= 0) { a; }
    else { fib_aux(n - 1, b, a +@ b); }
  fib_aux(n, big_int_of_int(0), big_int_of_int(1))
    |> string_of_big_int;
};