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.
(*D*) by case: s.
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 *)
(*D*) Canonical res_sT := Rel_s cmp_trans f_mon.
(* 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.
(*D*) move => s n.
(*D*) apply: (@cmp_trans _ (f (f n))); last exact: cmp_f.
(*D*) apply: (@cmp_trans _ (f n)); last exact: cmp_f.
(*D*) exact: cmp_f.
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 *)
(*D*) Canonical nat_rel_s : rel_s := Rel_s leq_trans leqnSn.
(* Test that your declaration has the desired behaviour by stating and *)
(* proving the result which should be trivial if the benchmark is *)
(* successful *)
Lemma lt3 : forall n, n <= n.+3.
Proof. move => n. by apply: f3. Qed.
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 prove that pair_rel is transitive *)
(*D*) Lemma pair_rel_trans : transitive pair_rel.
(*D*) Proof.
(*D*) case=> x1 x2 [y1 y2] [z1 z2] /andP /= [h1yx h2yx] /andP /= [h1xz h2xz].
(*D*) by rewrite /pair_rel /= (r1_trans h1yx) // (r2_trans h2yx).
(*D*) Qed.
(* State and prove that pair_fun is monotonic wrt pair_rel *)
(*D*)Lemma pair_fun_mon : forall x, pair_rel x (pair_fun x).
(*D*)Proof.
(*D*)by case=> x y; rewrite /pair_rel /= f1_mon f2_mon.
(*D*)Qed.
End Pairs.
(* Write a canonical declaration which builds a new instance of rel_s *)
(* from two existing ones using the lemmas proved in section Pairs. *)
(*D*)Canonical rel_s_pair (s1 s2 : rel_s) :=
(*D*) Rel_s (pair_rel_trans (@cmp_trans s1) (@cmp_trans s2))
(*D*) (pair_fun_mon (@cmp_f s1) (@cmp_f s2)).
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).
(*D*) Proof. exact: cmp_f. Qed.
(* Now instanciate rel_s for divisibility and doubling on nat and test *)
(* your approach *)
(*D*)Lemma dvdn_double : forall n, n %| n.*2.
(*D*)Proof. move => n; rewrite -mul2n dvdn_mull // dvdnn. Qed.
(*D*)Canonical Structure div_rel_s := Rel_s dvdn_trans dvdn_double.
(*D*)Lemma dvdn_times8 : forall n, n %| n.*2.*2.*2.
(*D*)Proof. move=> n; exact: f3. Qed.
(* 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 provably 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}.
(*D*)Canonical myord_subType := [subType for myordval by myord_rect].
(*D*)Lemma test2 : forall u v : myord, (val u) = (val v) -> u = v.
(*D*)Proof.
(*D*)move=> u v.
(*D*)About val_inj.
(*D*)exact: val_inj.
(*D*)Qed.
(*D*)Definition xmyord (x : nat)(px : x < n) : myord := Sub x px.
(*D*)Definition onat_of_myord (x : nat) : option myord := insub x.
(*D*)Check onat_of_myord.
(*D*)Definition otest2 (q : myord -> bool) (x : nat) :=
(*D*) if (insub x) is Some x_as_myord then q x_as_myord else false.
(*D*)About otest2.
(*D*)Definition myord_eqMixin := [eqMixin of myord by <:].
(*D*)Canonical myord_eqType := EqType myord myord_eqMixin.
(*D*)Lemma test_eq2 : forall x : myord, x == x.
(*D*)Proof. by []. Qed.
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 *)
(*D*) Canonical tuple_subType := [subType for tval by tuple_rect].
(* Prove the following lemma using only eqP and valP *)
Lemma size_tuple (t : tuple) : size t = n.
(*D*) Proof. exact: (eqP (valP t)). Qed.
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.
(*D *) Proof. move=> s z; exact: cats1. Qed.
End TupleSubType.
(* Declare a canonical instance of tuple for nil *)
(*D*)Canonical nil_tuple T := Tuple (isT : @size T [::] == 0).
(* Use this lemma to declare a canonical instance of tuple for lists of the *)
(* shape (x :: t) where t is itself a tuple *)
(*D*) Canonical cons_tuple n T x (t : tuple n T) :=
(*D*) Tuple (valP t : size (x :: t) == n.+1).
(* 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.
(*D*) Proof. by rewrite size_rcons size_tuple. Qed.
(* Use this lemma to declare a canonical instance of tuple for lists of the *)
(* shape (rcons x t) where t is itself a tuple *)
(* D *) Canonical rcons_tuple n T (t : tuple n T) x := Tuple (rcons_tupleP t x).
(* 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 *)
(*D*)Definition tuple_of_eqMixin (n : nat)(T : eqType) :=
(*D*) [eqMixin of (tuple n T) by <:].
(*D*)Canonical tuple_of_eqType n (T : eqType) :=
(*D*) EqType (tuple n T) (tuple_of_eqMixin n T).
End TupleDefinition.