Inside the MathComp book https://zenodo.org/records/7118596 there is the following example of use for the Canonical command:
(* Declaring seq with fixed size (i.e. a tuple): *)
Structure tuple_of n T := Tuple { tval :> seq T; _ : size tval == n}.
Notation "n .-tuple T" := (tuple_of n T) (at level 100, no associativity).
Lemma size_tuple T n (t : tuple_of n T) :
size t = n.
Proof.
destruct t. simpl. pose proof (@eqP nat).
unfold Equality.axiom in X. specialize (X (size tval0) n).
apply rwP in X. apply X. assumption.
Qed.
(* The following lema is important because when rev is applied in t,
the result is considered by Coq as having type seq T, so the result
lost the information about size: *)
Lemma rev_tupleP {n} {T} (t : tuple_of n T) :
size (rev t) == n.
Proof.
rewrite size_rev. rewrite size_tuple. by [].
Qed.
(* Such loss of information occurs because Coq can't produce a proof
about the size of "rev t", but with this lemma (which is the same
as a function that returns a proof) we can teach Coq a way to mantain
the type as tuple when applying the "rev" function (we are teaching
Coq how it can create a new tuple applying "rev" in the field "tval" ): *)
Canonical rev_tuple {n : nat} {T : Type} (t : tuple_of n T) := Tuple n T (rev t) (rev_tupleP t).
(* The same stuff happens with mapping: *)
Lemma map_tupleP {n A B} (f : A -> B) (t : tuple_of n A) :
size (map f t) == n.
Proof.
by rewrite size_map size_tuple.
Qed.
Canonical map_tuple {n : nat} {A B : Type} (f : A -> B) (t : tuple_of n A) :=
Tuple n B (map f t) (map_tupleP f t).
(* Thanks to the now extended capability of "type inference", we can prove the following
lemma byjust reasoning about tuples (the lemma "size_tuple" now can be applied to the
term "size (rev [seq 2 * x | x <- rev t])" ). *)
Example just_tuple n (t : tuple_of n nat) :
size (rev [seq 2 * x | x <- rev t]) = size t.
Proof.
rewrite size_tuple.
rewrite size_tuple.
reflexivity.
Qed.
My question is: I tried to make a similar example but It does not work, why? The code I wrote is:
Record zmod (n : nat) : Type := Build
{
x : nat;
axiom : x < n
}.
Definition zmodn_nat (n : nat) (e : zmod n) :=
match e with
| Build t _ => t
end.
Coercion zmodn_nat : zmod >-> nat.
Theorem Ex3 {n} :
∀ (a : zmod n), a < n.
Proof.
intros. destruct a. simpl. assumption.
Qed.
Theorem Ex4 {n} :
∀ (a : zmod n), (a %% n < n).
Proof.
destruct n.
{ intros. destruct a. unfold is_true in axiom0. inversion axiom0. }
{ intros. apply ltn_pmod. auto. }
Qed.
Definition mod_zmod {n : nat} (a : zmod n) : (zmod n) := Build n (a %% n) (Ex4 a).
Canonical mod_zmod.
Compute (rev [seq 2 * x | x <- rev [::5;2]]).
Example Ex5 {n} :
∀ (a : zmod n), (a %% n) < n = (a < n).
Proof.
intros. rewrite Ex3.
(* rewrite Ex3. *)
Abort.
In the last rewriting (commented), if I try to compile I get the following error:
Error: The LHS of Ex3
(_ < _)
does not match any subterm of the goal
