Fixpoint belast (x:nat) (l:list nat) := match l with | nil => nil | cons y l => cons x (belast y l) end. Lemma length_belast x s : length (belast x s) = length s. revert x. (* We need to generalize over x because the first argument of belast changes along the recursive calls. Observe the type of IHs with or without the revert *) induction s; simpl; intros. reflexivity. rewrite IHs; reflexivity. Qed. Fixpoint skip (l:list nat) := match l with | cons x (cons y l) => cons y (skip l) | _ => nil end. (* First attempt (failed) to prove the lemma by simple induction: Lemma length_skip' l : 2 * length (skip l) <= length l. induction l; simpl; intros. auto. destruct l; simpl; auto. simpl in IHl. *) (* IHl is about (skip (n::l)) or skip of the tail of l, but says nothing about skip l. Two solutions: - use fix to apply the induction hypothesis not on the direct subterm, but on the second subterm (just like skip) - generalize the statement to prove the theorem for l and (n::l) or the tail of l. *) Lemma length_skip l : 2 * length (skip l) <= length l. revert l. fix 1. (* recursion over the first argument: l *) destruct l as [ | x [ | y l] ]; simpl. auto. auto. rewrite <- plus_n_Sm. Search le. (* Use Search to find lemmas about a constant *) Require Import Arith. (* Arith contains many lemmas about le *) Search le. apply le_n_S. apply le_n_S. apply length_skip. Qed. Lemma length_skip' l : 2 * length (skip l) <= length l. (* We generalize the statement to prove to l and n::l *) assert (2 * length (skip l) <= length l /\ forall n, 2 * length (skip (n::l)) <= S (length l)). induction l; simpl; intros; auto. destruct IHl as (IHl,IHconsl). destruct l as [|n l']; simpl; auto. simpl in IHconsl. split; intros. (* for n::l', this is exactly the second part of the induction hypothesis *) apply IHconsl. exact 0. (* for n0::n::l', it uses the induction hypothesis on l' and the proof goes exactly as in length_skip *) simpl in IHl. rewrite <- plus_n_Sm. apply le_n_S. apply le_n_S. apply IHl. (* Now we just have to drop the second part of the strengthened statement *) destruct H. trivial. Qed. (* 2- - leq is OK: n' is a s ubterm of n - exp is not OK: recursive call on (S n), not a subterm of n (even though the stop condition (leq p n) will eventually become true) - ackermann is OK: 1- g m' is OK since m' is a subterm of m, so the fix g is OK 2- f n' _ is OK since n' is a subterm of n, so the main fix is OK *) Parameter T1 T2:Type. Parameter (t1:T1) (t2:T2). Definition g (b:bool) := match b return if b then T1 else T2 with true => t1 | false => t2 end. Inductive W (A:Type) (B:A->Type) := node : forall (a:A), (B a -> W A B) -> W A B. Check (W_rect : forall A B (P:W A B->Type), (forall a f, (forall b:B a, P (f b)) -> P (node A B a f)) -> forall w:W A B, P w). Definition nat_A := bool. Definition nat_B (a:nat_A) : Type := if a then False else unit. Definition natW := W nat_A nat_B. Definition OW : natW := node nat_A nat_B true (False_rect natW). Definition SW (n:natW) : natW := node nat_A nat_B false (fun _ => n). Definition bt_A := bool. Definition bt_B (V:Type) (a:bt_A) : Type := if a then False else bool. Definition tree V := W bt_A (bt_B V). Definition leaf V : tree V := node _ _ true (False_rect (tree V)). Definition bin V (l:tree V) (x:V) (r:tree V) : tree V := node _ _ false (fun b:bool => if b then l else r). Parameter n : natW. Definition f1 (x:unit) : natW := n. Definition f2 (x:unit) : natW := match x with tt => n end. Lemma f1_n x : f1 x = n. reflexivity. Qed. Lemma f2_n x : f2 x = n. destruct x. reflexivity. Qed. (* If f1 and f2 were convertible, the following command would succeed: *) Fail Check (eq_refl f1 : f1 = f2). Definition Sn : natW := node nat_A nat_B false f1. Definition alt_Sn : natW := node nat_A nat_B false f2. (* Sn is exactly SW n, but alt_Sn is neither convertible to OW or to SW k for some k. So it is not possible to define the dependent eliminator of natW: Given (P:natW->Type) (h0 : P OW) (hS: forall n, P n -> P (SW n)), there is no term of type (P alt_Sn) We can define an equality on W-types by comparing functions extensionally *) Inductive eqW {A B} : W A B -> W A B -> Prop := | eqWi a f1 f2 : (forall b:B a, eqW (f1 b) (f2 b)) -> eqW (node _ _ a f1) (node _ _ a f2). (* This equality is reflexive (and we could show it is symmetric and transitive) *) Lemma eqW_refl {A B} (w:W A B) : eqW w w. induction w; intros. constructor; intros. trivial. Qed. (* It solves the problem of alt_Sn: we can prove it is equal to Sn *) Lemma eqW_Sn : eqW Sn alt_Sn. constructor; intros. rewrite f1_n, f2_n. apply eqW_refl. Qed. (* More generally, we can prove the dependent elimination scheme for predicates P that respect eqW. This implies: forall n:natW, eqW n OW \/ exists k:natW, eqW n SW k *) Lemma natW_rect : forall (P:natW->Type), (forall w1 w2, eqW w1 w2 -> P w1 -> P w2) -> P OW -> (forall n, P n -> P (SW n)) -> forall i, P i. intros P resp h0 hS. induction i. destruct a. apply resp with OW; trivial. constructor. simpl. destruct b. simpl in w. apply resp with (SW (w tt)). constructor. destruct b; apply eqW_refl. apply hS. apply X. Defined.