(* We re-use the dependent types of bounded integers as given in the course. *)
Require Import List ZArith.
Inductive bnat (n : nat) : Type :=
cb : forall m, m < n -> bnat n.
Inductive array (n : nat) : Type :=
ca : forall l : list Z, length l = n -> array n.
(* Q1. try to write a function that compares n with m, returns
cb n m if n < m and cb 0 m otherwise. What condition is there
on m? Hint: use the boolean function leb on natural numbers and its
companion theorems. *)
Definition mkbound : forall m, 0 < m -> nat -> bnat m.
(* When you are finished, use the keyword Defined instead of 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. Define a function that takes as inputs two bounded numbers
and returns their product, as a number bounded by the product of the
bounds:
mult_bound : forall m m':nat, bnat m -> bnat m' -> bnat (m * m')
*)
(* Now, here is a model of a loop program, with an index variable
that is decremented at each call, starting at m-1, stopping at 0.
The index is obviously bounded by m, so we can represent the body
of the function, where the index can be used, with a function of
type (bnat m -> A -> A) *)
Fixpoint loop (A : Type) (m : nat) : (bnat m -> A -> A) -> A -> A :=
match m return (bnat m -> A -> A) -> A -> A with
0 => fun _ a => a
| S m' =>
fun f a => f (cb (S m') m' (lt_n_Sn m'))
(loop A m' (fun (i : bnat m') a' =>
f (extend_bound m' (S m') (lt_n_Sn m') i) a') a)
end.
(* Here is a model of safe, statically verified, array access. *)
Definition access : forall (m : nat) (l : list Z), m < length l -> Z.
induction m as [ | m IHm].
intros [ | z tl].
intros h; case (lt_n_O _ h).
intros _; exact z.
intros [ | z tl] h.
case (lt_n_O _ h).
apply (IHm tl).
simpl in h.
omega.
Defined.
Definition safe_access : forall m, bnat m -> array m -> Z.
intros m [n h] [l len].
apply (access n l).
rewrite len; exact h.
Defined.
(* Q6. Write a safe update access.
safe_update : forall m, array m -> bnat m -> Z -> array m.
*)
(* Q7. An advanced exercise is to use this loop model to describe a function
that access all elements in an array of integers and increments them. *)