Skip to content
Snippets Groups Projects
Commit 72d56d40 authored by François Clément's avatar François Clément
Browse files

Rename asym_equiv -> asym_equiv_alt.

Add antisym_equiv, asym_equiv, conn_equiv, conn_alt_equiv, str_conn_equiv.
parent dfc05c3e
No related branches found
No related tags found
No related merge requests found
......@@ -315,6 +315,44 @@ Hypothesis HT : eq_dec T.
Variable R : T -> T -> Prop.
Lemma antisym_equiv :
antisymmetric R <-> forall x y, br_and_conv R x y -> x = y.
Proof.
split; intros H x y.
intros [H1 H2]; apply H; easy.
intros H1 H2; apply H; easy.
Qed.
Lemma asym_equiv : asymmetric R <-> forall x y, ~ (br_and_conv R x y).
Proof.
split; intros H x y.
intros [H1 H2]; apply (H x y); easy.
intros H1 H2; apply (H x y); easy.
Qed.
Lemma conn_equiv : connected R <-> forall x y, x <> y -> comparable R x y.
Proof. easy. Qed.
Lemma conn_contra_equiv :
connected_contra R <->
forall x y, br_and_conv (complementary R) x y -> x = y.
Proof.
split; intros H x y.
intros [H1 H2]; apply H; easy.
intros H1 H2; apply H; easy.
Qed.
Lemma conn_alt_equiv :
connected_alt R <-> forall x y, comparable R x y \/ x = y.
Proof.
split; intros H x y.
destruct (H x y) as [H1 | [H1 | H1]]; [left; left | right | left; right]; easy.
destruct (H x y) as [[H1 | H1] | H1]; tauto.
Qed.
Lemma str_conn_equiv : strongly_connected R <-> forall x y, comparable R x y.
Proof. easy. Qed.
Lemma asym_antisym : asymmetric R -> antisymmetric R.
Proof. intros H x y H1 H2. exfalso; apply (H _ _ H1 H2). Qed.
......@@ -336,7 +374,7 @@ Proof.
intros H; split; [apply irrefl_asym_w_trans; easy | apply asym_irrefl].
Qed.
Lemma asym_equiv : asymmetric R <-> irreflexive R /\ antisymmetric R.
Lemma asym_equiv_alt : asymmetric R <-> irreflexive R /\ antisymmetric R.
Proof.
split; intros.
split; [apply asym_irrefl | apply asym_antisym]; easy.
......@@ -576,6 +614,13 @@ Lemma trans_incompar_rev :
transitive (incomparable R) -> transitive R.
Proof.
intros R1 H1 H2 H3 x y z; apply imp3_imp_equiv; intros H4.
destruct (H2 x y) as [H5 | H5], (H2 y z) as [H6 | H6]; try tauto.
apply not_and_equiv; intros [H7 H8].
specialize (H3 x y z).
rewrite imp3_imp_equiv in H3. unfold incomparable in H3.
rewrite -!not_or_equiv in H3. rewrite !NNPP_equiv in H3.
apply H5.
Aglopted. *)
(** With the br_and_conv operation. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment