Earn extra honor and gain new allies!
Honor is earned for each new codewarrior who joins.
Learn more
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;
};