(* We re-use the dependent types of bounded integers as given in the course. *) Require Import Arith List. Set Implicit Arguments. Definition bnat (n : nat) : Type := { m : nat | m < n }. (* Q1. Implement the following function that inject (if possible) a nat into a bnat. If the nat is too big, you could return a bnat containing 0. Hint: use the boolean function leb on natural numbers and its companion theorems. *) Definition mkbound : forall m, 0 < m -> nat -> bnat m. Proof. (* When you are finished, replace Admitted by Defined rather than Qed. *) Admitted. (* Q2, prove that if you have an element in bnat m, then 0 < m. *) Lemma bound_non_0 : forall m, bnat m -> 0 < m. Admitted. (* Q3, Define a function that increments a bounded natural number and returns a bounded natural number (with the same bound), falling back on 0 if the bound is reached. This uses the answers of the previous two questions. incr_bound : forall m, bnat m -> bnat m *) (* Q4. Define a function that takes as input m, m', a proof that m < m', a bounded number smaller than m, and returns a number smaller than m' extend_bound : forall m m':nat, m < m' -> bnat m -> bnat m' *) (* Q5. Implement the following function. Feel free to try several approaches. *) Definition is_prefix_of A (u v : list A) := exists w, u ++ w = v. Definition firstn : forall A (l:list A) n, n <= length l -> { l' | n = length l' /\ is_prefix_of l' l }. Proof. Admitted. (* Implementation of finite sets of integers. We would like to precisely implement the following interface for sets of integers *) Require Import ZArith. Open Scope Z_scope. Parameter set : Type. Parameter In : Z -> set -> Prop. Parameter mem : forall x s, { In x s }+{ ~ In x s }. Parameter add : forall x s, { s' | forall y, In y s' <-> x=y \/ In y s }. (* Q6. Propose an naive implementation with set := list Z *) (* We propose the following way of stating that a list is sorted *) Inductive sorted : list Z -> Prop := | sorted_0 : sorted nil | sorted_1 : forall a, sorted (a::nil) | sorted_2 : forall a b l, a <= b -> sorted (b::l) -> sorted (a::b::l). Hint Constructors sorted. (* The following properties might help. Proving then is not a priority here, but you can try later (at the end of the session). *) Lemma sorted_inv : forall l a, sorted (a::l) -> sorted l. Admitted. Lemma sorted_cons : forall l x, sorted l -> (forall y, List.In y l -> x<=y) -> sorted (x::l). Admitted. Lemma in_above : forall l a x, sorted (a::l) -> List.In x l -> a<=x. Admitted. (* Q7. Implement more clever functions for set := { l : list Z | sorted l } *) (* Q8. Try the Extraction command on the functions implemented during this session *)