Require Import ssreflect ssrfun ssrbool eqtype seq ssrnat div. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. (* We define her an interface for types equipped with a binary boolean *) (* relation and a unary operation monotonic wrt the previous relation*) (* Specification projections are unnamed to avoid introducing *) (* projections that do not play a role for the inference of canonical *) (* instances *) Structure rel_s := Rel_s { dom : Type; cmp : rel dom; f : dom -> dom; _ : transitive cmp; _ : forall x, cmp x (f x) }. (* Now we prove that the relation associated with an instance of rel_s *) (* is transitive.*) Lemma cmp_trans (s : rel_s) : transitive (@cmp s). Proof. by case: s. Qed. (* Prove the following lemma *) Lemma cmp_f (s : rel_s) : forall x : dom s, cmp x (f x). Proof. Qed. Section thms. (* We a assume a parameter type and all the material needed in order *) (* to build an instance of rel_s*) Variables (T :Type) (cmpT : rel T)(fT : T -> T). Hypothesis cmp_trans : transitive cmpT. Hypothesis f_mon : forall x, cmpT x (fT x). (* Define a canonical instance of rel_s for cmpT and fT *) (* Warning: the effect of canonical declarations do not survive *) (* to the end of sections *) (* This is a notation local to the section thms for the relation *) (* associated with the instance s *) End thms. (* Prove the following theorem *) Lemma f3 : forall (s : rel_s)(n : dom s), cmp n (f (f (f n))). Proof. Qed. (* Now f3 is our benchmark : we should obtain this result for free for *) (* types, rel and functions previously equipped with a canonical structure*) (* of rel_s *) (* Define a canonical instance of rel_s on type nat equipped with the *) (* relation leq and the successor operation *) (* Test that your declaration has the desired behaviour by stating and *) (* proving the result which should be trivial if the benchmark is *) (* successful *) Section Pairs. (* We assume two parameter types, and two binary boolean relations *) (* respectively on these types, and two unary functions *) Variables (T1 T2 : Type)(r1 : rel T1)(r2 : rel T2). Variables (f1 : T1 -> T1)(f2 : T2 -> T2). Hypothesis r1_trans : transitive r1. Hypothesis r2_trans : transitive r2. Hypothesis f1_mon : forall x, r1 x (f1 x). Hypothesis f2_mon : forall x, r2 x (f2 x). Definition pair_rel (u v : T1 * T2) := (r1 u.1 v.1) && (r2 u.2 v.2). (* Complete the following definition to define a function on pairs *) (* which associates (x, y) with the pair (f1 x, f2 y) *) Definition pair_fun (u : T1 * T2) := (*D *) (f1 u.1, f2 u.2). (* State and prouve that pair_rel is transitive *) (* State and prouve that pair_fun is monotonic wrt pair_rel *) End Pairs. (* Write a canonical declaration which builds a new instance of rel_s *) (* from two existing ones using the lemmas prouved in section Pairs. *) Definition test_fun := pair_fun S S. Definition test_comp := pair_rel leq leq. (* Find the shortest possible proof for this test lemma *) Lemma test : forall u : nat * nat, test_comp u (test_fun u). (* Now instanciate rel_s for divisibility and doubling on nat and test *) (* your approach *) (* More advanced exercises. These are toy version of formalized material *) (* to be found in the eqType, finType and tuple distributed libraries *) (* The eqType library of the distribution introduces a structure called *) (* subType such that (subType p) is the structure for types isomorphic to *) (* {x : T | p x} when (p : pred T) is a boolean predicate on type T *) (* Here is an excerpt from the documentation header of the eqType.v file: *) (* ---------------------------------------------------------------------------*) (* The subType interface supports the following operations: *) (* val == the generic injection from a subType S of T into T. *) (* For example, if u : {x : T | P}, then val u : T. *) (* val is injective because P is proof-irrelevant (P is in bool, *) (* and the is_true coercion expands to P = true). *) (* valP == the generic proof of P (val u) for u : subType P. *) (* Sub x Px == the generic constructor for a subType P; Px is a proof of P x *) (* and P should be inferred from the expected return type. *) (* insub x == the generic partial projection of T into a subType S of T. *) (* This returns an option S; if S : subType P then *) (* insub x = Some u with val u = x if P x, *) (* None if ~~ P x *) (* The insubP lemma encapsulates this dichotomy. *) (* P should be infered from the expected return type. *) (* ------------------ *) (* Subtypes inherit the eqType structure of their base types; the generic *) (* structure should be explicitly instantiated using the *) (* [eqMixin of S by <:] *) (* construct to declare the Equality mixin; this pattern is repeated for all *) (* the combinatorial interfaces (Choice, Countable, Finite). *) (* ---------------------------------------------------------------------------*) (* We start with a guided tour of the use of subTypes *) Section ToyExample. (* We assume a parameter eqType T, and a boolean unary predicate on T *) Variables (T : eqType)(p : pred T). (* We define a type for the elements of T for which p holds *) Structure pelem : Type := Pelem {pval : T; _ : p pval}. (* This is the incantation to automatically equip pelem with a structure of *) (* subType of T *) Canonical pelem_subType := [subType for pval by pelem_rect]. (* Now we get a set of generic constructions on pelem *) (* For instance we get that comparing elements in pelem is comparing their *) (* associated values in T. These values are accessed through the generic val *) (* injection *) Lemma test1 : forall u v : pelem, (val u) = (val v) -> u = v. Proof. move=> u v. About val_inj. exact: val_inj. Qed. (* Now suppose we dispose of an element (x : T) for which we have a proof that *) (* (p x) holds. We can use a generic pattern to forge the corresponding element*) (* of pelem *) Definition xpelem (x : T)(px : p x) : pelem := Sub x px. (* Finally the other way around, we cannot inject T into pelem since of course *) (* some elements of T might not satisfy p. But we can inject T into *) (* (option pelem), which is exactly a copy of pelem plus an extra default *) (* element None prouvably distinct from the other elements of (option pelem) *) (* Again there is a generic construction for subTypes for that purpose, *) (* called insub *) Definition oT_of_pelem (x : T) : option pelem := insub x. Check oT_of_pelem. (* An other example of application, we transform a function defined on pelem *) (* into a function defined on T by case analysis. *) Definition otest (q : pelem -> bool) (x : T) := if (insub x) is Some x_as_pelem then q x_as_pelem else false. About otest. (* Finally, declaring a canonical structure of subType of T provides a generic *) (* pattern to transmit the eqType structure available on T to pelem, by the *) (* following incantation*) (* Note that we actually cheated slightly in the lecture on the shape of the *) (* eqType structure *) Definition pelem_eqMixin := [eqMixin of pelem by <:]. Canonical pelem_eqType := EqType pelem pelem_eqMixin. (* Let us test that the eqType structure on pelem is operational, by testing that*) (* the == generic notation is available on pelem *) Lemma test_eq : forall x : pelem, x == x. Proof. by []. Qed. End ToyExample. Section OrdinalDefinition. Variable n : nat. (* Reproduce the content the previous section, replacing T by nat and pelem by *) (* the following type. Note that nat is already equipped with a structure of *) (* eqType *) Structure myord := {myordval : nat; _ : myordval < n}. End OrdinalDefinition. Section TupleDefinition. Section Def. Variables (n : nat)(T : Type). (* We know define a type for lists on T of prescribed length n *) (* The :> symbol means that tval is declared as a coercion: any inhabitant *) (* of tuple can be casted as a (seq T) by an automated and silent insertion *) (* of tval *) Structure tuple : Type := Tuple {tval :> seq T; _ : size tval == n}. (* Define a canonical instance of subType of (seq T) for tuple *) (* Prove the following lemma using only eqP and valP *) Lemma size_tuple (t : tuple) : size t = n. End Def. Section TupleSubType. Variables (n : nat)(T : eqType). (* Since n-tuples are coerced to lists, we benefit from the seq library for *) (* free and do not need to re-program and reprove all the factory *) (* Prove for instance the following lemma and conclude that it is useless... *) Lemma tuple_toy_cats1 : forall (s : tuple n T) z, s ++ [:: z] = rcons s z. End TupleSubType. (* Declare a canonical instance of tuple for nil *) (* Use this lemma to declare a canonical instance of tuple for lists of the *) (* shape (x :: t) where t is itself a tuple *) (* Test that the canonical structures works : these proofs should be accepted*) Lemma toy1 : size [::true] = 1. Proof. exact: size_tuple. Qed. Lemma toy2 : forall n (t : tuple n nat) x, size (x :: x :: t) = n.+2. Proof. move=> n t x. exact: size_tuple. Qed. (* Prove the following lemma: *) Lemma rcons_tupleP n T (t : tuple n T) x : size (rcons t x) == n.+1. (* Use this lemma to declare a canonical instance of tuple for lists of the *) (* shape (rcons x t) where t is itself a tuple *) (* Test that the canonical structure work as previously *) (* Now test that all the canonical structure interply nicely *) Lemma toy3 : forall n (t : tuple n nat) x, size (x :: x :: (rcons t x)) = n.+3. Proof. move=> n t x. exact: size_tuple. Qed. (* Definition a canonical instance of eqType for tuple on eqtypes *) End TupleDefinition.