The Coq mailing list

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

Hi Mukesh,

Concerning your first question, a possible proof would be as given below.

Now, for the "proper_subset" relation, I suggest you have a look at

https://github.com/DmxLarchey/PC19/blob/master/wf_incl.v

The definition of "proper_subset" is identical to "sincl" there 
(except the conjunction is in the reverse order).

The proof of the PHP (pigeon hole principle) is now part 
of the standard library (I think). The one given in

https://github.com/DmxLarchey/PC19/blob/master/php.v

is not particularily short/clean. The one given here
is a bit cleaner 

https://github.com/DmxLarchey/PHP-short/blob/main/php.v

The idea of the proof that proper_subset/sincl 
is well-founded is to show that every 
finite sincl-decrease sequence (a notion 
characterized inductively)

   l_n sincl l_{n-1} sincl l_{n-2} sincl ... sincl l_0

has length n bounded by the length of l_0. 

The reason is that one can extract, from the decreasing 
sequence l_n,...,l_0, a list m such that 
1) m is *duplication free*
2) m is included in l_0
3) length m = n
This list is composed of the witnesses of strict 
decrease.

Then, by the PHP, m cannot be strictly longer than l_0
hence n <= length l_0.

If there is a (common) bound on the length every *finite* 
sincl-decreasing sequence starting from l_0 then 
l_0 is accessible for sincl. From this, well foundness
follows.

Best,

D.


Require Import Arith List Wellfounded.

Section MuTi.

  Variables (X : Type).

  Implicit Type (l : list X).

  Print incl.

  Lemma well_founded_subset : well_founded (fun l m => incl l m /\ length l < 
length m).
  Proof.
    apply wf_incl with (R2 := fun l m => length l < length m).
    + now intros ? ? [].
    + apply wf_inverse_image, lt_wf.
  Qed.

End MuTi.






----- Mail original -----
> De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Lundi 5 Décembre 2022 10:16:35
> Objet: Re: [Coq-Club] Proper subset relation well-founded?

> Hi Dominique,
> 
> I think I get your idea of ""there is a point in ys which is not in xs".
> I came with this definition of proper_subset:
> 
> Definition proper_subset {A : Type} (xs ys : finset A) : Prop :=
>   (∀ x : A, In x xs -> In x ys) ∧
>  (∃ y : A, In y ys ∧ ~In y xs).
> 
> Now I need to figure out how to encode the "strict decrease" because,
> as you suggested, [1;1;1] is a proper subset of [1; 2; 2]. (seems an
> interesting proof).
> 
> 
> Best,
> Mukesh
> 
> On Mon, Dec 5, 2022 at 6:24 PM mukesh tiwari
> <mukeshtiwari.iiitm AT gmail.com> wrote:
>>
>> Hi Dominique,
>>
>> "However, it does not properly characterize proper subsets IMHO.
>> Indeed you have eg [1;1] is a proper subset of [1;2;2] but also of
>> [1;1;1]." Agree and that is why I used List.length to get rid of these
>> kinds of examples and force strict decrease.
>>
>> "I would suggest using "there is a point in ys which is not in xs"
>> (rather than the length criteria) to witness strict decrease. Also wf
>> but somewhat harder to prove. I can point to some code if needed."
>> That will be great if you can point me to some code for this.
>>
>> Best,
>> Mukesh
>>
>> On Mon, Dec 5, 2022 at 5:26 PM Dominique Larchey-Wendling
>> <Dominique.Larchey-Wendling AT loria.fr> wrote:
>> >
>> > Hi Mukesh,
>> >
>> > Your "subset" relation is included in the relation length xs < length ys 
>> > so it
>> > is wf by combination of wf_incl, wf_inverse_image and lt_wf. 
>> > Decidability of eq
>> > is *not* needed.
>> >
>> > However, it does not properly characterize proper subsets IMHO. Indeed 
>> > you have
>> > eg [1;1] is a proper subset of [1;2;2] but also of [1;1;1].
>> >
>> > I would suggest using "there is a point in ys which is not in xs" 
>> > (rather than
>> > the length criteria) to witness strict decrease. Also wf but somewhat 
>> > harder to
>> > prove. I can point to some code if needed.
>> >
>> > Best,
>> >
>> > Dominique
>> >
>> > Le 5 décembre 2022 06:50:10 GMT+01:00, mukesh tiwari
>> > <mukeshtiwari.iiitm AT gmail.com> a écrit :
>> >>
>> >> Hi everyone,
>> >>
>> >> Is this (proper) subset relation is well-founded? Based on my 
>> >> understand, I
>> >> believe the answer is no (and maybe we need more assumptions), but I am 
>> >> happy
>> >> be proven otherwise.  You can see the complete code [1].
>> >>
>> >>
>> >> Definition finset (A : Type) := list A.
>> >>
>> >> (* proper subset *)
>> >>
>> >> Definition subset {A : Type} (xs ys : finset A) : Prop :=
>> >>  (∀ x, In x xs -> In x ys) ∧
>> >>  (List.length xs < List.length ys). (* for proper subset *)
>> >>
>> >>
>> >>
>> >> Lemma well_founded_subset {A : Type} :
>> >> (∀ x y : A, {x = y} + {x ≠ y}) ->
>> >> well_founded (@subset A).
>> >> Proof.
>> >>
>> >>   intro Hdec.
>> >>   unfold well_founded.
>> >>   induction a as [| ah al Iha].
>> >>   + econstructor;
>> >>     intros ? [Hyl Hyr].
>> >>     simpl in Hyr; nia.
>> >>   +
>> >>     (* Induction Hypothesis peeling *)
>> >>     pose proof (Acc_inv  Iha) as Ha.
>> >>     (* transitivity *)
>> >>     econstructor;
>> >>     intros xt Hx.
>> >>     (* I can unfold one more time, but
>> >>       will I get anything meaningful? *)
>> >>     econstructor;
>> >>     intros yt Hy.
>> >>     (* case analysis *)
>> >>     destruct (List.In_dec Hdec ah yt) as [Hb | Hb].
>> >>     ++
>> >>
>> >>       (* In ah yt *)
>> >>       pose proof (subset_member _ _ _ Hb Hy) as Hc.
>> >>     (*
>> >>       ah ∈ xs so I can write
>> >>       xs = xsl ++ [ah] ++ xsr.
>> >>       From Hx : subset xt (ah :: al)
>> >>       I can infer: subset (xsl ++ xsr) al.
>> >>       But there is no way I can establish:
>> >>       subset yt (xsl ++ xsr) for transitive and
>> >>       induction hypothesis to work.
>> >>
>> >>       My conclusion is: it's not provable but
>> >>       happy to be proven wrong.
>> >>
>> >>       If it's not provable, can we make subset relation
>> >>       well founded?
>> >>
>> >>     *)
>> >>     admit.
>> >>   ++ admit.
>> >> Admitted.
>> >>
>> >>
>> >> Best,
>> >> Mukesh
>> >>
>> >>
>> >> [1]
> > >> https://gist.github.com/mukeshtiwari/ecdebdae6f28ddf4b231d160b16de37d