(* Exercise 6.1 *)
Theorem nso: forall x, S x <> O.
Proof.
intros x A.
set (p:=fun x => match x with 0 => True | S_ => False end).
assert (C: p(S x)). rewrite A. unfold p. trivial.
apply C.
Qed.

Theorem ntf: true <> false.
Proof.
Admitted.

Theorem S_injective: forall x y, S x = S y -> x=y.
Proof.
Admitted.

(* Exercise 6.2 *)
Parameter X : Type.

Definition relation := X -> X -> Prop.
Definition reflexive (r: relation) := forall x, r x x.
Definition transitive (r: relation) := forall x y z, r x y -> r y z -> r x z.
Definition contained (r p: relation) := forall x y, r x y -> p x y.
Definition left_trans (r p: relation) := forall x y z, r x y -> p y z -> p x z.

Inductive stari (r: relation): relation :=
|  stari_R : reflexive (stari r)
|  stari_LT : left_trans r (stari r).

Definition stard (r: relation): relation := fun x y =>
forall p, reflexive p -> left_trans r p -> p x y.

Definition id: relation := fun x y => x=y.
Definition comp (r p: relation) : relation := fun x y => exists z, r x z /\ p z y.
Fixpoint iter (X:Type) n x (f: X->X) := match n with 0 => x | S n' => f(iter X n' x f) end.

Definition starn (r: relation) : relation := fun x y => exists n, iter relation n id (comp r) x y.

Ltac sinv h := (inversion h; clear h; subst).

Lemma stari_T r : transitive (stari r).
Proof.
Admitted.

Lemma i2n r: contained (stari r) (starn r).
Proof.
Admitted.

Lemma n2i r: contained (starn r) (stari r).
Proof.
unfold contained. unfold starn. intros.
elim H. intro n. generalize x y. clear x y H.
induction n; simpl.
unfold id. intros. subst. apply stari_R.
unfold comp at 1. intros. sinv H. sinv H0.
apply IHn in H1. eapply stari_LT; eauto.
Qed.

Lemma d2i r: contained (stard r) (stari r).
Proof.
Admitted.

Lemma i2d r: contained (stari r) (stard r).
Proof.
Admitted.

Lemma stard_R r: reflexive (stard r).
Proof.
Admitted. 

Lemma stard_LT r: left_trans r (stard r).
Proof.
Admitted.

Lemma stard_wind r p: 
reflexive p -> left_trans r p -> contained (stard r) p.
Proof.
Admitted.

Lemma stard_ind (r p: relation): 
reflexive p -> 
(forall x y z, r x y -> stard r y z -> p y z -> p x z) -> 
contained (stard r) p.
Proof.
intros.
set (q:= fun x y => p x y /\ stard r x y).
assert (A: contained (stard r) q).
apply stard_wind.
unfold reflexive. unfold q. intuition. apply stard_R.
unfold left_trans. unfold q. intuition. eapply H0; eauto.
eapply stard_LT; eauto.
unfold q in A. unfold contained in A.
unfold contained. intuition. apply A in H1. intuition.
Qed.

Lemma stard_T r: transitive (stard r).
Proof. 
Admitted.