Skip to content

Latest commit

 

History

History
137 lines (117 loc) · 8.19 KB

TUTORIAL.md

File metadata and controls

137 lines (117 loc) · 8.19 KB
Raw

Tutorial

This tutorial for Trocq first explains how to use the plugin in general, then covers several examples of proof transfer cases.

Use of the plugin

The Trocq plugin must be used in two steps:

  1. First, the user fills in the knowledge base by declaring pairs of terms linked by a parametricity relation.
    These terms can be inductive types or any constants. Two terms a : A and a' : A' must be related by an instance of the relation AR linking their types A and A', i.e., an inhabitant of AR a a'. In the particular case of types, two types A and B must be related by an inhabitant of ParamNK.Rel A B with (N, K) the parametricity class describing the structure given to the relation between A and B, ranging from a raw relation to a full type equivalence.
    Declaring these relations can be done by filling every desired field of the Param record, but can be made easier by going through the definitions in theories/Common.v. Indeed, we offer to the user a way to generate Param records from functions (module Fun), split injections (module SplitInj), split surjections (module SplitSurj), or isomorphisms (module Iso), respectively yielding instances of Param at levels $(4, 0)$, $(4, 2_b)$, $(4, 2_a)$, and $(4, 4)$.

  2. Second, the user states a goal to prove featuring terms that are left-hand components in the previously declared pairs, so that Trocq can perform proof transfer and rephrase the goal with the right-hand components, by combining the parametricity relations provided with the pairs of terms.

The first step is done with the Trocq Use command whose only argument is the parametricity relation. The second step is done by calling the trocq tactic after stating the goal to prove. The tactic then automatically proves the goal substitution with a generated transfer proof and only leaves the associated goal to prove.

Examples

In this section, we show some use cases of Trocq related to arithmetic, polymorphism, and dependent types.

Binary natural numbers (peano_bin_nat.v)

In this example, we define a binary version of natural numbers in the following way:

Inductive positive : Set :=
  | xI : positive -> positive
  | xO : positive -> positive
  | xH : positive.

Inductive N : Set :=
  | N0 : N
  | Npos : positive -> N.

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:

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.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:

Trocq Use RN.

Now, suppose we want to prove the following lemma about binary natural numbers (the successor-based induction principle):

Lemma N_Srec : forall (P : N -> Type), P N0 -> (forall n, P n -> P n.+1%N) -> forall n, P n.

We can see N0 and a binary successor operation .+1%N appear in the goal. We must therefore add them to Trocq as well before running the tactic. As they are not type formers, the parametricity proofs expected to relate N0 to O and .+1%N to S are instances of the relation given in RN44 relating natural numbers in both encodings:

RN0 : RN 0%N 0%nat
RNS : forall m n, RN m n -> RN m.+1%N n.+1%nat

Once these proofs are defined, we can add them to Trocq with the following commands:

Trocq Use RN0.
Trocq Use RNS.

Now, everything has been declared and we are ready to call trocq on the goal, to obtain the following associated goal:

forall (P : nat -> PType map1 map1), P O -> (forall n, P n -> P (S n)) -> forall n, P n

Let us explain quickly the PType map1 map1. According to dependency propagation in the Trocq inference rules, the occurrence of Type in the original goal had to be related to itself at level $(2_a, 0)$ in the hierarchy, i.e. by a term of type Param2a0.Rel Type Type, which can be proved by giving structure $(2_a, 0)$ to any relation of the hierarchy. Because of all the occurrences of P in the goal, this initially arbitrary relation was constrained to be at least Param11.Rel, which explains the displayed class in the output goal. Please note that PType map1 map1 is convertible to Type, this is just present to inform the user about what was required during the proof.

We can conclude this proof by noticing the goal is now exactly the induction principle generated by Coq on the nat type, and calling exact nat_rect.

The peano_bin_nat.v file contains this example but remarks that the isomorphism-based RN44 was not strictly necessary, and a relation at level $(2_a, 3)$ was sufficient to perform this proof transfer.

Modular arithmetic (int_to_Zp.v)

In this example, we study a directed relation between unary integers (int) and integers modulo a constant $p$. Indeed, it is directed because the types are not fully equivalent and thus a relation at level $(4, 4)$ of the hierarchy cannot be stated between them. We know that two functions modp : Zmodp -> int and reprp : Zmodp -> int can be defined and the following property holds:

forall x, modp (reprp x) = x

The graph of modp is therefore a surjective relation, and through the SplitSurj module we can build a parametricity relation Rp : Param2a4.Rel Zmodp int, which can be added to Trocq with the following command:

Trocq Use Rp.

After adding to Trocq a proof relating additions in both encodings and a proof relating equality to itself at level $(0,1)$, with 2 further calls to Trocq Use, we can transfer the following goal to the statement of commutativity of addition over int:

(forall x y, x + y = y + x)%Zmodp.

As int is defined in the MathComp library, this property is already proved and comes under the name addC. We can therefore close the goal and get commutativity of addition over Zmodp "for free".

Bitwise arithmetic (Vector_tuple.v)

Here, we focus on relating two dependent types encoding for fixed-size bitvectors:

Definition bounded_nat (k : nat) := {n : nat & n < pow 2 k}%nat.
Definition bitvector (k : nat) := Vector.t Bool k.

We can relate them together, in an easier way by transitivity, by first relating bounded_nat k to bitvector k for a given k, then by relating Vector.t A k to Vector.t A' k' for any related types A and A', and any related numbers k and k', before combining both previous proofs with the following lemma available in Trocq:

Param44_trans : forall A B C, Param44.Rel A B -> Param44.Rel B C -> Param44.Rel A C.

This proof RBV can be added to Trocq by Trocq Use RBV. We can then define operations to get and set bits in both encodings of bitvectors, relate them with RBV, and add them to Trocq as well.

setBit_bv : forall {k : nat}, bitvector k -> nat -> Bool -> bitvector k
setBit_bnat : forall {k : nat}, bounded_nat k -> nat -> Bool -> bounded_nat k
getBit_bv : forall {k : nat}, bitvector k -> nat -> Bool
getBit_bnat : forall {k : nat}, bounded_nat k -> nat -> Bool
setBitR
  (k k' : nat) (kR : natR k k')
  (bn : bounded_nat k) (bv' : bitvector k') (r : RBV bn bv')
  (n n' : nat) (nR : natR n n')
  (b b' : Bool) (bR : BoolR b b') :
    RBV (setBit_bnat bn n b) (setBit_bv bv' n' b')
Trocq Use setBitR.
getBitR
  (k k' : nat) (kR : natR k k')
  (bn : bounded_nat k) (bv' : bitvector k') (r : RBV bn bv')
  (n n' : nat) (nR : natR n n') :
    BoolR (getBit_bnat bn n) (getBit_bv bv' n').
Trocq Use getBitR.

Now suppose we proved a lemma about getting a bit that just got set to a new value, in the bitvector encoding:

Lemma setBitThenGetSame :
  forall {k : nat} (bv : bitvector k) (i : nat) (b : Bool),
    (i < k)%nat -> getBit_bv (setBit_bv bv i b) i = b.

Provided that we add proofs in Trocq relating nat, Bool, equality, and order to themselves, we can call the trocq tactic on the following goal, and close the proof with setBitThenGetSame:

forall {k : nat} (bn : bounded_nat k) (i : nat) (b : Bool),
  (i < k)%nat -> getBit_bnat (setBit_bnat bn i b) i = b