NIso.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Import NBase.

Module Homomorphism (N1 N2 : NAxiomsRecSig).

Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity).

Definition homomorphism (f : N1.t -> N2.t) : Prop :=
  f N1.zero == N2.zero /\ forall n, f (N1.succ n) == N2.succ (f n).

Definition natural_isomorphism : N1.t -> N2.t :=
  N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.succ p).

Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism.Proper (N1.eq ==> N2.eq) natural_isomorphism
Proof.Proper (N1.eq ==> N2.eq) natural_isomorphism
unfold natural_isomorphism.Proper (N1.eq ==> N2.eq)
  (N1.recursion N2.zero
     (fun (_ : N1.t) (p : N2.t) => N2.succ p))
repeat red; intros.x, y:N1.t
H:N1.eq x y
N1.recursion N2.zero
  (fun (_ : N1.t) (p : N2.t) => N2.succ p) x ==
N1.recursion N2.zero
  (fun (_ : N1.t) (p : N2.t) => N2.succ p) y f_equiv; trivial.x, y:N1.t
H:N1.eq x y
(N1.eq ==> N2.eq ==> N2.eq)%signature
  (fun (_ : N1.t) (p : N2.t) => N2.succ p)
  (fun (_ : N1.t) (p : N2.t) => N2.succ p)
repeat red; intros.x, y:N1.t
H:N1.eq x y
x0, y0:N1.t
H0:N1.eq x0 y0
x1, y1:N2.t
H1:x1 == y1
N2.succ x1 == N2.succ y1 now f_equiv.
Qed.

Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero.natural_isomorphism N1.zero == N2.zero
Proof.natural_isomorphism N1.zero == N2.zero
unfold natural_isomorphism; now rewrite N1.recursion_0.
Qed.

Theorem natural_isomorphism_succ :
  forall n : N1.t, natural_isomorphism (N1.succ n) == N2.succ (natural_isomorphism n).forall n : N1.t,
natural_isomorphism (N1.succ n) ==
N2.succ (natural_isomorphism n)
Proof.forall n : N1.t,
natural_isomorphism (N1.succ n) ==
N2.succ (natural_isomorphism n)
unfold natural_isomorphism.forall n : N1.t,
N1.recursion N2.zero
  (fun (_ : N1.t) (p : N2.t) => N2.succ p) (N1.succ n) ==
N2.succ
  (N1.recursion N2.zero
     (fun (_ : N1.t) (p : N2.t) => N2.succ p) n)
intro n.n:N1.t
N1.recursion N2.zero
  (fun (_ : N1.t) (p : N2.t) => N2.succ p) (N1.succ n) ==
N2.succ
  (N1.recursion N2.zero
     (fun (_ : N1.t) (p : N2.t) => N2.succ p) n) rewrite N1.recursion_succ; auto with *.n:N1.t
Proper (N1.eq ==> N2.eq ==> N2.eq)
  (fun (_ : N1.t) (p : N2.t) => N2.succ p)
repeat red; intros.n, x, y:N1.t
H:N1.eq x y
x0, y0:N2.t
H0:x0 == y0
N2.succ x0 == N2.succ y0 now f_equiv.
Qed.

Theorem hom_nat_iso : homomorphism natural_isomorphism.homomorphism natural_isomorphism
Proof.homomorphism natural_isomorphism
unfold homomorphism, natural_isomorphism; split;
[exact natural_isomorphism_0 | exact natural_isomorphism_succ].
Qed.

End Homomorphism.

Module Inverse (N1 N2 : NAxiomsRecSig).

Module Import NBasePropMod1 := NBaseProp N1.
(* This makes the tactic induct available. Since it is taken from
(NBasePropFunct NAxiomsMod1), it refers to induction on N1. *)

Module Hom12 := Homomorphism N1 N2.
Module Hom21 := Homomorphism N2 N1.

Notation h12 := Hom12.natural_isomorphism.
Notation h21 := Hom21.natural_isomorphism.
Local Notation "n == m" := (N1.eq n m) (at level 70, no associativity).

Lemma inverse_nat_iso : forall n : N1.t, h21 (h12 n) == n.forall n : N1.t, h21 (h12 n) == n
Proof.forall n : N1.t, h21 (h12 n) == n
induct n.h21 (h12 N1.zero) == N1.zero
forall n : N1.t,
h21 (h12 n) == n -> h21 (h12 (N1.succ n)) == N1.succ n
now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0.forall n : N1.t,
h21 (h12 n) == n -> h21 (h12 (N1.succ n)) == N1.succ n
intros n IH.n:N1.t
IH:h21 (h12 n) == n
h21 (h12 (N1.succ n)) == N1.succ n
now rewrite Hom12.natural_isomorphism_succ, Hom21.natural_isomorphism_succ, IH.
Qed.

End Inverse.

Module Isomorphism (N1 N2 : NAxiomsRecSig).

Module Hom12 := Homomorphism N1 N2.
Module Hom21 := Homomorphism N2 N1.
Module Inverse12 := Inverse N1 N2.
Module Inverse21 := Inverse N2 N1.

Notation h12 := Hom12.natural_isomorphism.
Notation h21 := Hom21.natural_isomorphism.

Definition isomorphism (f1 : N1.t -> N2.t) (f2 : N2.t -> N1.t) : Prop :=
  Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\
  forall n, N1.eq (f2 (f1 n)) n /\
  forall n, N2.eq (f1 (f2 n)) n.

Theorem iso_nat_iso : isomorphism h12 h21.isomorphism h12 h21
Proof.isomorphism h12 h21
unfold isomorphism.Hom12.homomorphism h12 /\
Hom21.homomorphism h21 /\
(forall n : N1.t,
 N1.eq (h21 (h12 n)) n /\
 (forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0))
split.Hom12.homomorphism h12
Hom21.homomorphism h21 /\
(forall n : N1.t,
 N1.eq (h21 (h12 n)) n /\
 (forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0)) apply Hom12.hom_nat_iso.Hom21.homomorphism h21 /\
(forall n : N1.t,
 N1.eq (h21 (h12 n)) n /\
 (forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0))
split.Hom21.homomorphism h21
forall n : N1.t,
N1.eq (h21 (h12 n)) n /\
(forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0) apply Hom21.hom_nat_iso.forall n : N1.t,
N1.eq (h21 (h12 n)) n /\
(forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0)
split.n:N1.t
N1.eq (h21 (h12 n)) n
n:N1.t
forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0 apply Inverse12.inverse_nat_iso.n:N1.t
forall n0 : N2.t, N2.eq (h12 (h21 n0)) n0
apply Inverse21.inverse_nat_iso.
Qed.

End Isomorphism.