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 (m : nat) : Type := cb : forall n, n < m -> bnat m. 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 their companion theorems. *) SearchAbout leb. Definition mkbound : forall m, 0 < m -> nat -> bnat m. intros m hm n. case_eq (leb m n). intros _; apply (cb m 0). assumption. intros tst; apply (cb m n). apply leb_complete_conv. assumption. Defined. Lemma p0lt256 : 0 < 256. omega. Qed. Eval vm_compute in mkbound 256 p0lt256 500. (* Q2, prove that if you have an element in bnat m, then 0 < m. *) Lemma bound_non_0 : forall m, bnat m -> 0 < m. intros m n; destruct n as [n nm]; omega. Qed. (* 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. *) Definition incr_bound : forall m, bnat m -> bnat m := fun m n => match n with cb n' n'm => mkbound m (bound_non_0 m n) (S n') end. (* Q4. Define a function that takes as input m, m', a proof that m < m', a bounded number smaller than m, and returns a smaller number smaller than m' *) Definition extend_bound (m m':nat) : m < m' -> bnat m -> bnat m' := fun h n => match n with cb n h' => cb m' n (lt_trans _ _ _ h' h) end. (* 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') *) Definition mult_bound : forall m m':nat, bnat m -> bnat m' -> bnat (m * m'). intros m m' [v1 pv1] [v2 pv2]. destruct v2 as [ | v2']. exists 0. destruct m. case (lt_n_O v1); assumption. destruct m'. case (lt_n_O 0); assumption. simpl. apply lt_O_Sn. exists (v1 * S v2'). apply lt_trans with (m * S v2'). apply mult_lt_compat_r. assumption. apply lt_O_Sn. repeat rewrite (mult_comm m). apply mult_lt_compat_r. assumption. apply bound_non_0. exact (cb m v1 pv1). Qed. (* 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. *) Search lt. Fixpoint update (l : list Z) : forall n, Z -> n < length l -> list Z := match l return forall n, Z -> n < length l -> list Z with nil => fun n v (h : n < 0) => False_rect (list Z) (lt_n_O _ h) | z::tl => fun n v => match n return n < length (z::tl) -> list Z with 0%nat => fun _ => v::tl | S n' => fun h => z::update tl n' v (lt_S_n _ _ h) end end. Lemma update_length : forall l n v h, length (update l n v h) = length l. induction l. simpl. intros n v h; case (lt_n_O n). assumption. intros [ | n'] v; simpl. intros _; reflexivity. intros h; rewrite IHl; reflexivity. Defined. Definition safe_update : forall m, array m -> bnat m -> Z -> array m. intros m [l len] [i pi] v. assert (tmp: i < length l). rewrite len; assumption. apply (ca m (update l i v tmp)). rewrite update_length. assumption. Defined. (* 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. *) Fixpoint incr_list (l:list Z) : list Z := match l with nil => nil | a::tl => (a+1)%Z::incr_list tl end. Lemma incr_list_length : forall l, length (incr_list l) = length l. induction l; simpl; auto. Qed. Lemma th : forall m l, length l = m -> length (incr_list l) = m. intros; transitivity (length l); try assumption. apply incr_list_length. Qed. Definition incr_all' m (a : array m) := let (l, pl) := a in ca m (incr_list l) (th _ _ pl). Eval lazy in let (l, _) := (incr_all' _ (ca _ (0::1::2::nil)%Z (refl_equal _))) in l. Require Import Sumbool. Program Definition mkbound' (m :nat) (hm : 0 < m) (n : nat) := if sumbool_of_bool (leb m n) then cb m 0 hm else cb m n _. Next Obligation. apply leb_complete_conv; assumption. Defined. Definition incr_all (m : nat) (a : array m) : array m := loop (array m) m (fun i a' => safe_update m a' i (safe_access m i a' + 1)) a. Lemma p2lt3 : 2 < 3. auto with arith. Qed. Open Scope Z_scope. Check (ca 3 (0::1::2::nil)%Z (refl_equal _)). Check (cb 3 2 p2lt3). Eval lazy in (safe_access _ (cb 3 2 p2lt3) (ca 3 (0::1::2::nil)%Z (refl_equal _))). Eval lazy in loop (list nat) 3 (fun i l => let (v, _) := i in v::l) nil. Eval lazy in incr_all 3 (ca 3 (0::1::2::nil)%Z (refl_equal _)).