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

Cosmetics.

parent d7a118ea
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Subsets/Finite_family.v
+ 77
− 77
View file @ 2172230a
This diff is collapsed.
Subsets/Finite_table.v
+ 31
− 31
View file @ 2172230a
...@@ -735,26 +735,26 @@ Lemma liftT_S_equiv_def : ...@@ -735,26 +735,26 @@ Lemma liftT_S_equiv_def :
Proof. easy. Qed. Proof. easy. Qed.
Lemma insertTr_correct_l : Lemma insertTr_correct_l :
forall {m n} {i0 i} A (M : 'E^{m,n}), i = i0 -> insertTr i0 A M i = A. forall {m n i0 i} A (M : 'E^{m,n}), i = i0 -> insertTr i0 A M i = A.
Proof. intros; apply insertF_correct_l; easy. Qed. Proof. intros; apply insertF_correct_l; easy. Qed.
Lemma insertTr_correct_r : Lemma insertTr_correct_r :
forall {m n} {i0 i} (H : i <> i0) A (M : 'E^{m,n}), forall {m n i0 i} (H : i <> i0) A (M : 'E^{m,n}),
insertTr i0 A M i = M (insert_ord H). insertTr i0 A M i = M (insert_ord H).
Proof. intros; apply insertF_correct_r; easy. Qed. Proof. intros; apply insertF_correct_r; easy. Qed.
Lemma insertTc_correct_l : Lemma insertTc_correct_l :
forall {m n} {j0 j} i B (M : 'E^{m,n}), forall {m n j0 j} i B (M : 'E^{m,n}),
j = j0 -> insertTc j0 B M i j = B i. j = j0 -> insertTc j0 B M i j = B i.
Proof. intros; apply insertF_correct_l; easy. Qed. Proof. intros; apply insertF_correct_l; easy. Qed.
Lemma insertTc_correct_r : Lemma insertTc_correct_r :
forall {m n} {j0 j} (H : j <> j0) i B (M : 'E^{m,n}), forall {m n j0 j} (H : j <> j0) i B (M : 'E^{m,n}),
insertTc j0 B M i j = M i (insert_ord H). insertTc j0 B M i j = M i (insert_ord H).
Proof. intros; apply insertF_correct_r; easy. Qed. Proof. intros; apply insertF_correct_r; easy. Qed.
Lemma insertT_correct_lr : Lemma insertT_correct_lr :
forall {m n} {i0 i} j0 x A B (M : 'E^{m,n}), forall {m n i0 i} j0 x A B (M : 'E^{m,n}),
i = i0 -> insertT i0 j0 x A B M i = insertF j0 x A. i = i0 -> insertT i0 j0 x A B M i = insertF j0 x A.
Proof. move=>>; apply insertTr_correct_l. Qed. Proof. move=>>; apply insertTr_correct_l. Qed.
...@@ -769,7 +769,7 @@ rewrite insertTr_correct_r insertF_correct_r insertTc_correct_l; easy. ...@@ -769,7 +769,7 @@ rewrite insertTr_correct_r insertF_correct_r insertTc_correct_l; easy.
Qed. Qed.
Lemma insertT_correct_r : Lemma insertT_correct_r :
forall {m n} {i0 i} (Hi : i <> i0) {j0 j} (Hj : j <> j0) x A B (M : 'E^{m,n}), forall {m n i0 i} (Hi : i <> i0) {j0 j} (Hj : j <> j0) x A B (M : 'E^{m,n}),
insertT i0 j0 x A B M i j = M (insert_ord Hi) (insert_ord Hj). insertT i0 j0 x A B M i j = M (insert_ord Hi) (insert_ord Hj).
Proof. Proof.
intros; unfold insertT; rewrite insertTr_correct_r insertTc_correct_r; easy. intros; unfold insertT; rewrite insertTr_correct_r insertTc_correct_r; easy.
...@@ -871,25 +871,25 @@ Lemma skipT_equiv_def : ...@@ -871,25 +871,25 @@ Lemma skipT_equiv_def :
Proof. easy. Qed. Proof. easy. Qed.
Lemma replaceTr_correct_l : Lemma replaceTr_correct_l :
forall {m n} {i0 i} A (M : 'E^{m,n}), i = i0 -> replaceTr i0 A M i = A. forall {m n i0 i} A (M : 'E^{m,n}), i = i0 -> replaceTr i0 A M i = A.
Proof. move=>>; apply replaceF_correct_l. Qed. Proof. move=>>; apply replaceF_correct_l. Qed.
Lemma replaceTr_correct_r : Lemma replaceTr_correct_r :
forall {m n} {i0 i} A (M : 'E^{m,n}), i <> i0 -> replaceTr i0 A M i = M i. forall {m n i0 i} A (M : 'E^{m,n}), i <> i0 -> replaceTr i0 A M i = M i.
Proof. move=>>; apply replaceF_correct_r. Qed. Proof. move=>>; apply replaceF_correct_r. Qed.
Lemma replaceTc_correct_l : Lemma replaceTc_correct_l :
forall {m n} {j0 j} i B (M : 'E^{m,n}), forall {m n j0 j} i B (M : 'E^{m,n}),
j = j0 -> replaceTc j0 B M i j = B i. j = j0 -> replaceTc j0 B M i j = B i.
Proof. move=>>; apply replaceF_correct_l. Qed. Proof. move=>>; apply replaceF_correct_l. Qed.
Lemma replaceTc_correct_r : Lemma replaceTc_correct_r :
forall {m n} {j0 j} i B (M : 'E^{m,n}), forall {m n j0 j} i B (M : 'E^{m,n}),
j <> j0 -> replaceTc j0 B M i j = M i j. j <> j0 -> replaceTc j0 B M i j = M i j.
Proof. move=>>; apply replaceF_correct_r. Qed. Proof. move=>>; apply replaceF_correct_r. Qed.
Lemma replaceT_correct_lr : Lemma replaceT_correct_lr :
forall {m n} {i0 i} j0 x A B (M : 'E^{m,n}), forall {m n i0 i} j0 x A B (M : 'E^{m,n}),
i = i0 -> replaceT i0 j0 x A B M i = replaceF j0 x A. i = i0 -> replaceT i0 j0 x A B M i = replaceF j0 x A.
Proof. move=>>; apply replaceTr_correct_l. Qed. Proof. move=>>; apply replaceTr_correct_l. Qed.
...@@ -904,7 +904,7 @@ rewrite -> replaceTr_correct_r, replaceF_correct_r, replaceTc_correct_l; easy. ...@@ -904,7 +904,7 @@ rewrite -> replaceTr_correct_r, replaceF_correct_r, replaceTc_correct_l; easy.
Qed. Qed.
Lemma replaceT_correct_r : Lemma replaceT_correct_r :
forall {m n} {i0 i j0 j} x A B (M : 'E^{m,n}), forall {m n i0 i j0 j} x A B (M : 'E^{m,n}),
i <> i0 -> j <> j0 -> replaceT i0 j0 x A B M i j = M i j. i <> i0 -> j <> j0 -> replaceT i0 j0 x A B M i j = M i j.
Proof. Proof.
intros; unfold replaceT; intros; unfold replaceT;
...@@ -2449,50 +2449,50 @@ Lemma eqxT_equiv : ...@@ -2449,50 +2449,50 @@ Lemma eqxT_equiv :
Proof. intros; split. intros; apply skipT_eq; easy. apply skipT_reg. Qed. Proof. intros; split. intros; apply skipT_eq; easy. apply skipT_reg. Qed.
Lemma skipTr_neqxTr_compat : Lemma skipTr_neqxTr_compat :
forall {m n} {i0} {M N : 'E^{m.+1,n}}, forall {m n i0} {M N : 'E^{m.+1,n}},
neqxTr i0 M N -> skipTr i0 M <> skipTr i0 N. neqxTr i0 M N -> skipTr i0 M <> skipTr i0 N.
Proof. move=>>; apply skipF_neqxF_compat. Qed. Proof. move=>>; apply skipF_neqxF_compat. Qed.
Lemma skipTr_neqxTr_reg : Lemma skipTr_neqxTr_reg :
forall {m n} {i0} {M N : 'E^{m.+1,n}}, forall {m n i0} {M N : 'E^{m.+1,n}},
skipTr i0 M <> skipTr i0 N -> neqxTr i0 M N. skipTr i0 M <> skipTr i0 N -> neqxTr i0 M N.
Proof. move=>>; apply skipF_neqxF_reg. Qed. Proof. move=>>; apply skipF_neqxF_reg. Qed.
Lemma skipTc_neqxTc_compat : Lemma skipTc_neqxTc_compat :
forall {m n} {j0} {M N : 'E^{m,n.+1}}, forall {m n j0} {M N : 'E^{m,n.+1}},
neqxTc j0 M N -> skipTc j0 M <> skipTc j0 N. neqxTc j0 M N -> skipTc j0 M <> skipTc j0 N.
Proof. Proof.
move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply skipTc_reg. move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply skipTc_reg.
Qed. Qed.
Lemma skipTc_neqxTc_reg : Lemma skipTc_neqxTc_reg :
forall {m n} {j0} {M N : 'E^{m,n.+1}}, forall {m n j0} {M N : 'E^{m,n.+1}},
skipTc j0 M <> skipTc j0 N -> neqxTc j0 M N. skipTc j0 M <> skipTc j0 N -> neqxTc j0 M N.
Proof. Proof.
move=>>; rewrite contra_not_l_equiv -eqxTc_not_equiv; apply skipTc_eq. move=>>; rewrite contra_not_l_equiv -eqxTc_not_equiv; apply skipTc_eq.
Qed. Qed.
Lemma skipT_neqxT_compat : Lemma skipT_neqxT_compat :
forall {m n} {i0 j0} {M N : 'E^{m.+1,n.+1}}, forall {m n i0 j0} {M N : 'E^{m.+1,n.+1}},
neqxT i0 j0 M N -> skipT i0 j0 M <> skipT i0 j0 N. neqxT i0 j0 M N -> skipT i0 j0 M <> skipT i0 j0 N.
Proof. Proof.
move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply skipT_reg. move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply skipT_reg.
Qed. Qed.
Lemma skipT_neqxT_reg : Lemma skipT_neqxT_reg :
forall {m n} {i0 j0} {M N : 'E^{m.+1,n.+1}}, forall {m n i0 j0} {M N : 'E^{m.+1,n.+1}},
skipT i0 j0 M <> skipT i0 j0 N -> neqxT i0 j0 M N. skipT i0 j0 M <> skipT i0 j0 N -> neqxT i0 j0 M N.
Proof. Proof.
move=>>; rewrite contra_not_l_equiv -eqxT_not_equiv eqxT_equiv; easy. move=>>; rewrite contra_not_l_equiv -eqxT_not_equiv eqxT_equiv; easy.
Qed. Qed.
Lemma neqxTr_equiv : Lemma neqxTr_equiv :
forall {m n} {i0} {M N : 'E^{m.+1,n}}, forall {m n i0} {M N : 'E^{m.+1,n}},
neqxTr i0 M N <-> skipTr i0 M <> skipTr i0 N. neqxTr i0 M N <-> skipTr i0 M <> skipTr i0 N.
Proof. move=>>; apply neqxF_equiv. Qed. Proof. move=>>; apply neqxF_equiv. Qed.
Lemma neqxTc_equiv : Lemma neqxTc_equiv :
forall {m n} {j0} {M N : 'E^{m,n.+1}}, forall {m n j0} {M N : 'E^{m,n.+1}},
neqxTc j0 M N <-> skipTc j0 M <> skipTc j0 N. neqxTc j0 M N <-> skipTc j0 M <> skipTc j0 N.
Proof. Proof.
intros; split; intros; split;
...@@ -2500,7 +2500,7 @@ intros; split; ...@@ -2500,7 +2500,7 @@ intros; split;
Qed. Qed.
Lemma neqxT_equiv : Lemma neqxT_equiv :
forall {m n} {i0 j0} {M N : 'E^{m.+1,n.+1}}, forall {m n i0 j0} {M N : 'E^{m.+1,n.+1}},
neqxT i0 j0 M N <-> skipT i0 j0 M <> skipT i0 j0 N. neqxT i0 j0 M N <-> skipT i0 j0 M <> skipT i0 j0 N.
Proof. Proof.
intros; split; intros; split;
...@@ -2931,7 +2931,7 @@ rewrite -> 2!replaceTc_correct_r; auto. ...@@ -2931,7 +2931,7 @@ rewrite -> 2!replaceTc_correct_r; auto.
Qed. Qed.
Lemma replaceTr_neqxTr_compat_l : Lemma replaceTr_neqxTr_compat_l :
forall {m n} {i0} A C {M N : 'E^{m,n}}, forall {m n i0} A C {M N : 'E^{m,n}},
neqxTr i0 M N -> replaceTr i0 A M <> replaceTr i0 C N. neqxTr i0 M N -> replaceTr i0 A M <> replaceTr i0 C N.
Proof. move=>>; apply replaceF_neqxF_compat_l. Qed. Proof. move=>>; apply replaceF_neqxF_compat_l. Qed.
...@@ -2941,12 +2941,12 @@ Lemma replaceTr_neqxTr_compat_r : ...@@ -2941,12 +2941,12 @@ Lemma replaceTr_neqxTr_compat_r :
Proof. move=>>; apply replaceF_neqxF_compat_r. Qed. Proof. move=>>; apply replaceF_neqxF_compat_r. Qed.
Lemma replaceTr_neqxTr_reg : Lemma replaceTr_neqxTr_reg :
forall {m n} {i0 A C} {M N : 'E^{m,n}}, forall {m n i0 A C} {M N : 'E^{m,n}},
replaceTr i0 A M <> replaceTr i0 C N -> neqxTr i0 M N \/ A <> C. replaceTr i0 A M <> replaceTr i0 C N -> neqxTr i0 M N \/ A <> C.
Proof. move=>>; apply replaceF_neqxF_reg. Qed. Proof. move=>>; apply replaceF_neqxF_reg. Qed.
Lemma replaceTr_neqxTr_equiv : Lemma replaceTr_neqxTr_equiv :
forall {m n} {i0 A C} {M N : 'E^{m,n}}, forall {m n i0 A C} {M N : 'E^{m,n}},
replaceTr i0 A M <> replaceTr i0 C N <-> neqxTr i0 M N \/ A <> C. replaceTr i0 A M <> replaceTr i0 C N <-> neqxTr i0 M N \/ A <> C.
Proof. Proof.
intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]]; intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]];
...@@ -2954,7 +2954,7 @@ intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]]; ...@@ -2954,7 +2954,7 @@ intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]];
Qed. Qed.
Lemma replaceTc_neqxTc_compat_l : Lemma replaceTc_neqxTc_compat_l :
forall {m n} {j0} B D {M N : 'E^{m,n}}, forall {m n j0} B D {M N : 'E^{m,n}},
neqxTc j0 M N -> replaceTc j0 B M <> replaceTc j0 D N. neqxTc j0 M N -> replaceTc j0 B M <> replaceTc j0 D N.
Proof. Proof.
move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply replaceTc_reg. move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply replaceTc_reg.
...@@ -2966,7 +2966,7 @@ Lemma replaceTc_neqxTc_compat_r : ...@@ -2966,7 +2966,7 @@ Lemma replaceTc_neqxTc_compat_r :
Proof. move=>>; rewrite -contra_equiv; apply replaceTc_reg. Qed. Proof. move=>>; rewrite -contra_equiv; apply replaceTc_reg. Qed.
Lemma replaceTc_neqxTc_reg : Lemma replaceTc_neqxTc_reg :
forall {m n} {j0 B D} {M N : 'E^{m,n}}, forall {m n j0 B D} {M N : 'E^{m,n}},
replaceTc j0 B M <> replaceTc j0 D N -> neqxTc j0 M N \/ B <> D. replaceTc j0 B M <> replaceTc j0 D N -> neqxTc j0 M N \/ B <> D.
Proof. Proof.
move=>>; rewrite neqxTc_not_equiv -not_and_equiv -contra_equiv. move=>>; rewrite neqxTc_not_equiv -not_and_equiv -contra_equiv.
...@@ -2974,7 +2974,7 @@ intros; apply replaceTc_eq; easy. ...@@ -2974,7 +2974,7 @@ intros; apply replaceTc_eq; easy.
Qed. Qed.
Lemma replaceTc_neqxTc_equiv : Lemma replaceTc_neqxTc_equiv :
forall {m n} {j0 B D} {M N : 'E^{m,n}}, forall {m n j0 B D} {M N : 'E^{m,n}},
replaceTc j0 B M <> replaceTc j0 D N <-> neqxTc j0 M N \/ B <> D. replaceTc j0 B M <> replaceTc j0 D N <-> neqxTc j0 M N \/ B <> D.
Proof. Proof.
intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]]; intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]];
...@@ -2982,7 +2982,7 @@ intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]]; ...@@ -2982,7 +2982,7 @@ intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]];
Qed. Qed.
Lemma replaceT_neqxT_compat_l : Lemma replaceT_neqxT_compat_l :
forall {m n} {i0 j0} x y A C B D {M N : 'E^{m,n}}, forall {m n i0 j0} x y A C B D {M N : 'E^{m,n}},
neqxT i0 j0 M N -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N. neqxT i0 j0 M N -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
Proof. Proof.
move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply replaceT_reg. move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply replaceT_reg.
...@@ -2996,7 +2996,7 @@ move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg. ...@@ -2996,7 +2996,7 @@ move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
Qed. Qed.
Lemma replaceT_neqxT_compat_mr : Lemma replaceT_neqxT_compat_mr :
forall {m n} {i0} j0 x y A C {B D} (M N : 'E^{m,n}), forall {m n i0} j0 x y A C {B D} (M N : 'E^{m,n}),
neqxF i0 B D -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N. neqxF i0 B D -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
Proof. Proof.
move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg. move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
...@@ -3008,7 +3008,7 @@ Lemma replaceT_neqxT_compat_r : ...@@ -3008,7 +3008,7 @@ Lemma replaceT_neqxT_compat_r :
Proof. move=>>; rewrite -contra_equiv; apply replaceT_reg. Qed. Proof. move=>>; rewrite -contra_equiv; apply replaceT_reg. Qed.
Lemma replaceT_neqxT_reg : Lemma replaceT_neqxT_reg :
forall {m n} {i0 j0 x y A C B D} {M N : 'E^{m,n}}, forall {m n i0 j0 x y A C B D} {M N : 'E^{m,n}},
replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N ->
neqxT i0 j0 M N \/ neqxF j0 A C \/ neqxF i0 B D \/ x <> y. neqxT i0 j0 M N \/ neqxF j0 A C \/ neqxF i0 B D \/ x <> y.
Proof. Proof.
...@@ -3018,7 +3018,7 @@ intros; apply replaceT_eq; easy. ...@@ -3018,7 +3018,7 @@ intros; apply replaceT_eq; easy.
Qed. Qed.
Lemma replaceT_neqxT_equiv : Lemma replaceT_neqxT_equiv :
forall {m n} {i0 j0 x y A C B D} {M N : 'E^{m,n}}, forall {m n i0 j0 x y A C B D} {M N : 'E^{m,n}},
replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N <-> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N <->
neqxT i0 j0 M N \/ neqxF j0 A C \/ neqxF i0 B D \/ x <> y. neqxT i0 j0 M N \/ neqxF j0 A C \/ neqxF i0 B D \/ x <> y.
Proof. Proof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment