The Coq mailing list

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

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