Establish an isomorphism between finite natural numbers and sigma
I am here when Kok is studying the relationship between the two types that I have defined. The first is something like a finite subset nat
, with only three elements:
Inductive N3 := zero | one | two.
The second is a sigma type with items that satisfy the proposal {x: nat | x < 3}
. Here's its definition:
Definition less_than_3 := {x| x < 3}.
I want to prove that these two types are isomorphic. I have defined two functions involved in the following:
Definition lt3_to_N3 (n: less_than_3) : N3 :=
match n with
| exist 0 _ => zero
| exist 1 _ => one
| exist 2 _ => two
| exist _ _ => two
end.
Definition N3_to_lt3 (n: N3) : less_than_3 :=
match n with
| zero => exist _ 0 l_0_3
| one => exist _ 1 l_1_3
| two => exist _ 2 l_2_3
end.
Where l_0_3
, l_1_3
and l_2_3
are just axioms:
Axiom l_0_3 : 0 < 3.
Axiom l_1_3 : 1 < 3.
Axiom l_2_3 : 2 < 3.
I managed to identify the first part of isomorphism
Definition eq_n3_n3 (n: N3) : lt3_to_N3 (N3_to_lt3 n) = n.
Proof.
by case n.
Defined.
But I cannot identify the other side. Here's what I've done so far:
Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
case: x.
move=> n p.
simpl.
???
I'm not entirely sure about the rest of the definition. I also tried to match the image on x
and on (N3_to_lt3 (lt3_to_N3 x))
, but I'm not sure what to return.
Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)) :=
match N3_to_lt3 (lt3_to_N3 x) with
| x => ???
end.
Thanks for the help.
source to share
I would start with something like
Definition eq_lt3_lt3 (x: lt3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
destruct x as [ n h ].
destruct n as [ | [ | [ | p ]]]; simpl in *.
At this point, you will have goals such as:
exist (fun x : nat => x < 3) 0 h = exist (fun x : nat => x < 3) 0 l_0_3
Basically the only difference is that you have "some proof that 0 and lt 3 are named h
" on the left, and "your exact proof that 0 <3 named l_0_3
" on the right side.
Thus, you will have to look towards proving the inappropriateness / uniqueness of identity proofs (which is proved over nat and lt).
source to share
You can also have a little fun if you profit from the finType mechanism in mathematics.
For example, you can use enumeration of ordinals [isomorphic to your type] to prove your lemma by enumerating all values, rather than doing the cumbersome cases:
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma falseP T : false -> T.
Proof. by []. Qed.
Inductive N3 := zero | one | two.
Definition lt3_to_N3 (n: 'I_3) : N3 :=
match n with
| Ordinal 0 _ => zero
| Ordinal 1 _ => one
| Ordinal 2 _ => two
| Ordinal _ f => falseP _ f
end.
Definition N3_to_lt3 (n: N3) : 'I_3 :=
match n with
| zero => @Ordinal 3 0 erefl
| one => @Ordinal 3 1 erefl
| two => @Ordinal 3 2 erefl
end.
Lemma eq_lt3_lt3 : cancel lt3_to_N3 N3_to_lt3.
Proof.
apply/eqfunP; rewrite /FiniteQuant.quant0b /= /pred0b cardE /enum_mem.
by rewrite unlock /= /ord_enum /= !insubT.
Qed.
(* We can define an auxiliary lemma to make our proofs cleaner *)
Lemma all_by_enum (T : finType) (P : pred T) :
[forall x, P x] = all P (enum T).
Proof.
apply/pred0P/allP => /= H x; first by have/negbFE := H x.
suff Hx : x \in enum T by exact/negbF/H.
by rewrite mem_enum.
Qed.
Lemma eq_lt3_lt3' : cancel lt3_to_N3 N3_to_lt3.
Proof.
by apply/eqfunP; rewrite all_by_enum enumT unlock /= /ord_enum /= !insubT.
Qed.
As you can see, the current design of math-comp is not well suited for this task, but it is interesting to know the library a little more.
Another interesting exercise is to define an instance finType
for your custom datatype, and then establish that both sets have the same cardinality! There are many combinations of lemmas to try here to keep you fun!
source to share
Since you are using ssreflect, the easiest way is to use computational definition <
(in ssrnat
) and then apply the lemma val_inj
:
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Inductive N3 := zero | one | two.
Definition less_than_3 := {x| x < 3}.
Definition lt3_to_N3 (n: less_than_3) : N3 :=
match n with
| exist 0 _ => zero
| exist 1 _ => one
| exist 2 _ => two
| exist _ _ => two
end.
Definition N3_to_lt3 (n: N3) : less_than_3 :=
match n with
| zero => exist _ 0 erefl
| one => exist _ 1 erefl
| two => exist _ 2 erefl
end.
Lemma eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
by apply: val_inj; case: x => [[| [|[|x]]] Px].
Qed.
The assertion is a val_inj
little more complicated, but the basic idea is simple: for any Boolean predicate P
for type, the T
canonical projection { x : T | P x = true } -> T
is injective. As Wintz put it, it depends on Boolean equalities that are proof of inessentials; that is, any two proofs of equality between booleans are themselves equal. Because of this, equality on is {x | P x = true}
completely determined by the element x
; the component of the proof is irrelevant.
source to share