From 0dd378d82bdfbb04e3510ad7348bc8684aeb1837 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 14 Nov 2023 18:43:21 +0100 Subject: [PATCH] Adding helper functions --- _CoqProject | 1 + examples/peano_bin_nat.v | 16 ++--- theories/Common.v | 127 +++++++++++++++++++++++++++++++++++++++ theories/Trocq.v | 2 +- 4 files changed, 135 insertions(+), 11 deletions(-) create mode 100644 theories/Common.v diff --git a/_CoqProject b/_CoqProject index 9bbdf79..d837e91 100644 --- a/_CoqProject +++ b/_CoqProject @@ -17,6 +17,7 @@ theories/Param_paths.v theories/Param_sigma.v theories/Param_prod.v theories/Param_option.v +theories/Common.v examples/Example.v examples/int_to_Zp.v diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index 798c3e6..e56826e 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -92,7 +92,7 @@ Definition Nsucc (n : N) := Npos (succ_pos n). Definition Nadd (m n : N) := match m, n with | N0, x | x, N0 => x | Npos p, Npos q => Npos (Pos.add p q) -end. +end. Infix "+" := Nadd : N_scope. Notation "n .+1" := (Nsucc n) : N_scope. @@ -107,7 +107,7 @@ Definition Nmap (n : N) : nat := Fixpoint Ncomap (n : nat) : N := match n with O => 0 | S n => Nsucc (Ncomap n) end. -Definition RN@{} (m : N) (n : nat) := paths@{Set} (Ncomap n) m. +Definition RN@{} := sym_rel@{Set} (graph@{Set} Ncomap). Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed. @@ -127,16 +127,12 @@ Proof. by move=> kp; rewrite NcomapD kp Naddpp. Qed. Lemma NmapK (n : N) : Ncomap (Nmap n) = n. Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Qed. -Lemma Nmap_in_R@{} (m : N) (n : nat) : - paths@{Set} (Nmap m) n -> sym_rel@{Set} RN n m. -Proof. by move<-; apply: NmapK. Qed. - (* the best we can do to link these types is (4,4), but we only need (2a,3) which is morally that Nmap is a split injection *) - -Definition RN2a3@{} : Param2a3.Rel@{Set} N nat := @Param2a3.BuildRel@{Set} N nat RN@{} - (@Map2a.BuildHas@{Set} _ _ _ Nmap Nmap_in_R) - (@Map3.BuildHas@{Set} _ _ _ Ncomap (fun _ _ p => p) (fun _ _ p => p)). +Definition RN2a3 : Param2a3.Rel@{Set} N nat := SplitInj.toParamSym@{Set} {| + SplitInj.retract := Ncomap; + SplitInj.section := Nmap; + SplitInj.sectionK := NmapK |}. (* for brevity, we create witnesses at lower classes by forgetting fields in RN2a3 *) (* this behaviour can be automated so as to only declare Rn2a3 and get for free all the instances diff --git a/theories/Common.v b/theories/Common.v new file mode 100644 index 0000000..8c890bd --- /dev/null +++ b/theories/Common.v @@ -0,0 +1,127 @@ +(*****************************************************************************) +(* * Trocq *) +(* _______ * Copyright (C) 2023 MERCE *) +(* |__ __| * (Mitsubishi Electric R&D Centre Europe) *) +(* | |_ __ ___ ___ __ _ * Cyril Cohen *) +(* | | '__/ _ \ / __/ _` | * Enzo Crance *) +(* | | | | (_) | (_| (_| | * Assia Mahboubi *) +(* |_|_| \___/ \___\__, | ************************************************) +(* | | * This file is distributed under the terms of *) +(* |_| * GNU Lesser General Public License Version 3 *) +(* * see LICENSE file for the text of the license *) +(*****************************************************************************) + +Require Import ssreflect. +From elpi Require Export elpi. +From HoTT Require Export HoTT. +From Trocq Require Export + HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param + Param_paths Vernac. + +Definition graph@{i} {A B : Type@{i}} (f : A -> B) := paths o f. + +Module Fun. +Section Fun. +Universe i. +Context {A B : Type@{i}} (f : A -> B) (g : B -> A). +Definition toParam : Param40.Rel@{i} A B := + @Param40.BuildRel A B (graph f) + (@Map4.BuildHas@{i} _ _ _ _ + (fun _ _ => id) (fun _ _ => id) (fun _ _ _ => 1%path)) + (@Map0.BuildHas@{i} _ _ _). + +Definition toParamSym : Param04.Rel@{i} A B := + @Param04.BuildRel A B (sym_rel (graph g)) + (@Map0.BuildHas@{i} _ _ _) + (@Map4.BuildHas@{i} _ _ _ g (fun _ _ => id) (fun _ _ => id) + (fun _ _ _ => 1%path)). +End Fun. +End Fun. + +Module SplitInj. +Section SplitInj. +Universe i. +Context {A B : Type@{i}}. +Record type@{} := { + section :> A -> B; + retract : B -> A; + sectionK : forall x, retract (section x) = x +}. + +Definition fromParam@{} (R : Param2a2b.Rel@{i} A B) := {| + section := map R; + retract := comap R; + sectionK x := R_in_comap R _ _ (map_in_R R _ _ 1%path) +|}. + +Section to. +Variable (f : type). + +Let section_in_retract b a (e : f a = b) : retract f b = a := + transport (fun x => retract f x = a) e (sectionK f a). + +Definition toParam@{} : Param42b.Rel@{i} A B := + @Param42b.BuildRel A B (graph f) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (fun _ _ _ => 1%path)) + (@Map2b.BuildHas@{i} _ _ _ _ section_in_retract). + +Definition toParamSym@{} : Param2a4.Rel@{i} A B := + @Param2a4.BuildRel A B (sym_rel (graph (retract f))) + (@Map2a.BuildHas@{i} _ _ _ _ (fun a b => @section_in_retract b a)) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (fun _ _ _ => 1%path)). +End to. + +End SplitInj. +End SplitInj. + +Module SplitSurj. +Section SplitSurj. +Universe i. +Context {A B : Type@{i}}. +Record type := { + retract :> A -> B; + section : B -> A; + sectionK : forall x, retract (section x) = x +}. + +Definition fromParam@{} (R : Param2b2a.Rel@{i} A B) := {| + retract := map R; + section := comap R; + sectionK x := R_in_map R (comap R x) x (comap_in_R R x (comap R x) 1%path) +|}. + +Section to. +Context (f : type). + +Let section_in_retract b a (e : section f b = a) : f a = b := + transport (fun x => f x = b) e (sectionK f b). + +Definition toParam@{} : Param42a.Rel@{i} A B := + @Param42a.BuildRel A B (graph f) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (fun _ _ _ => 1%path)) + (@Map2a.BuildHas@{i} _ _ _ _ section_in_retract). + +Definition toParamSym@{} : Param2b4.Rel@{i} A B := + @Param2b4.BuildRel A B (sym_rel (graph (section f))) + (@Map2b.BuildHas@{i} _ _ _ _ (fun a b => @section_in_retract b a)) + (@Map4.BuildHas@{i} _ _ _ _ (fun _ _ => id) (fun _ _ => id) + (fun _ _ _ => 1%path)). +End to. + +End SplitSurj. +End SplitSurj. + +Module Equiv. +(* This is exactly adjointify *) +Definition fromParam@{i} {A B : Type@{i}} (R : Param33.Rel@{i} A B) : + A <~> B := {| + equiv_fun := map R; + equiv_isequiv := isequiv_adjointify _ (comap R) + (fun b => R_in_map R _ _ (comap_in_R R _ _ 1%path)) + (fun a => R_in_comap R _ _ (map_in_R R _ _ 1%path)) + |}. + +End Equiv. diff --git a/theories/Trocq.v b/theories/Trocq.v index 86ac72d..2fbbbc0 100644 --- a/theories/Trocq.v +++ b/theories/Trocq.v @@ -15,4 +15,4 @@ From elpi Require Export elpi. From HoTT Require Export HoTT. From Trocq Require Export HoTT_additions Hierarchy Param_Type Param_forall Param_arrow Database Param - Param_paths Vernac. + Param_paths Vernac Common.