From ec069cae6f772d44edd846d8fc7411f8feacc82d Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Jan 2024 15:16:10 +0100 Subject: [PATCH] Update TUTORIAL.md --- artifact-doc/TUTORIAL.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/artifact-doc/TUTORIAL.md b/artifact-doc/TUTORIAL.md index 29c6aee..cbb4682 100644 --- a/artifact-doc/TUTORIAL.md +++ b/artifact-doc/TUTORIAL.md @@ -33,14 +33,14 @@ Inductive N : Set := ``` We can show that there is an isomorphism between `N` and the standard library `nat` encoding for natural numbers in Peano style, by proving `Iso.type N nat`, *i.e.*, by inhabiting the following types: ```coq -N_to_nat : N -> nat -nat_to_N : nat -> N -N_to_natK : forall n, nat_to_N (N_to_nat n) = n -nat_to_NK : forann n, N_to_nat (nat_to_N n) = n +N.to_nat : N -> nat +N.of_nat : nat -> N +N.to_natK : forall n, N.of_nat (N.to_nat n) = n +N.of_natK : forall n, N.to_nat (N.of_nat n) = n ``` -By using `Iso.toParam`, we can prove `RN44 : Param44.Rel N nat`, which is a parametricity relation between both types, and as such, can be added to Trocq with the following command: +By using `Iso.toParamSym`, we can prove `RN : Param44.Rel N nat`, which is a parametricity relation between both types, and as such, can be added to Trocq with the following command: ```coq -Trocq Use RN44. +Trocq Use RN. ``` Now, suppose we want to prove the following lemma about binary natural numbers (the successor-based induction principle): @@ -134,4 +134,4 @@ Provided that we add proofs in Trocq relating `nat`, `Bool`, equality, and order ```coq forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool), (i < k)%nat -> getBit_bnat (setBit_bnat bn i b) i = b -``` \ No newline at end of file +```