The Coq mailing list

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

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