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. Definition bnat n := { m | m < n }. Definition array n := { l : list Z | length l = n }. (* successor on bnat, extending the bound. *) Definition succ_bnat n : bnat n -> bnat (S n) := fun m => let (x,p) := m in exist _ (S x) (lt_n_S _ _ p). Definition succ_bnat' n : bnat n -> bnat (S n). Proof. intros n m. destruct m as [x p]. exists (S x). auto with arith. Defined. Program Definition succ_bnat'' n : bnat n -> bnat (S n) := fun m => S m. Next Obligation. destruct m. simpl. auto with arith. Qed. (* successor on bnat, version with overflow to 0 *) Definition succ_bnat_mod n (m : bnat n) : bnat n. Proof. intros n m. destruct m as [m Hm]. case_eq (beq_nat n (S m)). exists 0. omega. exists (S m). apply beq_nat_false in H. omega. Defined. Program Definition succ_bnat_mod_prog n (m : bnat n) : bnat n := match beq_nat n (S m) with true => 0 | false => S m end. Next Obligation. destruct m; omega. Qed. Next Obligation. rename Heq_anonymous into H. destruct m as [m Hm]; simpl in *. symmetry in H; apply beq_nat_false in H. omega. Qed. (** Example of program with sumbool *) Definition le_lt_dec : forall n m : nat, { n<=m }+{ m < n }. Proof. induction n. left. auto with arith. destruct m. right. auto with arith. destruct (IHn m); [left | right]; auto with arith. Qed. (** Example of "programming" a proof *) Definition or_sym A B : A\/B -> B\/A := fun h => match h with | or_introl a => or_intror _ a | or_intror b => or_introl _ b end. (* Definition nat_of_or A B : A\/B -> nat := fun h => match h with | or_introl _ => 0 | or_intror _ => 1 end. proofs can be eliminated only to build proofs. *) (** Experiments for building a division for nat without general recursion *) Require Import Arith Omega. Ltac mysolver := simpl in *; omega. Definition DivSpec a b q := q*b <= a < (S q)*b. Fixpoint div a b := match a with | O => O | S a' => let q := div a' b in if leb ((S q)*b) a then S q else q end. Lemma div_ok : forall a b, 0 < b -> DivSpec a b (div a b). Proof. intros a b Hb. unfold DivSpec. induction a; intros. mysolver. simpl. case_eq (leb (b + (div a b) * b) (S a)); intros EQ. rewrite leb_iff in EQ. mysolver. rewrite leb_iff_conv in EQ. mysolver. Qed. Inductive reflect (P:Prop) : bool -> Prop := | reflect_true : P -> reflect P true | reflect_false : ~P -> reflect P false. Lemma reflect_iff : forall P b, (P<->b=true) <-> reflect P b. Proof. split. intros IFF. destruct b; constructor; rewrite IFF; auto. intros REF. destruct REF; intuition; discriminate. Qed. Lemma leb_reflect : forall n m, reflect (n<=m) (leb n m). Proof. intros. rewrite <- reflect_iff, leb_iff. intuition. Qed. Lemma div_ok' : forall a b, 0 < b -> DivSpec a b (div a b). Proof. intros a b Hb. unfold DivSpec. induction a; intros. mysolver. simpl. case leb_reflect; intros LE. mysolver. mysolver. Qed. Fixpoint div' a b := match a with | O => O | S a' => let q := div' a' b in if le_lt_dec ((S q)*b) a then S q else q end. Lemma div'_ok : forall a b, 0 < b -> DivSpec a b (div' a b). Proof. intros a b Hb. unfold DivSpec. induction a; intros. mysolver. simpl. destruct le_lt_dec. mysolver. mysolver. Qed. Definition div_rich : forall a b, 0 < b -> { q | DivSpec a b q }. Proof. intros a b Hb. unfold DivSpec. induction a. exists 0. mysolver. destruct IHa as [q Hq]. destruct (le_lt_dec ((S q)*b) (S a)). exists (S q). mysolver. exists q. mysolver. Defined. (* We can compute in Coq, but this isn't obvious *) Check lt_O_Sn. (* For precondition *) (* Eval compute in div_rich 50 7 (lt_O_Sn 6). No! would build a huge expression as postcondition *) Eval vm_compute in let (q,_) := div_rich 50 7 (lt_O_Sn 6) in q. (* Btw, a clever but structural div (we embed an internal minus): *) Fixpoint div_aux a b q r := match a with | O => q | S a' => match r with | O => div_aux a' b (S q) (pred b) | S r' => div_aux a' b q r' end end. Definition div_alt a b := div_aux a b O (pred b). Lemma div_aux_ok : forall a b q r, r let q' := div_aux a b q r in let r' := b - S r in q'*b <= a + q*b + r' < (S q')*b. Proof. induction a. intros. simpl in *. subst q'. subst r'. omega. intros. simpl in *. destruct r. assert (Pr : pred b < b) by omega. specialize (IHa b (S q) (pred b) Pr). subst q' r'. simpl in *. omega. specialize (IHa b q r). subst q' r'. omega. Qed. Lemma div_alt_ok : forall a b, 0 (div_alt a b)*b <= a < (S (div_alt a b))*b. Proof. intros. unfold div_alt. assert (Pr : pred b < b) by omega. assert (Aux:=div_aux_ok a b 0 (pred b) Pr). simpl in Aux. simpl. omega. Qed. (** In some situation, minus preserves being structurally smaller *) Fixpoint div_encore a b := match a with | O => O | S a' => (* a'-pred b is equivalent a-b (as long as b<>0), but unlike (a-b) Coq accepts it as structurally smaller than a *) if leb b a then S (div_encore (a'-pred b) b) else 0 end. Definition div_encore' : forall a b, 0 < b -> { q | DivSpec a b q }. Proof. fix 1. unfold DivSpec in *. destruct a as [ |a']. exists 0. mysolver. intros b Hb. destruct (le_lt_dec b (S a')). destruct (div_encore' (a'-(pred b)) b Hb) as (q,Hq). exists (S q). mysolver. exists 0. mysolver. Defined. (** We could even avoid the comparison [leb] or [le_lt_dec] But the function we obtain out-of-the-box needs some tweaking. *) Fixpoint div_toujours a b := match a with | O => O | S a' => S (div_toujours (a'-b) b) end. Definition div_adapt a b := match b with | O => O (* or False_rect in a rich version *) | S b' => pred (div_toujours (S a) b') end. (** A similar div+mod function, and correctness proofs *) Fixpoint diveucl a b := match a with | O => (O,O) | S a' => let a'' := a'-b in match a'' with | O => (1,a') | _ => let (q,r) := diveucl a'' b in (S q,r) end end. Functional Scheme diveucl_ind := Induction for diveucl Sort Prop. Lemma diveucl_pos : forall a b, 0 < a -> let (q,r) := diveucl a b in 0 < q. Proof. intros a b. functional induction diveucl a b; auto with *. Qed. Lemma diveucl_mod_bound : forall a b, let (q,r) := diveucl a b in r <= b. Proof. intros a b. functional induction diveucl a b. auto with *. omega. rewrite e1 in *. auto. Qed. Lemma diveucl_ok : forall a b, let (q,r) := diveucl a b in pred a = (pred q) * (S b) + r. Proof. intros a b. functional induction diveucl a b. auto. auto. simpl. assert (POS := diveucl_pos (a'-b) b). rewrite e1 in *. rewrite (S_pred q 0). simpl. omega. omega. Qed. Definition diveucl_full a b := match b with | O => (O,a) | S b' => let (q,r) := diveucl (S a) b' in (pred q, r) end. Lemma diveucl_full_ok : forall a b, let (q,r) := diveucl_full a b in a = q*b + r. Proof. intros. destruct b. simpl. auto. unfold diveucl_full. generalize (diveucl_ok (S a) b); destruct (diveucl (S a) b) as [q r]. auto. Qed. Lemma diveucl_full_mod_bound : forall a b, 0 < b -> let (q,r) := diveucl_full a b in r < b. Proof. intros. destruct b. inversion H. unfold diveucl_full. generalize (diveucl_mod_bound (S a) b); destruct diveucl as [q r]. auto with *. Qed. Lemma diveucl_div_toujours : forall a b, let (q,_) := diveucl a b in q = div_toujours a b. Proof. intros a b. functional induction diveucl a b. simpl. auto. simpl. rewrite e0; auto. simpl. f_equal. rewrite e1 in *. auto. Qed. Lemma div_toujours_ok : forall a b, (pred (div_toujours a b)) * (S b) <= pred a < (S (pred (div_toujours a b))) * (S b). Proof. intros a b. apply (div_ind (fun a b q => (pred q) * (S b) <= pred a < (S (pred q)) * (S b))). intros. simpl. omega. intros. simpl in *. Admitted. Lemma div_adapt_ok : forall a b, 0 < b -> (div_adapt a b) * b <= a < (S (div_adapt a b)) * b. Proof. intros. destruct b. inversion H. unfold div_adapt. change a with (pred (S a)) at 2 3. apply div_toujours_ok. Qed. Eval vm_compute in div_toujours 10 1.