Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* 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. *)