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

Fix {lex,colex}_trans.

Modify {symlex,revlex}_trans.
parent 69dda88a
No related branches found
No related tags found
No related merge requests found
Pipeline #8603 waiting for manual action
......@@ -933,36 +933,50 @@ Lemma revlexT_antisym :
antisymmetric R -> forall n, antisymmetric (@revlexT _ R n).
Proof. intros; apply antisym_conv, colexT_antisym; easy. Qed.
(* This seems wrong! Maybe some hypotheses are missing... *)
Lemma lex_trans :
forall P, transitive R -> forall n, transitive (@lex _ R P n).
antisymmetric R \/ asymmetric R -> transitive R ->
forall P n, transitive (@lex _ R P n).
Proof.
intros P H1 n x y z; induction n; [easy |].
rewrite !lex_S; intros [[H2a H2b] | [H2 H3]] [[H4a H4b] | [H4 H5]].
left; split; [admit (* WRONG? *) | apply H1 with (y ord0); easy].
rewrite -H4; left; easy.
rewrite H2; left; easy.
right; split; [rewrite H2 | apply IHn with (skipF y ord0)]; easy.
Admitted.
intros H1 H2 P n x y z; induction n; [easy |].
rewrite !lex_S; intros [[H3a H3b] | [H3 H4]] [[H5a H5b] | [H5 H6]].
(* *)
left; split; [| apply H2 with (y ord0); easy].
destruct (HT (x ord0) (z ord0)) as [H4 |]; [exfalso | easy].
rewrite H4 in H3b; destruct H1 as [H1 | H1].
contradict H5a; apply H1; easy.
contradict H5b; apply H1; easy.
(* *)
rewrite -H5; left; easy.
rewrite H3; left; easy.
right; split; [rewrite H3 | apply IHn with (skipF y ord0)]; easy.
Qed.
(* This seems wrong! Maybe some hypotheses are missing... *)
Lemma colex_trans :
forall P, transitive R -> forall n, transitive (@colex _ R P n).
antisymmetric R \/ asymmetric R -> transitive R ->
forall P n, transitive (@colex _ R P n).
Proof.
intros P H1 n x y z; induction n; [easy |].
rewrite !colex_S; intros [[H2a H2b] | [H2 H3]] [[H4a H4b] | [H4 H5]].
left; split; [admit (* WRONG? *) | apply H1 with (y ord_max); easy].
rewrite -H4; left; easy.
rewrite H2; left; easy.
right; split; [rewrite H2 | apply IHn with (skipF y ord_max)]; easy.
Admitted.
intros H1 H2 P n x y z; induction n; [easy |].
rewrite !colex_S; intros [[H3a H3b] | [H3 H4]] [[H5a H5b] | [H5 H6]].
(* *)
left; split; [| apply H2 with (y ord_max); easy].
destruct (HT (x ord_max) (z ord_max)) as [H4 |]; [exfalso | easy].
rewrite H4 in H3b; destruct H1 as [H1 | H1].
contradict H5a; apply H1; easy.
contradict H5b; apply H1; easy.
(* *)
rewrite -H5; left; easy.
rewrite H3; left; easy.
right; split; [rewrite H3 | apply IHn with (skipF y ord_max)]; easy.
Qed.
Lemma symlex_trans :
forall P, transitive R -> forall n, transitive (@symlex _ R P n).
antisymmetric R \/ asymmetric R -> transitive R ->
forall P n, transitive (@symlex _ R P n).
Proof. intros; apply trans_conv, lex_trans; easy. Qed.
Lemma revlex_trans :
forall P, transitive R -> forall n, transitive (@revlex _ R P n).
antisymmetric R \/ asymmetric R -> transitive R ->
forall P n, transitive (@revlex _ R P n).
Proof. intros; apply trans_conv, colex_trans; easy. Qed.
Lemma lexF_conn_alt :
......
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