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
.