Definition negb b := match b with true => false | false => true end. Definition andb b1 b2 := match b1 with | true => b2 | false => false end. Eval compute in fun b => andb false b. (* fun _ => false *) Eval compute in fun b => andb b false. (* fun b => if b then false else false *) Parameter T1 T2:Type. Parameter t1:T1. Parameter t2:T2. Definition g (b:bool) := match b return if b then T1 else T2 with | true => t1 | false => t2 end. Definition g' (b:bool) := match negb b as b' return if b' then T2 else T1 with | true => t2 | false => t1 end. Inductive even : nat -> Prop := | evenO : even 0 | evenS n : even n -> even (S (S n)). Require Import Omega. Lemma even_is_double n : even n -> exists m, n=m+m. induction 1. exists 0; reflexivity. destruct IHeven as (m,?). exists (S m). omega. Qed. Lemma even_is_double' n : (even n -> exists m, n=m+m) /\ (even (S n) -> exists m, S n = m+m). induction n; simpl; split; intros. exists 0; reflexivity. inversion H. destruct IHn. auto. destruct IHn. destruct H0 as (m,?). inversion_clear H; trivial. exists (S m). omega. Qed. Fixpoint belast (x:nat) l := match l with | nil => nil | cons y l => cons x (belast y l) end. Lemma length_belast x l : length (belast x l) = length l. revert x. (* we need to quntify over all x *) induction l; simpl; intros; auto. Qed. Fixpoint skip (l:list nat) := match l with | cons x (cons y l) => cons x (skip l) | _ => nil end. Lemma length_skip : forall l, 2 * length (skip l) <= length l. fix Hrec 1. destruct l; simpl. auto. destruct l; simpl. auto. specialize Hrec with (l:=l). omega. Qed. Fixpoint prodn (A:Type) n : Type := match n with | 0 => unit | 1 => A | S k => (A * prodn A k)%type end. Fixpoint length {A:Type} (l:list A) : nat := match l with | nil => 0 | cons _ l' => S (length l') end. Fixpoint embed {A} (l:list A) : prodn A (length l) := match l return prodn A (length l) with | nil => tt | cons a l' => (* make the recursive call here. p' : prodn A (length l') *) let p' : prodn A (length l') := embed l' in let h : prodn A (length l') -> prodn A (length (a::l')) := (* abstract over the type of p' *) match l' with | nil => fun _:unit => a | cons a' l'' => fun p':prodn A (length(a'::l'')) => (* Now the new p' has type prodn A (S (length l''))*) (a,p') end in h p' end.