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.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   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)         *)
(************************************************************************)

Proofs about standard combinators, exports functional extensionality.

Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - University Paris Sud

Require Import Coq.Program.Basics.
Require Export FunctionalExtensionality.

Open Scope program_scope.

Composition has id for neutral element and is associative.

Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f.forall (A B : Type) (f : A -> B), id ∘ f = f
Proof.forall (A B : Type) (f : A -> B), id ∘ f = f
  intros.A, B:Type
f:A -> B
id ∘ f = f
  reflexivity.
Qed.

Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f.forall (A B : Type) (f : A -> B), f ∘ id = f
Proof.forall (A B : Type) (f : A -> B), f ∘ id = f
  intros.A, B:Type
f:A -> B
f ∘ id = f
  reflexivity.
Qed.

Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D),
  h ∘ g ∘ f = h ∘ (g ∘ f).forall (A B C D : Type) (f : A -> B) (g : B -> C)
  (h : C -> D), h ∘ g ∘ f = h ∘ (g ∘ f)
Proof.forall (A B C D : Type) (f : A -> B) (g : B -> C)
  (h : C -> D), h ∘ g ∘ f = h ∘ (g ∘ f)
  intros.A, B, C, D:Type
f:A -> B
g:B -> C
h:C -> D
h ∘ g ∘ f = h ∘ (g ∘ f)
  reflexivity.
Qed.

Hint Rewrite @compose_id_left @compose_id_right : core.
Hint Rewrite <- @compose_assoc : core.

flip is involutive.

Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id.forall A B C : Type, flip ∘ flip = id
Proof.forall A B C : Type, flip ∘ flip = id
  intros.A, B, C:Type
flip ∘ flip = id
  reflexivity.
Qed.

prod_curry and prod_uncurry are each others inverses.

Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id.forall A B C : Type, prod_uncurry ∘ prod_curry = id
Proof.forall A B C : Type, prod_uncurry ∘ prod_curry = id
  intros.A, B, C:Type
prod_uncurry ∘ prod_curry = id
  reflexivity.
Qed.

Lemma prod_curry_uncurry : forall A B C, @prod_curry A B C ∘ prod_uncurry = id.forall A B C : Type, prod_curry ∘ prod_uncurry = id
Proof.forall A B C : Type, prod_curry ∘ prod_uncurry = id
  simpl ; intros.A, B, C:Type
prod_curry ∘ prod_uncurry = id
  unfold prod_uncurry, prod_curry, compose.A, B, C:Type
(fun (x : A * B -> C) (p : A * B) =>
 let (x0, y) := p in x (x0, y)) = id
  extensionality x ; extensionality p.A, B, C:Type
x:A * B -> C
p:(A * B)%type
(let (x0, y) := p in x (x0, y)) = id x p
  destruct p ; simpl ; reflexivity.
Qed.