Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Interval Lists

Resources

Download Files

Definitions File

theory Defs
  imports "HOL-Library.Extended_Nat"
begin


datatype interval = I nat enat ("[_,_')")
type_synonym intervals = "interval list"


fun set_of_i :: "interval \<Rightarrow> nat set" where
"set_of_i [l,\<infinity>) = {l..}" |
"set_of_i [l,h) = {l..<h}"

definition set_of :: "intervals \<Rightarrow> nat set" where
  "set_of ins = fold (\<union>) (map set_of_i ins) {}"


fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
"inv' k [] \<longleftrightarrow> True" |
"inv' k [[l,\<infinity>)] \<longleftrightarrow> k\<le>l" |
"inv' k ([l,r)#ins) \<longleftrightarrow> k\<le>l \<and> l<r \<and> inv' (Suc r) ins" |
"inv' _ _ \<longleftrightarrow> False"

definition inv where "inv = inv' 0"

end

Template File

theory Submission
  imports Defs
begin

definition compl :: "intervals \<Rightarrow> intervals" where
  "compl x = undefined"

theorem compl_inv:
  assumes "inv ins"
  shows "inv (compl ins)"
    and "set_of (compl ins) = -set_of ins"
  sorry

theorem compl_set_of:
  assumes "inv ins"
  shows "set_of (compl ins) = -set_of ins"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem compl_inv:
  assumes "inv ins"
  shows "inv (compl ins)"
  using assms by (rule Submission.compl_inv)

theorem compl_set_of:
  assumes "inv ins"
  shows "set_of (compl ins) = -set_of ins"
  using assms by (rule Submission.compl_set_of)

end
Download Files

Definitions File

import data.set.intervals
import tactic

/-! Set operations on interval lists -/
open set

/-!
Consider the following definition of interval lists
`interval n m` represents `[n,m)` (`Ico n m`):
-/

@[reducible]
def Interval := ℕ × with_top ℕ

@[reducible]
def Intervals := list Interval

@[simp]
def set_of_i : Interval → set ℕ
| (l, ⊤) := Ici l
| (l, some r) := Ico l r

def set_of_is (is : Intervals) : set ℕ :=
is.foldr (λ i s, set_of_i i ∪ s) ∅

/-!
As an invariant, every interval should be non-empty, and the list of intervals should be
ordered and of minimal length.
-/
@[simp]
def invariant' : ℕ → Intervals → Prop
| k []                := true
| k [(l, ⊤)]          := k ≤ l
| k ((l, some r)::is) := k ≤ l ∧ l < r ∧ invariant' (r + 1) is
| k ((l, ⊤)::_::_)    := false

@[simp]
def invariant : Intervals → Prop := invariant' 0

Template File

import .defs

/-!
Define complement and intersection operations for interval lists, and prove them correct!
-/
def complement : Intervals → Intervals :=
sorry

theorem invariant_complement {is : Intervals} (h : invariant is) :
  invariant (complement is) :=
sorry

theorem set_of_is_complement {is : Intervals} (h : invariant is) :
  set_of_is (complement is) = (set_of_is is)ᶜ :=
sorry

Check File

import .submission

theorem compl_test:
  complement [(3, some 6), (9, ⊤)] = [(0, some 3), (6, some 9)] ∧
  complement [(0, some 1), (4, some 8)] = [(1, some 4), (8, ⊤)] ∧
  complement [(0, ⊤)] = [] ∧
  complement [] = [(0, ⊤)] ∧
  complement [(0, some 1), (4, some 8), (10, some 11), (12, ⊤)] =
    [(1, some 4), (8, some 10), (11, some 12)] :=
⟨rfl, rfl, rfl, rfl, rfl⟩


theorem invariant_complement_check1: ∀ {is : Intervals} (h : invariant is),
  invariant (complement is) :=
@invariant_complement

theorem invariant_complement_check2: ∀ {is : Intervals} (h : invariant is),
  invariant (complement is) :=
@invariant_complement

theorem invariant_complement_check3: ∀ {is : Intervals} (h : invariant is),
  invariant (complement is) :=
@invariant_complement

theorem set_of_is_complement_check1: ∀ {is : Intervals} (h : invariant is),
  set_of_is (complement is) = (set_of_is is)ᶜ :=
