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.

# [Proof Ground 2021] Interval Lists

In this exercise, we consider the data structure of *interval lists*. Interval lists represent sets of natural numbers by a union of intervals. For instance the list `[1,3), [5,6), [9,∞)` represents the set `1,2,5,9,10,11,...`. As an invariant, every interval should be non-empty, and the list of intervals should be ordered and of minimal length. Your task is to define a complement operation on interval lists and to prove it correct. You will get partial credit for: - a correct definition (10%) - proving that the invariant is preservered (30%) - proving that the result correctly represents the complement (60%)

## Resources

### 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```

### 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
```

### 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.

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