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