(* Rownosc *) Print eq. (* x=x dla x:A to skrot od (eq A x x) *) (* Dowodzenie rownosci . *) Lemma re : forall (A:Set) (x:A), x=x. Lemma true_albo_false : forall b:bool, b=true \/ b=false. (* Uzywanie rownosci *) Lemma Leibniz : forall (A:Set)(x y:A), x=y -> forall (P:A->Prop), (P x) -> (P y). Lemma eq_trans: forall (A:Set) (x y z:A), x=y->y=z->x=z. Lemma f_funkcja : forall (A B:Set)(f:A->B)(x y:A), x=y -> (f x)=(f y). Print Leibniz. (* Jak sie typuje ten match ? *) (* Wezmy najpierw prostszy przyklad: *) Inductive Even : nat -> Prop := evenO : (Even O) | evenSS : forall (n:nat), (Even n) -> (Even (S (S n))). Lemma Even_pred_pred : forall (n:nat), (Even n) -> (Even (pred (pred n))). (* Jak sie typuje ten match ? *) (* Ten od rownosci typuje sie tak samo ! *) (**********************************************************) (* Match zalezny *) Lemma zero_lub_nie_zero : forall n, n=O \/ n=(S (pred n)). Show Proof. (* Jak sie typuje ten match ? *) (* napisac _recznie_ stala *) Definition nat_case : forall (P:nat -> Prop), (P O) -> (forall (n:nat), (P (S n))) -> forall (n:nat), (P n) := (**********************************************************) (* Definicje przez punkt staly *) Fixpoint plus (n m:nat) {struct n} : nat := match n with | O => m | S p => S (plus p m) end. (* zdefiniuj mnozenie *) Fixpoint razy (n m:nat) {struct n} : nat := (* zdefiniowac recznie zasade indukcji: *) (* uzywajac Fixpoint i match *) (* nat_rec : forall P : nat->Prop, P O -> (forall n:nat, P n -> P (S n)) -> forall n:nat, P n *) Fixpoint nat_rec (P: nat->Prop) (o:P O) (ss: forall n:nat, P n -> P (S n)) (n:nat) {struct n} : (P n) := (* dowody przez indukcje *) Lemma plus_zero : forall (n:nat),(plus n O)=n. Lemma plus_przem : forall (n m:nat), (plus n m) = (plus m n).