From 661624c59d8c01321b3081e561e8fa3b26d517cf Mon Sep 17 00:00:00 2001 From: Enzo Crance Date: Wed, 6 Dec 2023 10:35:03 +0100 Subject: [PATCH] :recycle: Move proofs about nat in a separate file --- _CoqProject | 1 + examples/Vector_tuple.v | 41 -------------- theories/Param_nat.v | 115 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 116 insertions(+), 41 deletions(-) create mode 100644 theories/Param_nat.v diff --git a/_CoqProject b/_CoqProject index d837e91..f126d6b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -13,6 +13,7 @@ theories/Database.v theories/Param.v theories/Trocq.v theories/Vernac.v +theories/Param_nat.v theories/Param_paths.v theories/Param_sigma.v theories/Param_prod.v diff --git a/examples/Vector_tuple.v b/examples/Vector_tuple.v index 63022c5..79ad369 100644 --- a/examples/Vector_tuple.v +++ b/examples/Vector_tuple.v @@ -84,47 +84,6 @@ Definition append : (* ========================================================================== *) -(* nat ~ nat *) - -Inductive natR : nat -> nat -> Type := - | OR : natR O O - | SR : forall (n n' : nat), natR n n' -> natR (S n) (S n'). - -Definition Param33_nat : Param33.Rel nat nat. -Proof. - unshelve econstructor. - - exact natR. - - unshelve econstructor. - + exact id. - + intros n n' e. destruct e. induction n as [|n IHn]. - * exact OR. - * apply SR, IHn. - + intros n n' nR. induction nR as [|n n' nR IHnR]. - * reflexivity. - * unfold id. apply ap. exact IHnR. - - unshelve econstructor. - + exact id. - + intros n n' e. destruct e. induction n as [|n IHn]. - * exact OR. - * apply SR, IHn. - + intros n n' nR. induction nR as [|n n' nR IHnR]. - * reflexivity. - * unfold id. apply ap. exact IHnR. -Defined. - -Definition Param00_nat : Param00.Rel nat nat := Param33_nat. -Definition Param2a0_nat : Param2a0.Rel nat nat := Param33_nat. - -Definition Param_add : - forall (n1 n1' : nat) (n1R : natR n1 n1') (n2 n2' : nat) (n2R : natR n2 n2'), - natR (n1 + n2) (n1' + n2'). -Proof. - intros n1 n1' n1R n2 n2' n2R. - induction n1R as [|n1 n1' n1R IHn1R]. - - simpl. exact n2R. - - simpl. apply SR. exact IHn1R. -Defined. - (* tuple ~ vector *) Inductive tuple_vectorR (A A' : Type) (AR : A -> A' -> Type) : diff --git a/theories/Param_nat.v b/theories/Param_nat.v new file mode 100644 index 0000000..d868c9c --- /dev/null +++ b/theories/Param_nat.v @@ -0,0 +1,115 @@ +(*****************************************************************************) +(* * 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. +Require Import HoTT_additions Hierarchy. + +Set Universe Polymorphism. +Unset Universe Minimization ToSet. + +Inductive natR : nat -> nat -> Type := + | OR : natR O O + | SR : forall (n n' : nat), natR n n' -> natR (S n) (S n'). + +Definition map_nat : nat -> nat := id. + +Definition map_in_R_nat : forall {n n' : nat}, map_nat n = n' -> natR n n' := + fun n n' e => + match e with + | idpath => + (fix F n := + match n with + | O => OR + | S m => SR m m (F m) + end) n + end. + +Definition R_in_map_nat : forall {n n' : nat}, natR n n' -> map_nat n = n' := + fix F n n' (nR : natR n n') : map_nat n = n' := + match nR with + | OR => idpath + | SR m m' mR => ap S (F m m' mR) + end. + +Axiom cheat : forall A, A. +Ltac cheat := apply cheat. + +Definition R_in_mapK_nat : forall {n n' : nat} (nR : natR n n'), + map_in_R_nat (R_in_map_nat nR) = nR. +Proof. + intros n n' nR. + induction nR. + - simpl. reflexivity. + - simpl. unfold map_in_R_nat. + elim IHnR. + elim (R_in_map_nat nR). + cheat. +Defined. + +Definition natR_sym : forall (n n' : nat), sym_rel natR n n' <~> natR n n'. +Proof. + intros n n'. + unshelve econstructor. + - intros nR. unfold sym_rel in nR. + induction nR. + + exact OR. + + exact (SR n' n IHnR). + - unshelve econstructor. + + intros nR. unfold sym_rel. + induction nR. + * exact OR. + * exact (SR n' n IHnR). + + intros nR. induction nR. + * simpl. reflexivity. + * simpl. apply ap. apply IHnR. + + intros nR. unfold sym_rel in nR. + induction nR. + * simpl. reflexivity. + * simpl. apply ap. apply IHnR. + + simpl. intros nR. unfold sym_rel in nR. + induction nR. + * simpl. reflexivity. + * simpl. cheat. +Defined. + +Definition Map4_nat : Map4.Has natR. +Proof. + unshelve econstructor. + - exact map_nat. + - exact @map_in_R_nat. + - exact @R_in_map_nat. + - exact @R_in_mapK_nat. +Defined. + +Definition Param44_nat : Param44.Rel nat nat. +Proof. + unshelve econstructor. + - exact natR. + - exact Map4_nat. + - apply (fun e => @eq_Map4 _ _ (sym_rel natR) natR e Map4_nat). + apply natR_sym. +Defined. + +Definition Param00_nat : Param00.Rel nat nat := Param44_nat. +Definition Param2a0_nat : Param2a0.Rel nat nat := Param44_nat. + +Definition Param_add : + forall (n1 n1' : nat) (n1R : natR n1 n1') (n2 n2' : nat) (n2R : natR n2 n2'), + natR (n1 + n2) (n1' + n2'). +Proof. + intros n1 n1' n1R n2 n2' n2R. + induction n1R as [|n1 n1' n1R IHn1R]. + - simpl. exact n2R. + - simpl. apply SR. exact IHn1R. +Defined.