### solutions TD3

parent 0fe64ebf
 Require Import List Arith. Import ListNotations. Set Implicit Arguments. (* Lemma nil_app : forall A (l:list A), nil ++ l = l. or shorter, with foralls rewritten as parameters: *) Lemma nil_app A (l:list A) : [] ++ l = l. Proof. reflexivity. Qed. Lemma app_nil A (l:list A) : l ++ [] = l. Proof. induction l. - reflexivity. - simpl. f_equal. apply IHl. (* or simpl. rewrite IHl. reflexivity. *) Qed. Lemma app_assoc A (u v w : list A) : (u++v)++w = u++(v++w). Proof. induction u. (* Avoid induction on v or w, won't help, no/little simplifications *) - simpl. reflexivity. - simpl. f_equal. apply IHu. Qed. (* Fixpoint length {A} (l:list A) := match l with | [] => 0 | _ :: l => S (length l) end. *) Print Datatypes.length. (* how is done the standard definition of List.length ? *) Lemma app_len {A} (l1 l2 : list A) : length (l1 ++ l2) = length l1 + length l2. Proof. induction l1; simpl. - reflexivity. - now f_equal. (* now is a tactic that solves basic proofs (it calls a automatic tactic called "easy") *) Qed. Search "++" length. (* For retrieving all standard lemmas about app and length *) (* REV First, if we use the "quadratic" rev definition (for instance List.rev), then the proofs are relatively easy, but computing with this rev is slow *) Print List.rev. (* it's the same as the following "slow" rev *) Fixpoint slow_rev {A} (l:list A) := match l with | [] => [] | x::l => slow_rev l ++ [x] end. Lemma slow_rev_length {A} (l : list A) : length (slow_rev l) = length l. Proof. induction l; simpl; auto. rewrite app_length. simpl. rewrite Nat.add_1_r. now f_equal. Qed. Lemma slow_rev_app {A} (l1 l2 : list A) : slow_rev (l1 ++ l2) = slow_rev l2 ++ slow_rev l1. Proof. induction l1; simpl; auto. - now rewrite app_nil. - rewrite IHl1. now rewrite app_assoc. Qed. (* Now, with the efficient definition suggested in this TD3, computing is linear in the size of the list, but proofs are more delicate : we need generalized statements on rev_append before specializing them to rev. *) Fixpoint rev_append {A} (l l' : list A) := match l with | [] => l' | x::l => rev_append l (x::l') end. Definition rev {A} (l:list A) := rev_append l []. Lemma rev_append_length {A} (l l' : list A) : length (rev_append l l') = length l + length l'. Proof. revert l'. (* for turning l' back into a forall, and have later a IH starting with forall. *) induction l; simpl; auto. intros. rewrite IHl. simpl. apply Nat.add_succ_r. Qed. Lemma rev_length {A} (l : list A) : length (rev l) = length l. Proof. unfold rev. rewrite rev_append_length. simpl. apply Nat.add_0_r. Qed. Lemma rev_append_app {A} (l1 l2 l' : list A) : rev_append (l1 ++ l2) l' = rev_append l2 (rev_append l1 l'). Proof. revert l'. induction l1; simpl; auto. Qed. Lemma rev_append_rev_app {A} (l l' : list A) : rev_append l l' = rev l ++ l'. Proof. revert l'. induction l; simpl; auto. intros. unfold rev. simpl. rewrite 2 IHl. rewrite app_assoc. reflexivity. Qed. Lemma rev_app {A} (l1 l2 : list A) : rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. unfold rev at 1 3. rewrite rev_append_app. rewrite rev_append_rev_app. reflexivity. Qed. (* Extra exercice : prove that `slow_rev l = rev l` *) Lemma slow_rev_rev {A} (l : list A) : slow_rev l = rev l. Proof. induction l. - simpl; auto. - simpl. unfold rev. simpl. rewrite rev_append_rev_app. now f_equal. Qed. (** SPLIT *) Fixpoint split {A} (l:list A) := match l with | [] => ([],[]) | a::l => let (l1,l2) := split l in (a::l2,l1) end. Fixpoint splitbis {A} (l:list A) := match l with | [] => ([],[]) | [a] => ([a],[]) | a::b::l => let (l1,l2) := splitbis l in (a::l1,b::l2) end. Lemma split_equiv_aux {A} (l:list A) : split l = splitbis l /\ forall x, split (x::l) = splitbis (x::l). Proof. induction l. - simpl; auto. - split. + apply IHl. + intros x. simpl. destruct IHl as (IH,_). rewrite IH. destruct (splitbis l) as (l1,l2). reflexivity. Qed. Lemma split_equiv {A} (l:list A) : split l = splitbis l. Proof. apply split_equiv_aux. Qed. (* Actually, we could do the previous proof directly, without auxiliary lemma, but that involves a generalized induction on all strictly smaller lists. *) Lemma split_equiv_direct {A} (l:list A) : split l = splitbis l. Proof. remember (length l) as n. revert l Heqn. induction n as [n IH] using lt_wf_ind. (* wf : "well founded" induction *) intros [|a [|b l]] E; simpl in *; trivial. replace (splitbis l) with (split l). - now destruct (split l). - apply (IH (length l)); subst; auto with arith. Qed. Lemma split_In {A} (l:list A) : let (l1,l2) := split l in forall x, In x l <-> In x l1 \/ In x l2. Proof. induction l. - simpl; intuition. - simpl. destruct (split l) as (l1,l2). simpl. intros. rewrite IHl. intuition. Qed. Lemma split_length {A} (l:list A) : let (l1,l2) := split l in length l1 = length l2 \/ length l1 = S (length l2). Proof. induction l. - simpl; auto. - simpl. destruct (split l) as (l1,l2). simpl. destruct IHl. + right. now f_equal. + now left. Qed. (* Some extra statements on the length of split : *) Lemma split_length_add {A} (l:list A) : let (l1,l2) := split l in length l = length l1 + length l2. Proof. induction l. - simpl; auto. - simpl. destruct (split l) as (l1,l2). simpl. f_equal. rewrite IHl. apply Nat.add_comm. Qed. Lemma split_div2 {A} (l:list A) : let (l1,l2) := split l in length l1 = (S (length l))/2 /\ length l2 = (length l) / 2. Proof. rewrite <- !Nat.div2_div. (* Nat.div2 is nicer that /2 during recursive proofs *) induction l; simpl; auto. destruct (split l) as (l1,l2). simpl. split. - now f_equal. - apply IHl. Qed.
 ... ... @@ -122,7 +122,7 @@ Lemma split_equiv_aux {A} (l:list A) : split l = splitbis l /\ forall x, split (x::l) = splitbis (x::l). ``` Show that `split` indeed dispatch the elements in the two final lists. For instance: Show that `split` indeed dispatches the elements in the two final lists. For instance: ```coq Lemma split_contains {A} (l:list A) : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment