diff --git a/_CoqProject b/_CoqProject index 616b59e..12de94b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,6 +3,7 @@ -R theories/ Trocq -R elpi/ Trocq.Elpi +-R examples/ Trocq_examples theories/HoTT_additions.v theories/Hierarchy.v @@ -23,10 +24,12 @@ theories/Param_prod.v theories/Param_option.v theories/Param_vector.v -examples/Example.v +examples/artifact_paper_example.v +examples/N.v examples/int_to_Zp.v examples/peano_bin_nat.v examples/setoid_rewrite.v examples/summable.v examples/trocq_setoid_rewrite.v examples/Vector_tuple.v +examples/misc.v diff --git a/examples/N.v b/examples/N.v new file mode 100644 index 0000000..45a2f5a --- /dev/null +++ b/examples/N.v @@ -0,0 +1,134 @@ +(*****************************************************************************) +(* * 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 *) +(*****************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Common. + +Set Universe Polymorphism. + +(* definition of binary natural numbers *) + +Inductive positive : Set := + | xI : positive -> positive + | xO : positive -> positive + | xH : positive. + +Declare Scope positive_scope. +Delimit Scope positive_scope with positive. +Bind Scope positive_scope with positive. + +Notation "1" := xH : positive_scope. +Notation "p ~ 1" := (xI p) + (at level 7, left associativity, format "p '~' '1'") : positive_scope. +Notation "p ~ 0" := (xO p) + (at level 7, left associativity, format "p '~' '0'") : positive_scope. + +Module Pos. +Local Open Scope positive_scope. +Fixpoint succ x := + match x with + | p~1 => (succ p)~0 + | p~0 => p~1 + | 1 => 1~0 + end. + +Fixpoint map (x : positive) : nat := + match x with + | p~1 => 1 + (map p + map p) + | p~0 => map p + map p + | 1 => 1 + end. + +Fixpoint add (x y : positive) : positive := + match x, y with + | 1, p | p, 1 => succ p + | p~0, q~0 => (add p q)~0 + | p~0, q~1 | p~1, q~0 => (add p q)~1 + | p~1, q~1 => succ (add p q)~1 + end. +Infix "+" := add : positive_scope. +Notation "p .+1" := (succ p) : positive_scope. + +Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Defined. +Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Defined. +Lemma addpS x y : x + y.+1 = (x + y).+1. +Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Defined. +Lemma addSp x y : x.+1 + y = (x + y).+1. +Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Defined. + +End Pos. +Infix "+" := Pos.add : positive_scope. +Notation "p .+1" := (Pos.succ p) : positive_scope. + +Inductive N : Set := + | N0 : N + | Npos : positive -> N. + +Declare Scope N_scope. +Delimit Scope N_scope with N. +Bind Scope N_scope with N. + +Notation "0" := N0 : N_scope. + +Definition succ_pos (n : N) : positive := + match n with + | N0 => 1%positive + | Npos p => Pos.succ p + end. + +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. +Infix "+" := Nadd : N_scope. +Notation "n .+1" := (Nsucc n) : N_scope. + +(* various possible proofs to fill the fields of a parametricity witness between N and nat *) + +Definition Nmap (n : N) : nat := + match n with + | N0 => 0 + | Npos p => Pos.map p + end. + +Fixpoint Ncomap (n : nat) : N := + match n with O => 0 | S n => Nsucc (Ncomap n) end. + +Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. +Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Defined. + +Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N. +Proof. +elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//. +rewrite -nat_add_n_Sm/= IHi. +case: (Ncomap i) => // p; case: (Ncomap j) => //=. +- by rewrite /Nsucc/= Pos.addp1. +- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp. +Defined. + +Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0. +Proof. by move=> kp; rewrite NcomapD kp Naddpp. Defined. + +Lemma NmapK (n : N) : Ncomap (Nmap n) = n. +Proof. by case: n => //= ; elim=> //= p /NcomapNpos/= ->. Defined. + +Lemma NcomapK (n : nat) : Nmap (Ncomap n) = n. +Proof. +elim: n => //= n IHn; rewrite -[in X in _ = X]IHn. +by case: (Ncomap n)=> //; elim=> //= p ->; rewrite /= !add_n_Sm. +Defined. + +Definition Niso := Iso.Build NcomapK NmapK. \ No newline at end of file diff --git a/examples/artifact_paper_example.v b/examples/artifact_paper_example.v new file mode 100644 index 0000000..906cd9d --- /dev/null +++ b/examples/artifact_paper_example.v @@ -0,0 +1,46 @@ +(*****************************************************************************) +(* * 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 *) +(*****************************************************************************) + +From Coq Require Import ssreflect. +From HoTT Require Import HoTT. +From Trocq Require Import Trocq. +From Trocq_examples Require Import N. + +Set Universe Polymorphism. + +(* Let us first prove that type nat , of unary natural numbers, and type N , of +binary ones, are equivalent *) +Definition RN44 : (N <=> nat)%P := Iso.toParamSym Niso. + +(* This equivalence proof coerces to a relation of type N -> nat -> Type , which +relates the respective zero and successor constants of these types: *) +Definition RN0 : RN44 0%N 0%nat. Proof. done. Defined. +Definition RNS : forall m n, RN44 m n -> RN44 (Nsucc m) (S n). +Proof. by move=> _ + <-; case=> //=. Defined. + +(* We now register all these informations in a database known to the tactic: *) +Trocq Use RN0. Trocq Use RNS. +Trocq Use RN44. + +(* We can now make use of the tactic to prove a recurrence principle on N *) +Lemma N_Srec : forall (P : N -> Type), P N0 -> + (forall n, P n -> P (Nsucc n)) -> forall n, P n. +Proof. trocq. (* N replaces nat in the goal *) exact nat_rect. Defined. + +(* Inspecting the proof term atually reveals that univalence was not needed +in the proof of N_Srec. *) +Print N_Srec. +Print Assumptions N_Srec. + +(* Indeed this computes *) +Eval compute in N_Srec (fun n => N) (0%N) Nadd (Npos 1~0~1~1~1~0). diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v index 3c30d1a..6b74cf7 100644 --- a/examples/int_to_Zp.v +++ b/examples/int_to_Zp.v @@ -52,8 +52,7 @@ Notation "x * y" := (mulp x%Zmodp y%Zmodp) : Zmodp_scope. Module IntToZmodp. -Definition Rp := SplitSurj.toParam - (SplitSurj.Build_type modp reprp reprpK). +Definition Rp := SplitSurj.toParam (SplitSurj.Build reprpK). Axiom Rzero' : Rp zero zerop. Variable Radd' : binop_param Rp Rp Rp add addp. @@ -88,25 +87,13 @@ End IntToZmodp. Module ZmodpToInt. -Definition Rp x n := eqmodp (reprp x) n. - -Definition Rp2a2b@{i} : Param2a2b.Rel Zmodp@{i} int@{i}. -Proof. -unshelve econstructor. -- exact Rp. -- unshelve econstructor. - + exact reprp. - + move=> a b; move=> /(ap modp); exact. -- unshelve econstructor. - + exact modp. - + by move=> a b; rewrite /Rp/sym_rel/eqmodp reprpK => <-. -Defined. +Definition Rp := SplitSurj.toParamSym (SplitSurj.Build reprpK). Axiom Rzero : Rp zerop zero. Variable Radd : binop_param Rp Rp Rp addp add. Variable paths_to_eqmodp : binop_param Rp Rp iff paths eqmodp. -Trocq Use Rp2a2b. +Trocq Use Rp. Trocq Use Param01_paths. Trocq Use Param10_paths. Trocq Use Radd. diff --git a/examples/Example.v b/examples/misc.v similarity index 100% rename from examples/Example.v rename to examples/misc.v diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v index 947060e..6cddc28 100644 --- a/examples/peano_bin_nat.v +++ b/examples/peano_bin_nat.v @@ -14,117 +14,10 @@ From Coq Require Import ssreflect. From HoTT Require Import HoTT. From Trocq Require Import Trocq. +From Trocq_examples Require Import N. Set Universe Polymorphism. -(* definition of binary natural numbers *) - -Inductive positive : Set := - | xI : positive -> positive - | xO : positive -> positive - | xH : positive. - -Declare Scope positive_scope. -Delimit Scope positive_scope with positive. -Bind Scope positive_scope with positive. - -Notation "1" := xH : positive_scope. -Notation "p ~ 1" := (xI p) - (at level 7, left associativity, format "p '~' '1'") : positive_scope. -Notation "p ~ 0" := (xO p) - (at level 7, left associativity, format "p '~' '0'") : positive_scope. - -Module Pos. -Local Open Scope positive_scope. -Fixpoint succ x := - match x with - | p~1 => (succ p)~0 - | p~0 => p~1 - | 1 => 1~0 - end. - -Fixpoint map (x : positive) : nat := - match x with - | p~1 => 1 + (map p + map p) - | p~0 => map p + map p - | 1 => 1 - end. - -Fixpoint add (x y : positive) : positive := - match x, y with - | 1, p | p, 1 => succ p - | p~0, q~0 => (add p q)~0 - | p~0, q~1 | p~1, q~0 => (add p q)~1 - | p~1, q~1 => succ (add p q)~1 - end. -Infix "+" := add : positive_scope. -Notation "p .+1" := (succ p) : positive_scope. - -Lemma addpp x : x + x = x~0. Proof. by elim: x => //= ? ->. Qed. -Lemma addp1 x : x + 1 = x.+1. Proof. by elim: x. Qed. -Lemma addpS x y : x + y.+1 = (x + y).+1. -Proof. by elim: x y => // p IHp [q|q|]//=; rewrite ?IHp ?addp1//. Qed. -Lemma addSp x y : x.+1 + y = (x + y).+1. -Proof. by elim: x y => [p IHp|p IHp|]// [q|q|]//=; rewrite ?IHp//. Qed. - -End Pos. -Infix "+" := Pos.add : positive_scope. -Notation "p .+1" := (Pos.succ p) : positive_scope. - -Inductive N : Set := - | N0 : N - | Npos : positive -> N. - -Declare Scope N_scope. -Delimit Scope N_scope with N. -Bind Scope N_scope with N. - -Notation "0" := N0 : N_scope. - -Definition succ_pos (n : N) : positive := - match n with - | N0 => 1%positive - | Npos p => Pos.succ p - end. - -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. -Infix "+" := Nadd : N_scope. -Notation "n .+1" := (Nsucc n) : N_scope. - -(* various possible proofs to fill the fields of a parametricity witness between N and nat *) - -Definition Nmap (n : N) : nat := - match n with - | N0 => 0 - | Npos p => Pos.map p - end. - -Fixpoint Ncomap (n : nat) : N := - match n with O => 0 | S n => Nsucc (Ncomap n) end. - -Lemma Naddpp p : (Npos p + Npos p)%N = Npos p~0. -Proof. by elim: p => //= p IHp; rewrite Pos.addpp. Qed. - -Lemma NcomapD i j : Ncomap (i + j) = (Ncomap i + Ncomap j)%N. -Proof. -elim: i j => [|i IHi] [|j]//=; first by rewrite -nat_add_n_O//. -rewrite -nat_add_n_Sm/= IHi. -case: (Ncomap i) => // p; case: (Ncomap j) => //=. -- by rewrite /Nsucc/= Pos.addp1. -- by move=> q; rewrite /Nsucc/= Pos.addpS Pos.addSp. -Qed. - -Let NcomapNpos p k : Ncomap k = Npos p -> Ncomap (k + k) = Npos p~0. -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. - (* 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 RN := SplitSurj.toParamSym@{Set} {| diff --git a/theories/Common.v b/theories/Common.v index d9c60c6..5b5b0d9 100644 --- a/theories/Common.v +++ b/theories/Common.v @@ -44,7 +44,7 @@ Module SplitInj. Section SplitInj. Universe i. Context {A B : Type@{i}}. -Record type@{} := { +Record type@{} := Build { section :> A -> B; retract : B -> A; sectionK : forall x, retract (section x) = x @@ -78,12 +78,13 @@ End to. End SplitInj. End SplitInj. +Arguments SplitInj.Build {A B section retract}. Module SplitSurj. Section SplitSurj. Universe i. Context {A B : Type@{i}}. -Record type := { +Record type := Build { retract :> A -> B; section : B -> A; sectionK : forall x, retract (section x) = x @@ -117,6 +118,7 @@ End to. End SplitSurj. End SplitSurj. +Arguments SplitSurj.Build {A B retract section}. Module Equiv. (* This is exactly adjointify *) @@ -134,7 +136,7 @@ Module Iso. Section Iso. Universe i. Context {A B : Type@{i}}. -Record type@{} := { +Record type@{} := Build { map :> A -> B; comap : B -> A; mapK : forall x, comap (map x) = x; @@ -184,3 +186,4 @@ End to. End Iso. End Iso. +Arguments Iso.Build {A B map comap}. \ No newline at end of file