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
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. Definition access : forall (m : nat) (l : list Z), m < length l -> Z. induction m as [ | m IHm]. intros [ | z tl]. SearchPattern (~_ < 0). 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 dyn_safe_access : forall m:nat, nat -> array m -> Z. intros m n [l len]; case_eq (leb m n). intros _; exact 0%Z. intros h; apply (access n l). rewrite len; apply leb_complete_conv; exact h. Qed. Module new_name_space. Program Fixpoint access' (n : nat) (l:list Z) : n < length l -> Z := match n with 0 => match l with nil => _ | z::tl => fun _ => z end | S p => match l with nil => _ | z::tl => fun _ => access' p tl _ end end. Next Obligation. case (lt_n_O 0); assumption. Qed. Next Obligation. case (lt_n_O (S p)); assumption. Qed. Next Obligation. omega. Qed. End new_name_space. 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. Lemma min_lt : forall n m, S n - m = 0 -> n < m. intros; omega. Qed. Notation "[< x -- y ]" := (cb x y (min_lt y x (refl_equal _))). Notation "[[ l ]]" := (ca _ l (refl_equal _)). Eval vm_compute in safe_access 5 [< 5 -- 3 ] [[ (10::11::12::13::14::nil)%Z ]].