## Stream: math-comp users

### Topic: ✔ Proving that functions are inverse of each other

#### Mukesh Tiwari (May 11 2022 at 20:17):

I am trying to prove the following lemmas. In the first lemma` finite_to_ord_correctness`, I am stuck with induction hypothesis because I can't massage the goal to be equal to induction hypothesis.

``````n: nat
i': t n
a: nat
Ha: (a < n)%coq_nat
IHn: of_nat_lt
(elimT (a < n)%coq_nat (eqn (a.+1 - n)%Nrec 0) ltP
(ltn_ord
(Ordinal (n:=n) (m:=a)
(introT (a < n)%coq_nat (eqn (a.+1 - n)%Nrec 0) ltP Ha)))) =
i'
--------------------------------------------------------------------------------
1/1
of_nat_lt
(Lt.lt_S_n a n
(elimT (a.+1 < n.+1)%coq_nat (eqn (a.+1 - n)%Nrec 0) ltP
(ltn_ord
(Ordinal (n:=n.+1) (m:=a.+1)
(introT (a.+1 < n.+1)%coq_nat (eqn (a.+1 - n)%Nrec 0) ltP
(Lt.lt_n_S a n Ha)))))) = i'

Lemma finite_to_ord_correctness n (i : Fin.t n) :
ord_to_finite (finite_to_ord i) = i.
Proof.
induction n.
+ inversion i.
+ pose proof fin_inv_S _ i as [-> | (i' & ->)].
++ cbn; reflexivity.
++  specialize (IHn i').
unfold
finite_to_ord,
ord_to_finite,
ssr_have in * |- *.
(* Thing below lead to off by one term in goal *)
cbn in * |- *.
destruct (to_nat i') as [a Ha].
cbn.
f_equal.
cbn in *.
Check Lt.lt_S_n.
``````

In this case, I have no idea how to prove it. Any hint would be very helpful. Complete source code.

``````Lemma ord_to_finite_correctness n (i : 'I_n) :
finite_to_ord (ord_to_finite i) = i.
Proof.
apply (@ordinal_ind n
(fun i => finite_to_ord (ord_to_finite i) = i)).
induction n.
+ intros m Hi.
(* I can't discharge it! *)
+ destruct m;
intros Hi.
++ cbn.
(* Hi should be (erefl true)
becuase it's a decidable
proposition
but how I can infer that *)
f_equal.
++ (* From Hi *)
cbn.
unfold finite_to_ord.
destruct to_nat.
(* Now, I don't know how to prove this! *)
``````

#### Li-yao (May 11 2022 at 20:40):

For the first one, use `of_nat_ext`. For the second, `to_nat_of_nat`.

#### Mukesh Tiwari (May 12 2022 at 19:05):

Thanks @Li-yao . The rewrite helped a lot but I can't figure out how to apply induction hypothesis in this case.

``````R: Type
n: nat
i: 'I_n.+1
m: nat
Hmt: m < n
IHn: Ordinal (n:=n) (m:=m)
(introT ltP (elimT ltP (ltn_ord (Ordinal (n:=n) (m:=m) Hmt)))) =
Ordinal (n:=n) (m:=m) Hmt
Hm: m.+1 < n.+1
Hin: 'I_n
------------------------------------------------------------------------------------------
1/1
Ordinal (n:=n.+1) (m:=m.+1)
(introT ltP (elimT ltP (ltn_ord (Ordinal (n:=n.+1) (m:=m.+1) Hm)))) =
Ordinal (n:=n.+1) (m:=m.+1) Hm

Lemma ord_to_finite_correctness n (i : 'I_n) :
finite_to_ord (ord_to_finite i) = i.
Proof.
unfold finite_to_ord,
ord_to_finite,
ssr_have.
rewrite to_nat_of_nat.
dependent inversion i.
cbn.
revert dependent m.
induction n.
+ intros ? Hm.
pose proof (Matrix.elimT ltP Hm) as Hf.
nia.
+ intros [ | m] Hm.
++ cbn.
f_equal.
symmetry.
apply Eqdep_dec.UIP_refl_bool.
++
pose proof (Matrix.elimT ltP Hm) as Hmt.
apply Lt.lt_S_n in Hmt.
apply (Matrix.introT ltP) in Hmt.
pose proof (Ordinal Hmt) as Hin.
(* I feel it's not the way that can be applied to goal *)
specialize (IHn Hin _ Hmt).
``````

#### Li-yao (May 12 2022 at 23:37):

The induction proof is already done in `to_nat_of_nat`. Note that both sides of the equality already have the same `n` and `m`, the only difference is the proof term `m < n`, which is unique.

``````  Lemma ord_to_finite_correctness n (i : 'I_n) :
finite_to_ord (ord_to_finite i) = i.
Proof.
unfold finite_to_ord, ord_to_finite, ssr_have.
rewrite to_nat_of_nat.
destruct i; cbn. f_equal. apply bool_irrelevance.
``````

#### Paolo Giarrusso (May 13 2022 at 05:39):

BTW, using `bool_irrelevance` should remove half the need to reprove `introT` etc as `Defined`. lemmas…

#### Paolo Giarrusso (May 13 2022 at 05:44):

@Li-yao it seems you can encapsulate what you did by proving something like `Lemma ord_eq_intro {n} (i j : ‘I_n) : (nat_of_ord i = nat_of_ord j) -> i = j.` — or use directly `Lemma ord_inj : injective nat_of_ord.`

#### Paolo Giarrusso (May 13 2022 at 05:49):

this is similar to `of_nat_ext`, which should avoid the other half of the need to reprove `Defined` lemmas

#### Paolo Giarrusso (May 13 2022 at 05:50):

there is also `Lemma to_nat_inj {n} (p q : t n) : proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q.`, which unlike `of_nat_ext` is not restricted to the result of `of_nat_lt`: it asserts that two `Fin.t` are equal whenever their projections down to naturals are equal.

#### Paolo Giarrusso (May 13 2022 at 05:53):

@Mukesh Tiwari to avoid problems with `Qed` proofs, whenever I deal with equality on sigma types (or worse, indexed types like `Fin.t`) I first find or prove such lemmas, so that I never need to prove that two proofs are equal.

#### Paolo Giarrusso (May 13 2022 at 05:55):

in particular, since equalities on booleans are provably proof-irrelevant, sigma types of shape `{ x : T | f x = true }` always satisfy such lemmas.

#### Paolo Giarrusso (May 13 2022 at 06:01):

Also proof-irrelevant: equalities on any type with decidable equality, but the ssreflect methodology recommends using boolean predicates `f : T -> bool`

#### Mukesh Tiwari (May 13 2022 at 16:50):

Thanks @Paolo Giarrusso and @Li-yao !

#### Notification Bot (May 13 2022 at 23:40):

Mukesh Tiwari has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC