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 Arith Omega. (*Set Implicit Arguments.*) Definition is_prefix_of A (u v : list A) := exists w, u ++ w = v. (* Replace the following axiom by an implementation. Feel free to try several approaches. *) Parameter firstn : forall A (l:list A) n, n <= length l -> { l' | n = length l' /\ is_prefix_of _ l' l }. Fixpoint firstn_pure A (l:list A) n := match l with | nil => nil | x::l' => match n with | O => nil | S n' => x::firstn_pure _ l' n' end end. Lemma firstn_pure_ok : forall A (l:list A) n, n <= length l -> n = length (firstn_pure _ l n) /\ is_prefix_of _ (firstn_pure _ l n) l. Proof. induction l. simpl; intros. split. omega. exists nil; auto. destruct n; simpl. split. auto. exists (a::l); auto. intros. destruct (IHl n). omega. split. omega. destruct H1 as (suff,Hsuff). exists suff. simpl. f_equal; auto. Qed. Definition firstn_full : forall A (l:list A) n, n <= length l -> { l' | n = length l' /\ is_prefix_of _ l' l }. Proof. intros. exists (firstn_pure _ l n). apply firstn_pure_ok. assumption. Defined. Definition firstn_full2 : forall A (l:list A) n, n <= length l -> { l' | n = length l' /\ is_prefix_of _ l' l } := fun A l n H => exist _ (firstn_pure _ l n) (firstn_pure_ok _ l n H). Definition firstn_bytac : forall A (l:list A) n, n <= length l -> { l' | n = length l' /\ is_prefix_of _ l' l }. Proof. induction l. intros. exists nil. simpl in *; split. omega. exists nil; auto. destruct n; intros. exists nil. simpl in *; split. omega. exists (a::l); auto. destruct (IHl n) as [lrec [H1 H2]]. simpl in *; omega. exists (a::lrec). split. simpl in *; omega. destruct H2 as (suff,Hsuff). exists suff. simpl. f_equal; auto. Defined. Program Fixpoint firstn_byprogram A (l:list A) n (h: n <= length l) : { l' | n = length l' /\ is_prefix_of _ l' l } := match l with | nil => nil | x::l' => match n with | O => nil | S n' => x :: firstn_byprogram _ l' n' _ end end. Next Obligation. split. simpl in *; omega. exists nil; auto. Qed. Next Obligation. split. auto. exists (x::l'); auto. Qed. Next Obligation. simpl in *; omega. Qed. Next Obligation. destruct (firstn_byprogram A l' n') as [lrec [H1 H2]]; simpl. split. omega. destruct H2 as (suff,Hsuff). exists suff. simpl. f_equal; auto. Defined. Recursive Extraction firstn_full firstn_full2 firstn_bytac firstn_byprogram. (* All versions produce the same extracted code !! *) Require Import ZArith. Open Scope Z_scope. (* Implementation of finite sets. We would like to precisely implement the following interface for sets of integers *) Parameter set : Type. Parameter In : Z -> set -> Prop. Parameter mem : forall x s, { In x s }+{ ~ In x s }. Parameter add : forall x s, { s' | forall y, In y s' <-> y=x \/ In y s }. (* 1) Propose an naive implementation with set := list Z *) Module FirstVersion. (* To use the same names in different attempts *) Definition set : Type := list Z. Definition In (x:Z)(s:set) : Prop := List.In x s. Definition mem : forall x s, { In x s }+{ ~ In x s }. Proof. induction s. right. intro H. inversion H. destruct (Z_eq_dec x a). left; simpl; auto. destruct IHs. left; simpl; auto. right. intro H; simpl in H; destruct H; auto. Defined. Definition add : forall x s, { s' | forall y, In y s' <-> y=x \/ In y s }. Proof. intros x s. exists (x::s). intros y. simpl. intuition. Qed. Definition remove : forall x s, { s' | forall y, In y s' <-> In y s /\ x<>y }. Proof. induction s. exists nil. intuition. destruct IHs as (s', Hs'). destruct (Z_eq_dec x a). exists s'. subst. intros. rewrite Hs'. simpl; intuition. exists (a::s'). intros; simpl. rewrite Hs'. intuition. Qed. End FirstVersion. Inductive sorted : list Z -> Prop := sorted_nil : sorted nil | sorted_single : forall a, sorted (a::nil) | sorted_2 : forall a b l, a <= b -> sorted (b::l) -> sorted (a::b::l). Hint Constructors sorted. Lemma sorted_inv : forall l a, sorted (a::l) -> sorted l. Proof. inversion 1; auto. Qed. Lemma sorted_cons : forall l x, sorted l -> (forall y, List.In y l -> x<=y) -> sorted (x::l). Proof. destruct l; auto. intros x Hs H. simpl in *; auto. Qed. Lemma in_above : forall l a x, sorted (a::l) -> List.In x l -> a<=x. Proof. induction l as [ | b l IH ]. contradiction. intros a x H; inversion H; subst. simpl. intros [EQ|IN]. omega. apply Zle_trans with b; auto. Qed. (* 2) Implement more clever functions for set := { l : list Z | sorted l } *) Module SecondVersion. Definition set := { l | sorted l }. Definition In (x:Z)(s:set) := List.In x (proj1_sig s). Definition mem : forall x s, { In x s }+{ ~ In x s }. Proof. destruct s as (s,hs). unfold In; simpl. induction s. right. auto. destruct (Z_dec x a) as [[LT|GT]|EQ]. right. simpl. intros [EQ|IN]. omega. assert (a<=x) by (apply in_above with s; auto). omega. destruct IHs. inversion hs; auto. left; simpl; auto. right; simpl; auto. intro H; destruct H; auto. omega. left; simpl; auto. Defined. Fixpoint add_pure x s := match s with | nil => x::nil | a::s' => match Zcompare x a with | Eq => s | Lt => x::s | Gt => a::(add_pure x s') end end. Lemma add_ok : forall x s, sorted s -> forall y, List.In y (add_pure x s) <-> y=x \/ List.In y s. Proof. induction s. simpl. intuition. intros. simpl. case_eq (Zcompare x a); intros CMP. apply Zcompare_Eq_eq in CMP. simpl. intuition. simpl. intuition. change (x>a) in CMP. simpl. rewrite IHs. intuition. apply sorted_inv in H; auto. Qed. Lemma add_sorted : forall x s, sorted s -> sorted (add_pure x s). Proof. induction s. simpl. auto. simpl. case_eq (Zcompare x a); intros CMP. auto. change (xa) in CMP. intros. apply sorted_cons. apply IHs. apply sorted_inv in H; auto. intros y. rewrite add_ok. destruct 1. omega. apply in_above with s; auto. apply sorted_inv in H; auto. Qed. Program Definition add x s : { s' | forall y, In y s' <-> y=x \/ In y s } := add_pure x s. Next Obligation. destruct s as (s,hs); simpl. apply add_sorted; auto. Qed. Next Obligation. destruct s as (s,hs); unfold In; simpl. apply add_ok; auto. Qed. End SecondVersion. (* If you have extra time, try to implement more set operators (remove, inter, union, ...), or other representations of sets (trees,...) *)