1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(* Evgeny Makarov, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: NIso.v 10934 2008-05-15 21:58:20Z letouzey $ i*)
15
Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
17
Module NBasePropMod2 := NBasePropFunct NAxiomsMod2.
19
Notation Local N1 := NAxiomsMod1.N.
20
Notation Local N2 := NAxiomsMod2.N.
21
Notation Local Eq1 := NAxiomsMod1.Neq.
22
Notation Local Eq2 := NAxiomsMod2.Neq.
23
Notation Local O1 := NAxiomsMod1.N0.
24
Notation Local O2 := NAxiomsMod2.N0.
25
Notation Local S1 := NAxiomsMod1.S.
26
Notation Local S2 := NAxiomsMod2.S.
27
Notation Local "n == m" := (Eq2 n m) (at level 70, no associativity).
29
Definition homomorphism (f : N1 -> N2) : Prop :=
30
f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n).
32
Definition natural_isomorphism : N1 -> N2 :=
33
NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p).
35
Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd.
37
unfold natural_isomorphism.
39
apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
41
unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
45
Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2.
47
unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0.
50
Theorem natural_isomorphism_succ :
51
forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
53
unfold natural_isomorphism.
54
intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
55
[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
58
Theorem hom_nat_iso : homomorphism natural_isomorphism.
60
unfold homomorphism, natural_isomorphism; split;
61
[exact natural_isomorphism_0 | exact natural_isomorphism_succ].
66
Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
68
Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1.
69
(* This makes the tactic induct available. Since it is taken from
70
(NBasePropFunct NAxiomsMod1), it refers to induction on N1. *)
72
Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
73
Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.
75
Notation Local N1 := NAxiomsMod1.N.
76
Notation Local N2 := NAxiomsMod2.N.
77
Notation Local h12 := Hom12.natural_isomorphism.
78
Notation Local h21 := Hom21.natural_isomorphism.
80
Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity).
82
Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n.
85
now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0.
87
now rewrite Hom12.natural_isomorphism_succ, Hom21.natural_isomorphism_succ, IH.
92
Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig).
94
Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2.
95
Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1.
97
Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2.
98
Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1.
100
Notation Local N1 := NAxiomsMod1.N.
101
Notation Local N2 := NAxiomsMod2.N.
102
Notation Local Eq1 := NAxiomsMod1.Neq.
103
Notation Local Eq2 := NAxiomsMod2.Neq.
104
Notation Local h12 := Hom12.natural_isomorphism.
105
Notation Local h21 := Hom21.natural_isomorphism.
107
Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop :=
108
Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
109
forall n : N1, Eq1 (f2 (f1 n)) n /\
110
forall n : N2, Eq2 (f1 (f2 n)) n.
112
Theorem iso_nat_iso : isomorphism h12 h21.
115
split. apply Hom12.hom_nat_iso.
116
split. apply Hom21.hom_nat_iso.
117
split. apply Inverse12.inverse_nat_iso.
118
apply Inverse21.inverse_nat_iso.