Establish isomorphism between finite natural numbers and sigma

Question

I'm here with Coq studying the relations between two types I've defined. The first is something like a finite subset of nat, with just three elements:

Inductive N3 := zero | one | two.

The second is a sigma type with elements satisfying the proposition {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 definied the two functions involved in the following manner:

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 succeed in defining the first part of the isomorphism

Definition eq_n3_n3 (n: N3) : lt3_to_N3 (N3_to_lt3 n) = n.
Proof.
by case n.
Defined.

But I'm not able to define 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 sure at all about the rest of the definition. I also tried to pattern-match on x and on (N3_to_lt3 (lt3_to_N3 x)), but I'm not sure about 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.

Answer 1

You can also have some fun if you profit from the finType machinery in math-comp.

For example, you can use the enumeration of ordinals [isomorphic to your type] to prove your lemma by enumerating all the values instead of doing 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 super well-suited to do this job, but it is fun to get to know the library a bit more nonetheless.

Another fun exercise is to define the finType instance for your custom datatype and then establish that both sets have the same cardinality! There are many lemma combinations to try here so you will have fun!

Answer 2

Since you are using ssreflect, the easiest route is to use the computational definition of < (in ssrnat), and then apply the val_inj lemma:

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 statement of val_inj is a bit complicated, but the basic idea is simple: for any boolean predicate P on a type T, the canonical projection { x : T | P x = true } -> T is injective. As Vinz put it, this relies on boolean equalities being proof irrelevant; that is, any two proofs of an equality between booleans are themselves equal. Because of that, equality on {x | P x = true} is entirely determined by the element x; the proof component is irrelevant.

Answer 3

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'll have goals like:

exist (fun x : nat => x < 3) 0 h = exist (fun x : nat => x < 3) 0 l_0_3

Basically the only difference now is that you have "some proof that 0 < 3 named h" on the left hand side and "Your exact proof that 0 < 3 named l_0_3" on the right hand side.

So you'll have to look in the direction of proof irrelevant / uniqueness of identity proofs (which is provable over nat & lt).