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.
Admitted.
```

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! *)
admit.
+ destruct m;
intros Hi.
++ cbn.
(* Hi should be (erefl true)
becuase it's a decidable
proposition
but how I can infer that *)
f_equal.
admit.
++ (* From Hi *)
cbn.
unfold finite_to_ord.
destruct to_nat.
(* Now, I don't know how to prove this! *)
```

For the first one, use `of_nat_ext`

. For the second, `to_nat_of_nat`

.

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).
```

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.
```

BTW, using `bool_irrelevance`

should remove half the need to reprove `introT`

etc as `Defined`

. lemmas…

@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.`

this is similar to `of_nat_ext`

, which should avoid the other half of the need to reprove `Defined`

lemmas

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.

@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.

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

always satisfy such lemmas.

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

Thanks @Paolo Giarrusso and @Li-yao !

Mukesh Tiwari has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC