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. Set Implicit Arguments. Definition is_prefix_of A (u v : list A) := exists w, u ++ w = v. (* Exercise 1: 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 }. (* Exercise 2: Implementation of finite sets of integers. We would like to precisely implement the following interface for sets of integers *) Require Import ZArith. Open Scope Z_scope. 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' <-> x=y \/ In y s }. (* Q.1) Propose an naive implementation with set := list Z *) (* We propose the following way of stating that a list is sorted *) 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. (* The following properties might help. Proving then is not a priority here, but you can try later (at the end of the session). *) Lemma sorted_inv : forall l a, sorted (a::l) -> sorted l. Admitted. Lemma sorted_cons : forall l x, sorted l -> (forall y, List.In y l -> x<=y) -> sorted (x::l). Admitted. Lemma in_above : forall l a x, sorted (a::l) -> List.In x l -> a<=x. Admitted. (* Q.2) Implement more clever functions for set := { l : list Z | sorted l } *) (* If you have extra time, try to implement more set operators (remove, inter, union, ...), or other representations of sets (trees,...) *)