Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Fairis
Commits
aead381e
Commit
aead381e
authored
May 30, 2016
by
Jacques-Henri Jourdan
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Csum: sum of two CMRAs
parent
93df90de
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
327 additions
and
0 deletions
+327
-0
_CoqProject
_CoqProject
+1
-0
algebra/csum.v
algebra/csum.v
+326
-0
No files found.
_CoqProject
View file @
aead381e
...
@@ -55,6 +55,7 @@ algebra/upred_tactics.v
...
@@ -55,6 +55,7 @@ algebra/upred_tactics.v
algebra/upred_big_op.v
algebra/upred_big_op.v
algebra/frac.v
algebra/frac.v
algebra/one_shot.v
algebra/one_shot.v
algebra/csum.v
algebra/list.v
algebra/list.v
program_logic/model.v
program_logic/model.v
program_logic/adequacy.v
program_logic/adequacy.v
...
...
algebra/csum.v
0 → 100644
View file @
aead381e
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
upred
.
Local
Arguments
pcore
_
_
!
_
/
.
Local
Arguments
cmra_pcore
_
!
_
/
.
Local
Arguments
validN
_
_
_
!
_
/
.
Local
Arguments
valid
_
_
!
_
/
.
Local
Arguments
cmra_validN
_
_
!
_
/
.
Local
Arguments
cmra_valid
_
!
_
/
.
Inductive
csum
(
A
B
:
Type
)
:=
|
Cinl
:
A
->
csum
A
B
|
Cinr
:
B
->
csum
A
B
|
CsumBot
:
csum
A
B
.
Arguments
Cinl
{
_
_
}
_.
Arguments
Cinr
{
_
_
}
_.
Arguments
CsumBot
{
_
_
}
.
Section
cofe
.
Context
{
A
B
:
cofeT
}
.
Implicit
Types
a
:
A
.
Implicit
Types
b
:
B
.
(
*
Cofe
*
)
Inductive
csum_equiv
:
Equiv
(
csum
A
B
)
:=
|
Cinl_equiv
a
a
'
:
a
≡
a
'
->
Cinl
a
≡
Cinl
a
'
|
Cinlr_equiv
b
b
'
:
b
≡
b
'
->
Cinr
b
≡
Cinr
b
'
|
CsumBot_equiv
:
CsumBot
≡
CsumBot
.
Existing
Instance
csum_equiv
.
Inductive
csum_dist
:
Dist
(
csum
A
B
)
:=
|
Cinl_dist
n
a
a
'
:
a
≡
{
n
}
≡
a
'
->
Cinl
a
≡
{
n
}
≡
Cinl
a
'
|
Cinlr_dist
n
b
b
'
:
b
≡
{
n
}
≡
b
'
->
Cinr
b
≡
{
n
}
≡
Cinr
b
'
|
CsumBot_dist
n
:
CsumBot
≡
{
n
}
≡
CsumBot
.
Existing
Instance
csum_dist
.
Global
Instance
Cinl_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
Cinl
A
B
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
Cinl_proper
:
Proper
((
≡
)
==>
(
≡
))
(
@
Cinl
A
B
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
Cinl_inj
:
Inj
(
≡
)
(
≡
)
(
@
Cinl
A
B
).
Proof
.
by
inversion_clear
1.
Qed
.
Global
Instance
Cinl_inj_dist
n
:
Inj
(
dist
n
)
(
dist
n
)
(
@
Cinl
A
B
).
Proof
.
by
inversion_clear
1.
Qed
.
Global
Instance
Cinr_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
Cinr
A
B
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
Cinr_proper
:
Proper
((
≡
)
==>
(
≡
))
(
@
Cinr
A
B
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
Cinr_inj
:
Inj
(
≡
)
(
≡
)
(
@
Cinr
A
B
).
Proof
.
by
inversion_clear
1.
Qed
.
Global
Instance
Cinr_inj_dist
n
:
Inj
(
dist
n
)
(
dist
n
)
(
@
Cinr
A
B
).
Proof
.
by
inversion_clear
1.
Qed
.
Program
Definition
csum_chain_l
(
c
:
chain
(
csum
A
B
))
(
a
:
A
)
:
chain
A
:=
{|
chain_car
n
:=
match
c
n
return
_
with
Cinl
a
'
=>
a
'
|
_
=>
a
end
|}
.
Next
Obligation
.
intros
c
a
n
i
?
;
simpl
.
by
destruct
(
chain_cauchy
c
n
i
).
Qed
.
Program
Definition
csum_chain_r
(
c
:
chain
(
csum
A
B
))
(
b
:
B
)
:
chain
B
:=
{|
chain_car
n
:=
match
c
n
return
_
with
Cinr
b
'
=>
b
'
|
_
=>
b
end
|}
.
Next
Obligation
.
intros
c
b
n
i
?
;
simpl
.
by
destruct
(
chain_cauchy
c
n
i
).
Qed
.
Instance
csum_compl
:
Compl
(
csum
A
B
)
:=
λ
c
,
match
c
0
with
|
Cinl
a
=>
Cinl
(
compl
(
csum_chain_l
c
a
))
|
Cinr
b
=>
Cinr
(
compl
(
csum_chain_r
c
b
))
|
CsumBot
=>
CsumBot
end
.
Definition
csum_cofe_mixin
:
CofeMixin
(
csum
A
B
).
Proof
.
split
.
-
intros
mx
my
;
split
.
+
by
destruct
1
;
constructor
;
try
apply
equiv_dist
.
+
intros
Hxy
;
feed
inversion
(
Hxy
0
);
subst
;
constructor
;
try
done
;
apply
equiv_dist
=>
n
;
by
feed
inversion
(
Hxy
n
).
-
intros
n
;
split
.
+
by
intros
[
|
a
|
];
constructor
.
+
by
destruct
1
;
constructor
.
+
destruct
1
;
inversion_clear
1
;
constructor
;
etrans
;
eauto
.
-
by
inversion_clear
1
;
constructor
;
apply
dist_S
.
-
intros
n
c
;
rewrite
/
compl
/
csum_compl
.
feed
inversion
(
chain_cauchy
c
0
n
);
first
auto
with
lia
;
constructor
.
+
rewrite
(
conv_compl
n
(
csum_chain_l
c
a
'
))
/=
.
destruct
(
c
n
);
naive_solver
.
+
rewrite
(
conv_compl
n
(
csum_chain_r
c
b
'
))
/=
.
destruct
(
c
n
);
naive_solver
.
Qed
.
Canonical
Structure
csumC
:
cofeT
:=
CofeT
(
csum
A
B
)
csum_cofe_mixin
.
Global
Instance
csum_discrete
:
Discrete
A
→
Discrete
B
→
Discrete
csumC
.
Proof
.
by
inversion_clear
3
;
constructor
;
apply
(
timeless
_
).
Qed
.
Global
Instance
csum_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
B
→
LeibnizEquiv
(
csumC
A
B
).
Proof
.
by
destruct
3
;
f_equal
;
apply
leibniz_equiv
.
Qed
.
Global
Instance
Cinl_timeless
a
:
Timeless
a
→
Timeless
(
Cinl
a
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
timeless
_
).
Qed
.
Global
Instance
Cinr_timeless
b
:
Timeless
b
→
Timeless
(
Cinr
b
).
Proof
.
by
inversion_clear
2
;
constructor
;
apply
(
timeless
_
).
Qed
.
End
cofe
.
Arguments
csumC
:
clear
implicits
.
(
*
Functor
on
COFEs
*
)
Definition
csum_map
{
A
A
'
B
B
'
}
(
fA
:
A
→
A
'
)
(
fB
:
B
→
B
'
)
(
x
:
csum
A
B
)
:
csum
A
'
B
'
:=
match
x
with
|
Cinl
a
=>
Cinl
(
fA
a
)
|
Cinr
b
=>
Cinr
(
fB
b
)
|
CsumBot
=>
CsumBot
end
.
Instance:
Params
(
@
csum_map
)
4.
Lemma
csum_map_id
{
A
B
}
(
x
:
csum
A
B
)
:
csum_map
id
id
x
=
x
.
Proof
.
by
destruct
x
.
Qed
.
Lemma
csum_map_compose
{
A
A
'
A
''
B
B
'
B
''
}
(
f
:
A
→
A
'
)
(
f
'
:
A
'
→
A
''
)
(
g
:
B
→
B
'
)
(
g
'
:
B
'
→
B
''
)
(
x
:
csum
A
B
)
:
csum_map
(
f
'
∘
f
)
(
g
'
∘
g
)
x
=
csum_map
f
'
g
'
(
csum_map
f
g
x
).
Proof
.
by
destruct
x
.
Qed
.
Lemma
csum_map_ext
{
A
A
'
B
B
'
:
cofeT
}
(
f
f
'
:
A
→
A
'
)
(
g
g
'
:
B
→
B
'
)
x
:
(
∀
x
,
f
x
≡
f
'
x
)
→
(
∀
x
,
g
x
≡
g
'
x
)
→
csum_map
f
g
x
≡
csum_map
f
'
g
'
x
.
Proof
.
by
destruct
x
;
constructor
.
Qed
.
Instance
csum_map_cmra_ne
{
A
A
'
B
B
'
:
cofeT
}
n
:
Proper
((
dist
n
==>
dist
n
)
==>
(
dist
n
==>
dist
n
)
==>
dist
n
==>
dist
n
)
(
@
csum_map
A
A
'
B
B
'
).
Proof
.
intros
f
f
'
Hf
g
g
'
Hg
[];
destruct
1
;
constructor
;
by
apply
Hf
||
apply
Hg
.
Qed
.
Definition
csumC_map
{
A
A
'
B
B
'
}
(
f
:
A
-
n
>
A
'
)
(
g
:
B
-
n
>
B
'
)
:
csumC
A
B
-
n
>
csumC
A
'
B
'
:=
CofeMor
(
csum_map
f
g
).
Instance
csumC_map_ne
A
A
'
B
B
'
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(
@
csumC_map
A
A
'
B
B
'
).
Proof
.
by
intros
f
f
'
Hf
g
g
'
Hg
[];
constructor
.
Qed
.
Section
cmra
.
Context
{
A
B
:
cmraT
}
.
Implicit
Types
a
:
A
.
Implicit
Types
b
:
B
.
(
*
CMRA
*
)
Instance
csum_valid
:
Valid
(
csum
A
B
)
:=
λ
x
,
match
x
with
|
Cinl
a
=>
✓
a
|
Cinr
b
=>
✓
b
|
CsumBot
=>
False
end
.
Instance
csum_validN
:
ValidN
(
csum
A
B
)
:=
λ
n
x
,
match
x
with
|
Cinl
a
=>
✓
{
n
}
a
|
Cinr
b
=>
✓
{
n
}
b
|
CsumBot
=>
False
end
.
Instance
csum_pcore
:
PCore
(
csum
A
B
)
:=
λ
x
,
match
x
with
|
Cinl
a
=>
Cinl
<
$
>
pcore
a
|
Cinr
b
=>
Cinr
<
$
>
pcore
b
|
CsumBot
=>
Some
CsumBot
end
.
Instance
csum_op
:
Op
(
csum
A
B
)
:=
λ
x
y
,
match
x
,
y
with
|
Cinl
a
,
Cinl
a
'
=>
Cinl
(
a
⋅
a
'
)
|
Cinr
b
,
Cinr
b
'
=>
Cinr
(
b
⋅
b
'
)
|
_
,
_
=>
CsumBot
end
.
Lemma
Cinl_op
a
a
'
:
Cinl
a
⋅
Cinl
a
'
=
Cinl
(
a
⋅
a
'
).
Proof
.
done
.
Qed
.
Lemma
Cinr_op
b
b
'
:
Cinr
b
⋅
Cinr
b
'
=
Cinr
(
b
⋅
b
'
).
Proof
.
done
.
Qed
.
Lemma
csum_included
x
y
:
x
≼
y
↔
y
=
CsumBot
∨
(
∃
a
a
'
,
x
=
Cinl
a
∧
y
=
Cinl
a
'
∧
a
≼
a
'
)
∨
(
∃
b
b
'
,
x
=
Cinr
b
∧
y
=
Cinr
b
'
∧
b
≼
b
'
).
Proof
.
split
.
-
intros
[
z
Hy
];
destruct
x
as
[
a
|
b
|
],
z
as
[
a
'
|
b
'
|
];
inversion_clear
Hy
;
auto
.
+
right
;
left
;
eexists
_
,
_
;
split_and
!
;
eauto
.
eexists
;
eauto
.
+
right
;
right
;
eexists
_
,
_
;
split_and
!
;
eauto
.
eexists
;
eauto
.
-
intros
[
->|
[(
a
&
a
'
&->&->&
c
&?
)
|
(
b
&
b
'
&->&->&
c
&?
)]].
+
destruct
x
;
exists
CsumBot
;
constructor
.
+
exists
(
Cinl
c
);
by
constructor
.
+
exists
(
Cinr
c
);
by
constructor
.
Qed
.
Lemma
csum_cmra_mixin
:
CMRAMixin
(
csum
A
B
).
Proof
.
split
.
-
intros
n
[];
destruct
1
;
constructor
;
by
cofe_subst
.
-
intros
????
[
n
a
a
'
Ha
|
n
b
b
'
Hb
|
n
]
[
=
];
subst
;
eauto
.
+
destruct
(
pcore
a
)
as
[
ca
|
]
eqn
:?
;
simplify_option_eq
.
destruct
(
cmra_pcore_ne
n
a
a
'
ca
)
as
(
ca
'
&->&?
);
auto
.
exists
(
Cinl
ca
'
);
by
repeat
constructor
.
+
destruct
(
pcore
b
)
as
[
cb
|
]
eqn
:?
;
simplify_option_eq
.
destruct
(
cmra_pcore_ne
n
b
b
'
cb
)
as
(
cb
'
&->&?
);
auto
.
exists
(
Cinr
cb
'
);
by
repeat
constructor
.
-
intros
?
[
a
|
b
|
]
[
a
'
|
b
'
|
]
H
;
inversion_clear
H
;
cofe_subst
;
done
.
-
intros
[
a
|
b
|
];
rewrite
/=
?
cmra_valid_validN
;
naive_solver
eauto
using
O
.
-
intros
n
[
a
|
b
|
];
simpl
;
auto
using
cmra_validN_S
.
-
intros
[
a1
|
b1
|
]
[
a2
|
b2
|
]
[
a3
|
b3
|
];
constructor
;
by
rewrite
?
assoc
.
-
intros
[
a1
|
b1
|
]
[
a2
|
b2
|
];
constructor
;
by
rewrite
1
?
comm
.
-
intros
[
a
|
b
|
]
?
[
=
];
subst
;
auto
.
+
destruct
(
pcore
a
)
as
[
ca
|
]
eqn
:?
;
simplify_option_eq
.
constructor
;
eauto
using
cmra_pcore_l
.
+
destruct
(
pcore
b
)
as
[
cb
|
]
eqn
:?
;
simplify_option_eq
.
constructor
;
eauto
using
cmra_pcore_l
.
-
intros
[
a
|
b
|
]
?
[
=
];
subst
;
auto
.
+
destruct
(
pcore
a
)
as
[
ca
|
]
eqn
:?
;
simplify_option_eq
.
feed
inversion
(
cmra_pcore_idemp
a
ca
);
repeat
constructor
;
auto
.
+
destruct
(
pcore
b
)
as
[
cb
|
]
eqn
:?
;
simplify_option_eq
.
feed
inversion
(
cmra_pcore_idemp
b
cb
);
repeat
constructor
;
auto
.
-
intros
x
y
?
[
->|
[(
a
&
a
'
&->&->&?
)
|
(
b
&
b
'
&->&->&?
)]]
%
csum_included
[
=
].
+
exists
CsumBot
.
rewrite
csum_included
;
eauto
.
+
destruct
(
pcore
a
)
as
[
ca
|
]
eqn
:?
;
simplify_option_eq
.
destruct
(
cmra_pcore_preserving
a
a
'
ca
)
as
(
ca
'
&->&?
);
auto
.
exists
(
Cinl
ca
'
).
rewrite
csum_included
;
eauto
10.
+
destruct
(
pcore
b
)
as
[
cb
|
]
eqn
:?
;
simplify_option_eq
.
destruct
(
cmra_pcore_preserving
b
b
'
cb
)
as
(
cb
'
&->&?
);
auto
.
exists
(
Cinr
cb
'
).
rewrite
csum_included
;
eauto
10.
-
intros
n
[
a1
|
b1
|
]
[
a2
|
b2
|
];
simpl
;
eauto
using
cmra_validN_op_l
;
done
.
-
intros
n
[
a
|
b
|
]
y1
y2
Hx
Hx
'
.
+
destruct
y1
as
[
a1
|
b1
|
],
y2
as
[
a2
|
b2
|
];
try
(
exfalso
;
by
inversion_clear
Hx
'
).
apply
(
inj
Cinl
)
in
Hx
'
.
destruct
(
cmra_extend
n
a
a1
a2
)
as
([
z1
z2
]
&?&?&?
);
auto
.
exists
(
Cinl
z1
,
Cinl
z2
).
by
repeat
constructor
.
+
destruct
y1
as
[
a1
|
b1
|
],
y2
as
[
a2
|
b2
|
];
try
(
exfalso
;
by
inversion_clear
Hx
'
).
apply
(
inj
Cinr
)
in
Hx
'
.
destruct
(
cmra_extend
n
b
b1
b2
)
as
([
z1
z2
]
&?&?&?
);
auto
.
exists
(
Cinr
z1
,
Cinr
z2
).
by
repeat
constructor
.
+
by
exists
(
CsumBot
,
CsumBot
);
destruct
y1
,
y2
;
inversion_clear
Hx
'
.
Qed
.
Canonical
Structure
csumR
:=
CMRAT
(
csum
A
B
)
csum_cofe_mixin
csum_cmra_mixin
.
Global
Instance
csum_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
B
→
CMRADiscrete
csumR
.
Proof
.
split
;
first
apply
_.
by
move
=>
[
a
|
b
|
]
HH
/=
;
try
apply
cmra_discrete_valid
.
Qed
.
Global
Instance
Cinl_persistent
a
:
Persistent
a
→
Persistent
(
Cinl
a
).
Proof
.
rewrite
/
Persistent
/=
.
inversion_clear
1
;
by
repeat
constructor
.
Qed
.
Global
Instance
Cinr_persistent
b
:
Persistent
b
→
Persistent
(
Cinr
b
).
Proof
.
rewrite
/
Persistent
/=
.
inversion_clear
1
;
by
repeat
constructor
.
Qed
.
(
**
Internalized
properties
*
)
Lemma
csum_equivI
{
M
}
(
x
y
:
csum
A
B
)
:
(
x
≡
y
)
⊣⊢
(
match
x
,
y
with
|
Cinl
a
,
Cinl
a
'
=>
a
≡
a
'
|
Cinr
b
,
Cinr
b
'
=>
b
≡
b
'
|
CsumBot
,
CsumBot
=>
True
|
_
,
_
=>
False
end
:
uPred
M
).
Proof
.
uPred
.
unseal
;
do
2
split
;
first
by
destruct
1.
by
destruct
x
,
y
;
try
destruct
1
;
try
constructor
.
Qed
.
Lemma
csum_validI
{
M
}
(
x
:
csum
A
B
)
:
(
✓
x
)
⊣⊢
(
match
x
with
|
Cinl
a
=>
✓
a
|
Cinr
b
=>
✓
b
|
CsumBot
=>
False
end
:
uPred
M
).
Proof
.
uPred
.
unseal
.
by
destruct
x
.
Qed
.
(
**
Updates
*
)
Lemma
csum_update_l
(
a1
a2
:
A
)
:
a1
~~>
a2
→
Cinl
a1
~~>
Cinl
a2
.
Proof
.
intros
Ha
n
[[
a
|
b
|
]
|
]
?
;
simpl
in
*
;
auto
.
-
by
apply
(
Ha
n
(
Some
a
)).
-
by
apply
(
Ha
n
None
).
Qed
.
Lemma
csum_update_r
(
b1
b2
:
B
)
:
b1
~~>
b2
→
Cinr
b1
~~>
Cinr
b2
.
Proof
.
intros
Hb
n
[[
a
|
b
|
]
|
]
?
;
simpl
in
*
;
auto
.
-
by
apply
(
Hb
n
(
Some
b
)).
-
by
apply
(
Hb
n
None
).
Qed
.
Lemma
csum_updateP_l
(
P
:
A
→
Prop
)
(
Q
:
csum
A
B
→
Prop
)
a
:
a
~~>:
P
→
(
∀
a
'
,
P
a
'
→
Q
(
Cinl
a
'
))
→
Cinl
a
~~>:
Q
.
Proof
.
intros
Hx
HP
n
mf
Hm
.
destruct
mf
as
[[
a
'
|
b
'
|
]
|
];
try
by
destruct
Hm
.
-
destruct
(
Hx
n
(
Some
a
'
))
as
(
c
&?&?
);
naive_solver
.
-
destruct
(
Hx
n
None
)
as
(
c
&?&?
);
naive_solver
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
csum_updateP_r
(
P
:
B
→
Prop
)
(
Q
:
csum
A
B
→
Prop
)
b
:
b
~~>:
P
→
(
∀
b
'
,
P
b
'
→
Q
(
Cinr
b
'
))
→
Cinr
b
~~>:
Q
.
Proof
.
intros
Hx
HP
n
mf
Hm
.
destruct
mf
as
[[
a
'
|
b
'
|
]
|
];
try
by
destruct
Hm
.
-
destruct
(
Hx
n
(
Some
b
'
))
as
(
c
&?&?
);
naive_solver
.
-
destruct
(
Hx
n
None
)
as
(
c
&?&?
);
naive_solver
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
csum_updateP
'_
l
(
P
:
A
→
Prop
)
a
:
a
~~>:
P
→
Cinl
a
~~>:
λ
m
'
,
∃
a
'
,
m
'
=
Cinl
a
'
∧
P
a
'
.
Proof
.
eauto
using
csum_updateP_l
.
Qed
.
Lemma
csum_updateP
'_
r
(
P
:
B
→
Prop
)
b
:
b
~~>:
P
→
Cinr
b
~~>:
λ
m
'
,
∃
b
'
,
m
'
=
Cinr
b
'
∧
P
b
'
.
Proof
.
eauto
using
csum_updateP_r
.
Qed
.
End
cmra
.
Arguments
csumR
:
clear
implicits
.
(
*
Functor
*
)
Instance
csum_map_cmra_monotone
{
A
A
'
B
B
'
:
cmraT
}
(
f
:
A
→
A
'
)
(
g
:
B
→
B
'
)
:
CMRAMonotone
f
→
CMRAMonotone
g
→
CMRAMonotone
(
csum_map
f
g
).
Proof
.
split
;
try
apply
_.
-
intros
n
[
a
|
b
|
];
simpl
;
auto
using
validN_preserving
.
-
intros
x
y
;
rewrite
!
csum_included
.
intros
[
->|
[(
a
&
a
'
&->&->&?
)
|
(
b
&
b
'
&->&->&?
)]];
simpl
;
eauto
10
using
included_preserving
.
Qed
.
Program
Definition
csumRF
(
Fa
Fb
:
rFunctor
)
:
rFunctor
:=
{|
rFunctor_car
A
B
:=
csumR
(
rFunctor_car
Fa
A
B
)
(
rFunctor_car
Fb
A
B
);
rFunctor_map
A1
A2
B1
B2
fg
:=
csumC_map
(
rFunctor_map
Fa
fg
)
(
rFunctor_map
Fb
fg
)
|}
.
Next
Obligation
.
by
intros
Fa
Fb
A1
A2
B1
B2
n
f
g
Hfg
;
apply
csumC_map_ne
;
try
apply
rFunctor_ne
.
Qed
.
Next
Obligation
.
intros
Fa
Fb
A
B
x
.
rewrite
/=
-{
2
}
(
csum_map_id
x
).
apply
csum_map_ext
=>
y
;
apply
rFunctor_id
.
Qed
.
Next
Obligation
.
intros
Fa
Fb
A1
A2
A3
B1
B2
B3
f
g
f
'
g
'
x
.
rewrite
/=
-
csum_map_compose
.
apply
csum_map_ext
=>
y
;
apply
rFunctor_compose
.
Qed
.
Instance
csumRF_contractive
Fa
Fb
:
rFunctorContractive
Fa
→
rFunctorContractive
Fb
→
rFunctorContractive
(
csumRF
Fa
Fb
).
Proof
.
by
intros
??
A1
A2
B1
B2
n
f
g
Hfg
;
apply
csumC_map_ne
;
try
apply
rFunctor_contractive
.
Qed
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment