The Coq mailing list

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

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