(* Walka z Inversion *) (* Axiom falsz : False. Ltac joker := destruct falsz. *) Inductive Even : nat -> Prop := evO : Even 0 | evSS : forall n, Even n -> Even (S(S n)). (* Goal forall n, Even (2+n) -> Even n. destruct 1. Show Proof. Focus 2. induction H. Show Proof. Focus 2. *) Goal forall m, Even m -> forall n, m=2+n -> Even n. destruct 1. simpl. intros. simplify_eq H. simpl. intros. simplify_eq H0. intro. rewrite <- H1. assumption. Qed. Goal forall n, Even (2+n) -> Even n. (* inversion 1. assumption. Show Proof. *) inversion_clear 1. assumption. Qed. Goal forall n, Even (2+n) -> Even n. intros. remember (2+n) as m. destruct H. discriminate Heqm. inversion Heqm. subst. assumption. Show Proof. Qed. Lemma nie1 : ~Even 1. intro. (* case H. destruct H. *) inversion H. Qed. Inductive plistn (A:Set) : nat -> Set := pniln : plistn A O | pconsn : A -> forall n, plistn A n -> plistn A (S n). Fixpoint In (A:Set) (a:A) (n:nat) (l : plistn A n) {struct l} : Prop := match l with pniln => False | pconsn b m l' => a=b \/ In A a m l' end. Lemma pnil_zero : forall (A:Set) (l : plistn A 0), forall a:A, ~(In A a 0 l). intros. dependent inversion l. Show Proof. simpl. intro. assumption. Qed.