✔ Proving that functions are inverse of each other · math-comp users

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! *)

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

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

Stream: math-comp users

Topic: ✔ Proving that functions are inverse of each other

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