The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Dominique,

Thank you very much for your response. It is much clearer now.  At
least, now I can see the structure of the proof.

(* I am posting it here because not many people from Coq mailing list
are on Zulip chat *)
Also, yesterday during this proof I realised that the induction
principle for  `le` is not strong enough so I used the 'Scheme le_indd
:= Induction for le Sort Prop. ' to derive a more general one, but I
could not finish the proof, but Paolo Giarrusso, at Zulip chat, came
up with this proof using the Equations package.  I don't understand
all the machinery behind the 'dependent elimination' from Equations
but it's really making life easy.

Require Import Lia.
Require Import Equations.Prop.Equations.
Scheme le_indd := Induction for le Sort Prop.

Set Equations With UIP.

Lemma le_unique : forall {m n : nat}
  (p q : m <= n), p = q.
Proof.
  induction p using le_indd.
  + intros Hq.
    dependent elimination Hq; [|lia].
    easy.
  + intros Hq.
    dependent elimination Hq; [lia|].
    f_equal.
    apply IHp.
Qed.
Print Assumptions le_unique. (* Closed under the global context *)

Best,
Mukesh


On Sun, Jun 5, 2022 at 8:46 PM Dominique Larchey-Wendling
<dominique.larchey-wendling AT loria.fr> wrote:
>
> 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