(** Inductive predicates *) Require Import Arith. Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, even n -> even (S (S n)). Example E10: even 10. apply even_S. constructor. repeat constructor. Qed. Print E10. Lemma double_even : forall n, even (2 * n). Proof. induction n;simpl. constructor. simpl in IHn. SearchRewrite (_ + S _). SearchRewrite (_ + 0). repeat (rewrite <- plus_n_O in * || rewrite <- plus_n_Sm in *). constructor. assumption. Qed. Lemma even_double : forall n , even n -> exists k, n = 2 * k. Proof. intros n H. Check even_ind. induction H. - now exists 0. - destruct IHeven as [k Hk]. exists (S k). rewrite Hk. Require Import ArithRing. ring. Qed. (** Warning! The following stuff is already defined in Coq *) Inductive le (n:nat) : nat -> Prop := | le_n : n <= n | le_S : forall p, n <= p -> n <= S p where "n <= p" := (le n p). Example le_6_8 : 6 <= 8. constructor. constructor. constructor. Qed. Hint Constructors le. Example le_6_8_again : 6 <= 8. auto. Qed. Lemma le_n_plus_pn : forall n p:nat, n <= p + n. Proof. intro n;induction p. auto. simpl. constructor. trivial. Qed. Hint Resolve le_n_plus_pn. Lemma le_n_plus_np : forall n p:nat, n <= n + p. Proof. intros n p;rewrite (plus_comm n p). auto. Qed. Lemma le_plus : forall n p, n <= p -> exists q, n + q = p. intros n p H. About le_ind. induction H. exists 0. rewrite plus_comm. reflexivity. destruct IHle as [q Hq]. exists (S q). subst p;ring. Qed. Lemma le_trans : forall n p q , n <= p -> p <= q -> n <= q. Proof. intros n p q H;induction H. auto. intros. (* @#@#@#@~~@@@@@!!!!!! *) Restart. intros n p q H H0. (** induction H0 will try to prove P(q) aka n <= q for any q >= p *) induction H0. (* the base case is (P p) i.e. (n <= p) *) auto. (** the induction step assumes IHle : (P p0) for some p0 >= p and trues to infer (P (S p0)), i.e. (n <= (S p0)) *) constructor 2. assumption. Qed. Inductive and (P Q:Prop) : Prop := conj : P -> Q -> (and P Q). Notation "P /\ Q" := (and P Q). Check and_ind. Inductive or (P Q : Prop) := | or_intro_l : P -> or P Q | or_intro_r : Q -> or P Q. Notation "P \/ Q" := (or P Q). Inductive False : Prop :=. Check False_ind. Inductive ex {A: Type}(P:A-> Prop) := ex_intro : forall w:A, P w -> ex P. Notation "'my_exists' w ',' Q" := (ex (fun w => Q)) (at level 200). Goal my_exists n, (0 < n). apply ex_intro with 3. auto. Qed. Inductive leibniz {A:Type}(x:A) : A -> Prop := refl_equal : leibniz x x. Notation "x = y" := (leibniz x y). Check eq_ind.