Library Coq.Sets.Permut
We consider a Set U, given with a commutative-associative operator op,
and a congruence cong; we show permutation lemmas
Section Axiomatisation.
Variable U :
Type.
Variable op :
U ->
U ->
U.
Variable cong :
U ->
U ->
Prop.
Hypothesis op_comm :
forall x y:U,
cong (
op x y) (
op y x).
Hypothesis op_ass :
forall x y z:U,
cong (
op (
op x y)
z) (
op x (
op y z)).
Hypothesis cong_left :
forall x y z:U,
cong x y ->
cong (
op x z) (
op y z).
Hypothesis cong_right :
forall x y z:U,
cong x y ->
cong (
op z x) (
op z y).
Hypothesis cong_trans :
forall x y z:U,
cong x y ->
cong y z ->
cong x z.
Hypothesis cong_sym :
forall x y:U,
cong x y ->
cong y x.
Remark. we do not need: Hypothesis cong_refl : (x:U)(cong x x).
Lemma cong_congr :
forall x y z t:U,
cong x y ->
cong z t ->
cong (
op x z) (
op y t).
Lemma comm_right :
forall x y z:U,
cong (
op x (
op y z)) (
op x (
op z y)).
Lemma comm_left :
forall x y z:U,
cong (
op (
op x y)
z) (
op (
op y x)
z).
Lemma perm_right :
forall x y z:U,
cong (
op (
op x y)
z) (
op (
op x z)
y).
Lemma perm_left :
forall x y z:U,
cong (
op x (
op y z)) (
op y (
op x z)).
Lemma op_rotate :
forall x y z t:U,
cong (
op x (
op y z)) (
op z (
op x y)).
Needed for treesort ...
Lemma twist :
forall x y z t:U,
cong (
op x (
op (
op y z)
t)) (
op (
op y (
op x t))
z).
End Axiomatisation.