@set_of_is_complement

theorem set_of_is_complement_check2: ∀ {is : Intervals} (h : invariant is),
  set_of_is (complement is) = (set_of_is is)ᶜ :=
@set_of_is_complement

theorem set_of_is_complement_check3: ∀ {is : Intervals} (h : invariant is),
  set_of_is (complement is) = (set_of_is is)ᶜ :=
@set_of_is_complement

theorem set_of_is_complement_check4: ∀ {is : Intervals} (h : invariant is),
  set_of_is (complement is) = (set_of_is is)ᶜ :=
@set_of_is_complement

theorem set_of_is_complement_check5: ∀ {is : Intervals} (h : invariant is),
  set_of_is (complement is) = (set_of_is is)ᶜ :=
@set_of_is_complement

theorem set_of_is_complement_check6: ∀ {is : Intervals} (h : invariant is),
  set_of_is (complement is) = (set_of_is is)ᶜ :=
@set_of_is_complement
Download Files

Definitions File

From Coq Require Export List Bool.
Export ListNotations.

Set Implicit Arguments.

Structure interval := I {imin : nat; imax : option nat}.

Notation "[ l , r )" := (I l (Some r)) (at level 0).
Notation "[ l , '+oo' )" := (I l None) (at level 0).

Definition intervals := list interval.

(* The standard library does not do a very good job here, e.g. using
   Ensembles is not automation friendly.
   So, here is a very small set library.
   A set is represented as a predicate `A -> Prop` over a type A. *)
Section Sets.
Variable A : Type.

Definition set := A -> Prop.

Implicit Types S T : set.

Definition in_set x S : Prop := (S x).
Definition empty_set : set := fun _ : A => False.
Definition set_union S T : set := fun x => S x \/ T x.
Definition set_inter S T : set := fun x => S x /\ T x.
Definition set_diff S T : set := fun x => S x /\ ~ T x.
Definition set_compl S : set := fun x => ~ S x.
Definition subset_eq S T : Prop := forall x, in_set x S -> in_set x T.
End Sets.

Notation "x ∈ S" := (in_set x S) (at level 60, no associativity).
Notation "∅" := (@empty_set _) (at level 0, no associativity).
Notation "S ⊆ T" := (subset_eq S T) (at level 55, left associativity).
Notation "S ≡ T" := (forall x, in_set x S <-> in_set x T) (at level 58, no associativity).
Notation "S ∪ T" := (set_union S T) (at level 55, left associativity).
Notation "S ∩ T" := (set_inter S T) (at level 50, left associativity).
Notation "S \ T" := (set_diff S T) (at level 55, left associativity).
Notation "∁ S" := (set_compl S) (at level 0, no associativity).
#[export] Hint Unfold in_set empty_set set_union set_inter set_compl set_diff : core.

Notation " '{' l '..}' " := (fun n => l <= n) (at level 0, no associativity).
(* sets *)


(* This is how we map an interval to a set of natural numbers *)
Definition set_of_i (i : interval) : set nat :=
  match i with
  | [l, r) => fun n => l <= n /\ n < r
  | [l, +oo) => {l ..}
  end.

Definition set_of (is1 : intervals) : set nat :=
  fold_right (fun i acc => (set_of_i i) ∪ acc) ∅ is1.

(*
As an invariant, every interval should be non-empty, and the list of
intervals should be ordered and of minimal length.
 *)

Fixpoint inv' (k: nat) (is1 : intervals) : Prop :=
  match is1 with
  | [] => True
  | [ [l, +oo) ] => k <= l
  | [l, r) :: is1 =>
       (k <= l) /\ (l < r) /\ inv' (r + 1) is1
  | _ => False
  end.

Definition inv : intervals -> Prop := inv' 0.

Template File

Require Import Defs.

(*
Define complement and intersection operations for interval lists, and prove them correct!
*)

(* complement *)
Definition compl (ins : intervals) : intervals.
Admitted.

Theorem invariant_complement ins :
  inv ins ->
  inv (compl ins).
Proof.
Admitted.

Theorem set_of_is_complement ins :
  inv ins ->
  set_of (compl ins) ≡ ∁ (set_of ins).
Proof.
Admitted.

Terms and Conditions