palmskog

Require Import List.
Import ListNotations.
Require Import Sumbool.

Ltac break_and :=
  repeat match goal with
           | [H : _ /\ _ |- _ ] => destruct H
         end.

Ltac break_if :=

palmskog

Require Import List.
Import ListNotations.
Require Import Sumbool.

Ltac break_let :=
  match goal with
    | [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:?
    | [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:?
  end.

palmskog

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Ltac break_match :=
  match goal with
    | [ |- context [ match ?X with _ => _ end ] ] =>
      match type of X with
        | sumbool _ _ => destruct X

palmskog

From mathcomp
Require Import all_ssreflect.

Section Barendregt.

Variable P : Prop.

Fixpoint B (n : nat) := match n with | 1 => P | n'.+1 => P <-> B n' | 0 => False end.

Lemma B2n: forall n, n >= 1 -> B (2 * n).

palmskog

 (VernacExpr()(VernacRequire()(false)(((v(Ident(Id List)))(loc(((fname(InFile Dedup_before.v))(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 15)(ep 19))))))))
 (VernacExpr()(VernacImport false(((v(Ident(Id ListNotations)))(loc(((fname(InFile Dedup_before.v))(line_nb 2)(bol_pos 21)(line_nb_last 2)(bol_pos_last 21)(bp 28)(ep 41))))))))
 (VernacExpr()(VernacBeginSection((v(Id dedup))(loc(((fname(InFile Dedup_before.v))(line_nb 4)(bol_pos 44)(line_nb_last 4)(bol_pos_last 44)(bp 52)(ep 57)))))))
 (VernacExpr()(VernacAssumption(DoDischarge Definitional)NoInline((false(((((v(Id A))(loc(((fname(InFile Dedup_before.v))(line_nb 5)(bol_pos 59)(line_nb_last 5)(bol_pos_last 59)(bp 70)(ep 71)))))()))((v(CSort(GType())))(loc(((fname(InFile Dedup_before.v))(line_nb 5)(bol_pos 59)(line_nb_last 5)(bol_pos_last 59)(bp 74)(ep 78))))))))))
 (VernacExpr()(VernacAssumption(DoDischarge Logical)NoInline((false(((((v(Id A_eq_dec))(loc(((fname(InFile Dedup_before.v))(line_nb 6)(bol_pos 80)(line_nb_last 6)(bol_pos_last 80)(bp

palmskog

Require Import List.
Import ListNotations.

Section dedup.
  Variable A : Type.
  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.

  Fixpoint dedup (xs : list A) : list A :=
    match xs with
    | [] => []

palmskog

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)



type 'char c = 'char

palmskog

module Util {

  datatype Option<T> = Some(v:T) | None

  function unionMap<U(!new), V>(m: map<U,V>, m': map<U,V>): map<U,V>
    requires m !! m'; // disjoint
    ensures forall i :: i in unionMap(m, m') <==> i in m || i in m';
    ensures forall i :: i in m ==> unionMap(m, m')[i] == m[i];
    ensures forall i :: i in m' ==> unionMap(m, m')[i] == m'[i];
  {

palmskog

module Collections {

  method ArrayCopy<T>(src:array<T>, srcIndex:int, dst:array<T>, dstIndex:int, len:int)
    modifies dst;
    requires src != dst;
    requires 0 <= len;
    requires 0 <= srcIndex && srcIndex + len <= src.Length;
    requires 0 <= dstIndex && dstIndex + len <= dst.Length;
    ensures forall k :: 0 <= k < dstIndex ==> dst[k] == old(dst[k]);
    ensures forall k :: dstIndex <= k < dstIndex + len ==> dst[k] == src[k - dstIndex + srcIndex];

palmskog

module Collections {

  method ArrayCopy<T>(src:array<T>, srcIndex:int, dst:array<T>, dstIndex:int, len:int)
    modifies dst;
    requires src != dst;
    requires 0 <= len;
    requires 0 <= srcIndex && srcIndex + len <= src.Length;
    requires 0 <= dstIndex && dstIndex + len <= dst.Length;
    ensures forall k :: 0 <= k < dstIndex ==> dst[k] == old(dst[k]);
    ensures forall k :: dstIndex <= k < dstIndex + len ==> dst[k] == src[k - dstIndex + srcIndex];