- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
Lemma mfun_equiv_commut f g g1 g2 :
mfun_equiv g (g2 ∘ g1) ->
commute f g1 ->
commute f g2 ->
commute f g.
Proof.
intros Hg Hcomm_g1 Hcomm_g2 a z.
split; intros H; unfold mfun_equiv in Hg.
- destruct H as [b [Hb Hz]].
rewrite Hg in Hz.
destruct Hz as [d [Hd Hz]].
destruct (Hcomm_g1 a d) as [Hg1f Hfg1]. clear Hfg1.
destruct Hg1f as [d' [Had' Hcd']]. { sauto. }
morph_shift g2 d'.
destruct Had' as [c' Hc'].
destruct (Hcomm_g2 c' z') as [Hg2f Hfg2].
destruct Hg2f as [z'' [Hz'' Hz'z'']]. { sauto. }
destruct Hz'' as [e'' He''].
exists z''.
split.
+ exists e''.
split.
* rewrite Hg. sauto.
* easy.
+ now rewrite Hequiv_z_z', Hz'z''.
- destruct H as [c [Hc Hz]].
rewrite Hg in Hc.
destruct Hc as [b [Hb Hc]].
destruct (Hcomm_g2 b z) as [Hg2f Hfg2]. clear Hg2f.
destruct Hfg2 as [z' [Hbz' Hzz']]. { sauto. }
destruct Hbz' as [d [Hdz' Hbd']].
destruct (Hcomm_g1 a d) as [Hg1f Hfg1]. clear Hg1f.
destruct Hfg1 as [d' [Had' Hdd']]. { sauto. }
destruct Had' as [b' [Hab' Hb'd']].
morph_shift g2 d'.
exists z''.
split.
+ exists b'.
split.
* easy.
* rewrite Hg. exists d'. sauto.
+ now rewrite Hzz', Hequiv_z'_z''.
Qed.
Follow us!