The Coq mailing list

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

Thanks Dominique, your hint was more than enough to discharge the proof [1].

Best,
Mukesh

[1] https://github.com/mukeshtiwari/CoqUtil/blob/main/src/Fin.v#L270-L322

On Sat, Jun 18, 2022 at 6:16 PM Dominique Larchey-Wendling
<dominique.larchey-wendling AT loria.fr> wrote:
>
> Hi Mukesh,
>
> "Understandable but I have mt = S nt so I get ..." from [1]
>
> Be careful, the identity mt = S nt does *not* make nt a sub-term
> of mt.
>
> The sub-term relation *cannot be expressed* by a term of the
> Coq language, it is only recognized by the type-checker.
>
> Basically here, you need to destruct mt as [ | nt' ],
> *call the fixpoint on nt'* and then possibly rewrite nt'
> as nt after having proved that nt = nt'. The case where
> mt is 0 can be discriminated away.
>
> Best,
>
> Dominique
>
> ----- Mail original -----
> > De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> > À: "coq-club" <coq-club AT inria.fr>
> > Envoyé: Samedi 18 Juin 2022 09:52:29
> > Objet: Re: [Coq-Club] Custom Induction Principal for le_unique
>
> > 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