The Coq mailing list

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

Hi everyone,

I have made some progress on this, and now I am facing one last
obstacle [1].  How can I replace a term  in this expression  'P (S nt)
(le_S n nt Hnt) (eq_rect nw (fun w : nat => n <= S w) (le_S n nw Hnw)
nt pf)'  by another equal term without causing ill-typed error. In
particular, I want to replace all the occurrences of nt by mt' and
replace pf by Hmnw. I want to discharge this goal [1] (also
copy-pasted below).



n, m: nat
P: forall m : nat, n <= m -> n <= m -> Prop
mt: nat
Hna: n <= mt
nt: nat
Hnt: n <= nt
Heq: mt = S nt
nw: nat
Hnw: n <= nw
pf: nw = nt
mt': nat
Hmm: nt = mt'
Hmnw: nw = mt'
============================================================
P (S nt) (le_S n nt Hnt) (eq_rect nw (fun w : nat => n <= S w) (le_S n
nw Hnw) nt pf)


Best,
Mukesh

[1] 
https://gist.github.com/mukeshtiwari/66a24eff6ac598e691c341d3faafb5d2#file-custom-v-L98

On Mon, Jun 6, 2022 at 7:04 PM mukesh tiwari
<mukeshtiwari.iiitm AT gmail.com> wrote:
>
> 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