The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Mukesh,

Maybe this one gives a better intuition?
But it does not go through a double induction principle.
Rather the classic combination of induction and then inversion.

Best,

D.

--------

Require Import Eqdep_dec Arith.

Fact uip_nat {n : nat} (e : n = n) : e = eq_refl.
Proof. apply UIP_dec, eq_nat_dec. Qed. 

Fact le_inv n m (H : n <= m) : 
     (exists e : m = n, eq_rect _ _ H _ e = le_n n)
  \/ (exists m' (e : m = S m') (H' : n <= m'), eq_rect _ _ H _ e = le_S _ _ 
H').
Proof.
  revert m H.
  intros ? [ | m H ].
  + left; now exists eq_refl.
  + right; now exists m, eq_refl, H.
Qed.

Check lt_irrefl.

Lemma le_unique : forall {m n : nat}
    (p q : m <= n), p = q.
Proof.
  intros m. refine (fix loop n p { struct p } := _).
  destruct p as [ | n p ]; intros q.
  + clear loop; destruct (le_inv _ _ q) as [ (e & H) | (m' & e & H1 & H2) ].
    * now rewrite (uip_nat e) in H.
    * exfalso; subst; clear H2.
      now apply lt_irrefl in H1.
  + specialize (loop _ p).
    destruct (le_inv _ _ q) as [ (e & H) | (m' & e & H1 & H2) ].
    * clear loop; exfalso; subst; clear H.
      now apply lt_irrefl in p.
    * injection e; intros H3.
      revert e H1 H2; rewrite <- H3; intros e H1 H2.
      rewrite (loop H1).
      rewrite (uip_nat e) in H2; simpl in H2; subst q.
      f_equal; apply loop.
Qed.


----- Mail original -----
> De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Dimanche 5 Juin 2022 20:12:47
> Objet: [Coq-Club] Custom Induction Principal for le_unique

> Hi everyone,
> 
> I am trying to understand this proof [1]. It is very difficult to
> understand by replaying the proof so I decided to write a custom
> induction principle (le_pair_ind) which would make the proof trivial
> and easier to read. However, I am stuck with a pattern in le_pair_ind.
> In le_pair_ind, the first pattern, on l,  is fine but the problem
> arises in the second pattern match, on h. I don't know how to force h
> to be le_n. Any help would be appreciated.
> 
> 
> 
> Lemma le_pair_ind :
>    forall (n : nat)
>    (P : forall m : nat, n <= m -> n <= m -> Prop),
>    P n (le_n n) (le_n n) ->
>    (forall (m : nat) (l h : n <= m), P m l h ->
>      P (S m) (le_S n m l) (le_S n m h)) ->
>    forall (m : nat) (l h : n <= m), P m l h.
>  Proof.
>    intros ? P Hb Hc.
>    refine(
>      fix Fn m l :=
>      match l as lp in (_ <= mp) return forall h, P mp lp h with
>      | le_n _  => fun h => _ (* I DON'T KNOW HOW TO FORCE h  TO BE le_n *)
>      | le_S _ m lp => _
>      end).
>  Admitted.
> 
>  Lemma le_unique : forall {m n : nat}
>    (p q : m <= n), p = q.
>  Proof.
>    intros ? ? ? ?.
>    apply (le_pair_ind m
>      (fun (n : nat) (a : m <= n) (b : m <= n) => a = b)).
>    + exact eq_refl.
>    + intros ? ? ? He;
>      subst; reflexivity.
>  Qed.
> 
> Best,
> Mukesh
> 
> [1] https://github.com/coq/coq/blob/master/theories/Arith/Peano_dec.v#L40